cpt_mass_equality
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.
claimLet $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 in Recognition Science
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.
scope and limits
- Does not establish CPT invariance from ledger axioms alone.
- Does not apply to continuous fields or non-discrete representations.
- Does not address spin, momentum, or other quantum numbers.
- Does not incorporate numerical values from the phi-ladder or alpha band.
formal statement (Lean)
198theorem cpt_mass_equality :
199 ∀ (mass : LedgerEntry → ℝ),
200 (∀ e, mass e = mass (applyCPT e)) → -- CPT invariance
201 (∀ e, mass e = mass (applyPT e)) → -- PT invariance (locality)
202 (∀ e, mass e = mass (applyC e)) := by
proof body
Tactic-mode proof.
203 intro mass hCPT hPT e
204 -- CPT = C ∘ PT, so CPT ∘ PT⁻¹ = C (since PT is involutive, PT⁻¹ = PT)
205 -- mass(e) = mass(CPT(e)) = mass(C(P(T(e))))
206 -- mass(PT(e)) = mass(e) by hPT
207 -- Apply CPT to PT(e): mass(PT(e)) = mass(CPT(PT(e)))
208 -- CPT(PT(e)) = C(P(T(P(T(e))))) = C(P(T(P(T(e)))))
209 -- But PT(PT(e)) = e, so CPT(PT(e)) = C(e)
210 -- Thus mass(e) = mass(PT(e)) = mass(CPT(PT(e))) = mass(C(e))
211 have h1 : mass (applyPT e) = mass e := (hPT e).symm
212 have h2 : mass (applyPT e) = mass (applyCPT (applyPT e)) := hCPT (applyPT e)
213 have h3 : applyCPT (applyPT e) = applyC e := by
214 simp only [applyCPT, applyC, applyP, applyT, applyPT]
215 cases e with
216 | mk pos tick charge cost cost_nonneg =>
217 congr 1
218 · funext i; simp only [neg_neg]
219 · exact reverseTick_involutive _
220 rw [h3] at h2
221 rw [← h1, h2]
222
223/-- **THEOREM (Lifetime Equality)**: CPT + PT invariance implies lifetimes are C-invariant. -/