pith. machine review for the scientific record. sign in
structure definition def or abbrev high

LedgerState

show as:
view Lean formalization →

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.

claimA 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 in Recognition Science

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.

scope and limits

formal statement (Lean)

  38structure LedgerState where
  39  entries : List ℂ
  40  phase : ℝ  -- Global phase
  41
  42/-- Two ledger states are physically equivalent if they differ only by a global phase.
  43
  44    This is the origin of U(1) gauge symmetry! -/

used by (40)

From the project-wide theorem graph. These declarations reference this one in their body.

… and 10 more

depends on (17)

Lean names referenced from this declaration's body.