reverseTick

formal source

 100/-! ## T Symmetry: Time Reversal from 8-Tick Reversal -/
 101
 102/-- Reverse a tick in the 8-tick cycle: t ↦ 7 - t (mod 8). -/
 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]