def
definition
applyP
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 93.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
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
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. -/