Ledger

formal source

  70  cost_nonneg : cost ≥ 0
  71
  72/-- A ledger is a collection of balanced entries. -/
  73structure Ledger where
  74  /-- The entries. -/
  75  entries : List LedgerEntry
  76  /-- Double-entry balance: charges sum to zero. -/
  77  balanced : (entries.map LedgerEntry.charge).sum = 0
  78
  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)⟩