theorem proved term proof

`cpt_composition`

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

formal statement (Lean)

 107theorem cpt_composition :
 108    -- C, P, T each correspond to phase flips on the 3 hypercube axes
 109    -- Their composition is the identity (phase 0)
 110    phaseExp ⟨0, by norm_num⟩ = 1 := phase_0_is_one

proof body

Term-mode proof.

 111
 112/-! ## Summary Certificate -/
 113
 114/-- **SPIN-STATISTICS CERTIFICATE**:
 115    All claims in `RS_Spin_Statistics_Theorem.tex` are certified by this module
 116    and `Foundation.EightTick`. No hypotheses remain. -/

depends on (13)

Lean names referenced from this declaration's body.

T in IndisputableMonolith.Foundation.Breath1024 decl_use
phase in IndisputableMonolith.Foundation.EightTick decl_use
phase_0_is_one in IndisputableMonolith.Foundation.EightTick decl_use
phaseExp in IndisputableMonolith.Foundation.EightTick decl_use
identity in IndisputableMonolith.Foundation.ObserverForcing decl_use
is in IndisputableMonolith.Foundation.OptionAEmpiricalProgram decl_use
is in IndisputableMonolith.Foundation.SimplicialLedger.EdgeLengthFromPsi decl_use
is in IndisputableMonolith.GameTheory.MechanismDesignFromSigma decl_use
T in IndisputableMonolith.Gap45.SyncMinimization decl_use
is in IndisputableMonolith.Mathematics.RamanujanBridge.MockThetaPhantom decl_use
and in IndisputableMonolith.NumberTheory.CirclePhaseLift decl_use
phase in IndisputableMonolith.NumberTheory.RiemannHypothesis.Wedge decl_use
identity in IndisputableMonolith.RRF.Foundation.VantageCategory decl_use