cpt_involutive
plain-language theorem explainer
The theorem establishes that the combined charge-parity-time operator is an involution on ledger entries in Recognition Science. A physicist working on discrete QFT models would cite this to confirm that CPT symmetry holds exactly at the ledger level. The proof proceeds by case analysis on the ledger structure and direct verification that each component (position, tick, charge) is restored after two applications.
Claim. For every ledger entry $e$ with position in $Fin 3 → ℝ$, phase tick, integer charge, and non-negative cost, the composition of charge conjugation, parity inversion, and time reversal satisfies $CPT(CPT(e)) = e$.
background
The module derives CPT invariance from the ledger's double-entry structure in Recognition Science. A LedgerEntry is the structure recording a recognition event: position as a map from Fin 3 to reals, tick as the fundamental phase, charge as an integer, and cost as a non-negative real. The local setting is QFT-005, where C arises from J-cost symmetry, P from D=3 isotropy, and T from the reversible 8-tick cycle. Upstream results supply the tick as the RS-native time quantum τ₀ = 1 and cost as the J-cost of a recognition event.
proof idea
The term proof cases on the LedgerEntry mk constructor, then applies simp on the definitions of applyCPT, applyC, applyP, and applyT. Congruence reduces the equality to the three fields. Position equality follows from funext and neg_neg; tick equality invokes the reverseTick involution lemma; charge equality follows from neg_neg.
why it matters
This result shows that CPT is conserved even when individual C, P, or T symmetries can be violated, as required by the ledger double-entry structure. It fills the CPT theorem step in the QFT-005 paper proposition for PRL. The result rests on the eight-tick octave and D=3 forcing from the T0-T8 chain, closing a discrete symmetry that standard QFT assumes but does not derive.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.