cpt_composition
plain-language theorem explainer
CPT invariance in Recognition Science follows from the composition of the three parity operations on the Q3 hypercube reducing to the zero phase. Workers on discrete models of spin and statistics would reference this result when connecting the eight-tick structure to particle exchange symmetries. The argument applies the established identity for the phase exponential at zero.
Claim. The composition of charge conjugation, parity, and time reversal on the three axes of the hypercube yields the zero phase in the eight-tick cycle, so that the complex exponential of that phase equals one: $e^{i0}=1$.
background
The module derives the spin-statistics theorem from the eight-tick ledger. The phase function maps each index k in Fin 8 to kπ/4. phaseExp then forms the complex value exp(i times that phase). Upstream phase_0_is_one states that this exponential equals 1 at k=0, which is the identity or boson phase. The local setting is the complete spin-statistics connection from the RS eight-tick structure, with no hypotheses remaining.
proof idea
The proof is a one-line term wrapper that directly invokes the upstream theorem phase_0_is_one. That theorem unfolds phaseExp and phase, then simplifies the zero case using exp(0)=1.
why it matters
This supplies the RS statement of CPT invariance inside the spin-statistics derivation. It rests on the eight-tick octave and the hypercube model for three spatial dimensions. The result supports the module's spin_statistics_theorem, pauli_exclusion, and the overall certificate that all claims in the associated paper are certified with no hypotheses left.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.