cpt_lifetime_equality
CPT invariance together with PT invariance forces lifetimes to be invariant under charge conjugation alone. Researchers deriving discrete symmetries from ledger structures in Recognition Science would cite this when showing that particle-antiparticle lifetime equality follows from the combined symmetries. The proof is a short tactic sequence that composes the given equalities with the involution of the operators to isolate the C action.
claimLet $l :$ LedgerEntry $→ ℝ$ be any lifetime function. If $l(e) = l($applyCPT$(e))$ for every ledger entry $e$ and $l(e) = l($applyPT$(e))$ for every $e$, then $l(e) = l($applyC$(e))$ for every $e$.
background
The module QFT-005 derives CPT invariance from the ledger's double-entry structure in Recognition Science. A LedgerEntry records a recognition event by a 3-vector position in Fin 3 → ℝ, a Phase tick, an integer charge, and a nonnegative real cost. The operators applyC, applyP, applyT, applyPT and applyCPT implement charge conjugation, parity, time reversal and their compositions on these entries. Upstream, the tick constant supplies the fundamental time quantum τ₀ = 1, while cost functions descend from the multiplicative recognizer and observer forcing layers.
proof idea
The tactic proof introduces the lifetime function and the two invariance hypotheses. It forms an auxiliary equality by applying the PT hypothesis, then substitutes the CPT hypothesis on the PT-transformed entry. A case split on the LedgerEntry constructor together with simp on the operator definitions shows that applyCPT ∘ applyPT equals applyC, using reverseTick_involutive and negation involution. Two rewrites close the chain to the C-invariance conclusion.
why it matters in Recognition Science
The result supplies one concrete implication inside the CPT derivation from ledger symmetry. It shows how the combination of CPT and PT forces C-invariance for lifetimes, aligning with the module claim that CPT is always conserved while individual C, P or T may be violated. The argument rests on the J-cost symmetry and eight-tick octave already established in the foundation layer.
scope and limits
- Does not prove the CPT or PT invariance hypotheses themselves.
- Does not extend the equality to mass or charge observables.
- Does not treat continuous spacetime symmetries or field operators.
- Remains inside the discrete ledger representation of recognition events.
formal statement (Lean)
224theorem cpt_lifetime_equality :
225 ∀ (lifetime : LedgerEntry → ℝ),
226 (∀ e, lifetime e = lifetime (applyCPT e)) →
227 (∀ e, lifetime e = lifetime (applyPT e)) →
228 (∀ e, lifetime e = lifetime (applyC e)) := by
proof body
Tactic-mode proof.
229 intro lifetime hCPT hPT e
230 -- Same proof structure as mass equality
231 have h1 : lifetime (applyPT e) = lifetime e := (hPT e).symm
232 have h2 : lifetime (applyPT e) = lifetime (applyCPT (applyPT e)) := hCPT (applyPT e)
233 have h3 : applyCPT (applyPT e) = applyC e := by
234 simp only [applyCPT, applyC, applyP, applyT, applyPT]
235 cases e with
236 | mk pos tick charge cost cost_nonneg =>
237 congr 1
238 · funext i; simp only [neg_neg]
239 · exact reverseTick_involutive _
240 rw [h3] at h2
241 rw [← h1, h2]
242
243/-! ## Falsification Criteria -/
244
245/-- CPT violation would be detected by:
246 1. Mass difference between particle and antiparticle
247 2. Lifetime difference between particle and antiparticle
248 3. Charge-to-mass ratio difference -/