pith. machine review for the scientific record. sign in
theorem proved term proof

cpt_involutive

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

formal statement (Lean)

 156theorem cpt_involutive (e : LedgerEntry) :
 157    applyCPT (applyCPT e) = e := by

proof body

Term-mode proof.

 158  -- Show each field is restored
 159  cases e with
 160  | mk pos tick charge cost cost_nonneg =>
 161    simp only [applyCPT, applyC, applyP, applyT]
 162    congr 1
 163    · -- position: -(-x) = x
 164      funext i
 165      simp only [neg_neg]
 166    · -- tick: reverseTick (reverseTick p) = p
 167      exact reverseTick_involutive tick
 168    · -- charge: -(-c) = c
 169      simp only [neg_neg]
 170
 171/-! ## Individual Symmetry Violations -/
 172
 173/-- C, P, T can be individually violated, but CPT is always conserved. -/

depends on (21)

Lean names referenced from this declaration's body.