theorem
proved
tactic proof
cpt_mass_equality
show as:
view Lean formalization →
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. -/