Generators, Closure, and Universality: A Minimal Deterministic Theory with Machine-Checked Proofs

We develop an entirely parameter-free theory in which observables emerge solely from generators through closure.No external constants, models, or phenomenological inputs are permitted. This design forces determinism and uniqueness at the syntactic level and yields structural minimality and completeness as direct consequences of the algebraic construction.We establish a universal embedding theorem characterizing the generator algebra as an initial deterministic structure. All arguments are formalized in Lean 4 and verified by the proof kernel, providing complete mechanical certification of correctness. The framework illustrates how foundational theories can be derived purely from algebraic principles while remaining fully machine-verifiable.