cpt_mass_equality
plain-language theorem explainer
CPT invariance of mass together with PT invariance forces invariance under charge conjugation, establishing equal masses for particles and antiparticles. Researchers deriving discrete symmetries in Recognition Science QFT models would cite this implication. The tactic proof reduces the claim by rewriting the composition CPT composed with PT using the involution of PT and case analysis on the ledger entry structure.
Claim. Let $m$ assign real values to ledger entries. If $m(e) = m(CPT(e))$ and $m(e) = m(PT(e))$ for every ledger entry $e$, then $m(e) = m(C(e))$ for every $e$.
background
A LedgerEntry is a recognition event carrying position in three-dimensional space, time as a Phase (tick number), integer charge, and nonnegative cost. The cost is the J-cost of the state, drawn from the multiplicative recognizer and observer forcing constructions. The tick is the fundamental RS time quantum with value 1 in native units, and the eight-tick cycle supplies the time-reversal symmetry.
proof idea
The tactic proof introduces the mass function and the two invariance hypotheses. It forms the auxiliary equalities mass(PT e) = mass e and mass(PT e) = mass(CPT(PT e)), then simplifies CPT composed with PT to C by simp on the operator definitions followed by case analysis on the LedgerEntry constructor and application of reverseTick_involutive. Rewriting yields the required mass(e) = mass(C e).
why it matters
The result fills the mass-equality step in the QFT-005 derivation of CPT invariance from ledger symmetry. It uses the double-entry structure that supplies C from J-cost symmetry and T from the eight-tick octave, showing that the combination CPT plus PT yields C alone. No downstream theorems are recorded, indicating the lemma supports further QFT constructions such as lifetime equality.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.