LedgerEntry
plain-language theorem explainer
LedgerEntry structures a recognition event as a 3D position vector, phase tick, integer charge, and non-negative real cost. Researchers deriving CPT invariance from discrete ledger symmetries in Recognition Science cite this as the atomic object. The declaration is a plain structure definition that directly encodes the fields and the cost non-negativity constraint.
Claim. A ledger entry consists of a position $p : Fin 3 → ℝ$, a phase tick $τ$, an integer charge $q ∈ ℤ$, and a cost $c ∈ ℝ$ satisfying $c ≥ 0$.
background
In the QFT.CPTInvariance module the ledger encodes recognition events whose symmetries yield CPT. Position uses Fin 3 to index the three spatial dimensions forced by the eight-tick octave and D=3. Tick imports the fundamental time quantum τ₀ = 1 from Constants, while charge is an integer indicator and cost carries the explicit non-negativity axiom. Upstream LedgerFactorization supplies the underlying (ℝ₊, ×) structure and J calibration that later convert cost into the J-cost used by QuantumLedger.
proof idea
This is a structure definition that directly encodes the five fields with the cost non-negativity constraint. No lemmas are applied; the declaration simply introduces the type used by downstream Ledger and entry_cost_nonneg.
why it matters
LedgerEntry supplies the atomic objects for the Ledger structure in QuantumLedger, which enforces balance and conservation. It fills the discrete carrier needed for the CPT theorem in the module, where C arises from J(x)=J(1/x), P from 3D isotropy, and T from 8-tick reversibility. The structure therefore sits at the base of the ledger-forcing chain and feeds every subsequent CPT operation and cost theorem.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.