LedgerState
plain-language theorem explainer
Ledger states consist of a finite list of complex amplitudes together with one global real phase. Gauge theorists deriving U(1) symmetry from information redundancy cite this record as the primitive object. The declaration is a direct structure definition carrying no proof obligations.
Claim. A ledger state is a pair consisting of a finite sequence of complex numbers $(z_i)$ and a real phase angle $θ ∈ ℝ$.
background
Recognition Science encodes physical reality in ledgers whose representational redundancy produces gauge freedom. The module derives U(1) invariance from the observation that distinct ledger representations can describe identical events. Upstream results supply the eight-tick phase map giving discrete angles $kπ/4$ for $k=0,…,7$, the RS-native units fixing $c=1$, and the ledger factorization structure that calibrates the underlying J-cost.
proof idea
The declaration is a direct structure definition introducing the two fields entries and phase.
why it matters
This structure supplies the root object for all gauge-invariance arguments in the framework. It is invoked by the diagonal Hamiltonian in HamiltonianEmergence and by the ledger-identity theorem in InformationIsLedger. It realizes the module claim that gauge symmetry originates in ledger redundancy and links to the eight-tick octave through its phase field.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.