applyC

formal source

  79/-! ## C Symmetry: Charge Conjugation from J(x) = J(1/x) -/
  80
  81/-- Apply charge conjugation to a ledger entry. -/
  82def applyC (e : LedgerEntry) : LedgerEntry :=
  83  { e with charge := -e.charge }
  84
  85/-- **THEOREM**: Charge conjugation preserves cost.
  86    This is the J(x) = J(1/x) symmetry at the ledger level. -/
  87theorem c_preserves_cost (e : LedgerEntry) :
  88    (applyC e).cost = e.cost := rfl
  89
  90/-! ## P Symmetry: Parity from Voxel Reflection -/
  91
  92/-- Apply parity (spatial reflection) to a ledger entry. -/
  93def applyP (e : LedgerEntry) : LedgerEntry :=
  94  { e with position := fun i => -(e.position i) }
  95
  96/-- **THEOREM**: Parity preserves cost (J is rotationally invariant). -/
  97theorem p_preserves_cost (e : LedgerEntry) :
  98    (applyP e).cost = e.cost := rfl
  99
 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