Ledger
plain-language theorem explainer
A Ledger is a finite list of recognition events whose charges sum to zero. Researchers deriving CPT invariance from Recognition Science ledger symmetry cite this structure to encode double-entry balance. The definition is a direct structure pairing the entry list with the zero-sum predicate on charges.
Claim. A ledger is a list of entries $e_i$, each with position in $Fin 3 → ℝ$, tick in Phase, charge in $ℤ$, and non-negative cost, such that $∑_i charge(e_i) = 0$.
background
The module QFT-005 derives CPT invariance from the ledger's double-entry structure. C-symmetry arises from the J(x) = J(1/x) cost symmetry, P-symmetry from D=3 isotropy, and T-symmetry from the reversible eight-tick cycle. A LedgerEntry is a recognition event carrying position in three dimensions, a Phase tick, integer charge, and non-negative cost. The upstream balanced predicate requires that the charge list of any ledger sums to zero, enforcing the double-entry rule at the structural level.
proof idea
This is a structure definition that directly bundles the entries list with the balanced condition. It references the upstream balanced predicate on event lists and the LedgerEntry structure to enforce zero total charge.
why it matters
The structure supplies the balanced collection required for the CPT theorem in the QFT-005 module. It implements the ledger symmetry that forces C-invariance via charge conjugation and supports the combination with P and T operations. The declaration sits at the base of the CPT derivation chain and connects to the eight-tick octave and D=3 spatial forcing from the UnifiedForcingChain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.