def
definition
applyPT
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
open lean source
IndisputableMonolith.QFT.CPTInvariance on GitHub at line 184.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
181/-! ## CPT Predictions -/
182
183/-- PT transformation (parity + time reversal). -/
184def applyPT (e : LedgerEntry) : LedgerEntry :=
185 applyP (applyT e)
186
187/-- Helper: PT is involutive -/
188theorem pt_involutive (e : LedgerEntry) : applyPT (applyPT e) = e := by
189 simp only [applyPT, applyP, applyT]
190 cases e with
191 | mk pos tick charge cost cost_nonneg =>
192 congr 1
193 · funext i; simp only [neg_neg]
194 · exact reverseTick_involutive _
195
196/-- **THEOREM (Mass Equality)**: CPT + PT invariance implies C invariance.
197 This shows that particles and antiparticles have equal mass. -/
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
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]