def
definition
applyT
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 106.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
103def reverseTick (p : Phase) : Phase := ⟨(7 - p.val) % 8, Nat.mod_lt _ (by norm_num)⟩
104
105/-- Apply time reversal to a ledger entry. -/
106def applyT (e : LedgerEntry) : LedgerEntry :=
107 { e with tick := reverseTick e.tick }
108
109/-- **THEOREM**: Time reversal preserves cost. -/
110theorem t_preserves_cost (e : LedgerEntry) :
111 (applyT e).cost = e.cost := rfl
112
113/-! ## CPT: The Combined Transformation -/
114
115/-- Apply the full CPT transformation to a ledger entry. -/
116def applyCPT (e : LedgerEntry) : LedgerEntry :=
117 applyC (applyP (applyT e))
118
119/-- **THEOREM (CPT Invariance)**: The CPT transformation preserves cost. -/
120theorem cpt_preserves_cost (e : LedgerEntry) :
121 (applyCPT e).cost = e.cost := rfl
122
123/-- **THEOREM**: CPT preserves ledger balance. -/
124theorem cpt_preserves_balance (L : Ledger) :
125 ((L.entries.map applyCPT).map LedgerEntry.charge).sum = 0 := by
126 -- C negates charges: sum of negated charges = -(sum of charges) = -0 = 0
127 have hsum : (L.entries.map LedgerEntry.charge).sum = 0 := L.balanced
128 -- The transformed charge is -e.charge for each entry
129 have h_map : (L.entries.map applyCPT).map LedgerEntry.charge =
130 L.entries.map (fun e => -e.charge) := by
131 rw [List.map_map]
132 congr 1
133 rw [h_map]
134 -- Sum of negations = -(sum)
135 rw [show (L.entries.map (fun e => -e.charge)).sum =
136 -(L.entries.map LedgerEntry.charge).sum by