cpt_preserves_balance
plain-language theorem explainer
The theorem shows that CPT transformation on a balanced ledger leaves the total charge sum at zero. Researchers deriving CPT invariance from discrete ledger symmetries in Recognition Science would cite this when building QFT foundations. The proof extracts the original zero sum, rewrites the CPT-mapped charges as negated charges via list composition, then applies induction to confirm the negated sum equals the negation of zero.
Claim. Let $L$ be a ledger whose entries satisfy $sum_e charge(e) = 0$. Then $sum_e charge(CPT(e)) = 0$.
background
In the QFT-005 module, CPT invariance follows from the ledger's double-entry structure. A Ledger is a list of LedgerEntry records, each carrying an integer charge together with position, tick, and cost; the structure requires that the sum of charges over all entries equals zero. This zero-sum condition encodes the recognition accounting that underlies particle-antiparticle duality via the J-cost symmetry J(x) = J(1/x). The module treats C, P, and T as separate discrete symmetries forced by the J-function, D = 3 isotropy, and the eight-tick cycle, yet proves their composite CPT is strictly conserved. Upstream, the balanced property is supplied by LedgerForcing.balanced, which asserts every ledger satisfies the zero-sum condition by construction.
proof idea
The tactic proof first binds the original zero sum from L.balanced. It then rewrites the charge list after applyCPT as the list of negated charges using List.map_map and a congruence step. An induction on the entry list establishes that the sum of negated charges equals the negation of the original sum; the final steps substitute the zero sum and apply neg_zero.
why it matters
This result supplies the core CPT conservation statement inside the Recognition Science ledger framework and directly supports the paper proposition on CPT from discrete ledger structure. It closes the loop on the forcing chain landmarks T7 (eight-tick octave) and T8 (D = 3), showing that the combination of symmetries preserves balance even when individual C, P, or T operations may not. With zero downstream uses recorded, the theorem functions as a terminal lemma for subsequent QFT derivations rather than an intermediate step.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.