reverseTick_involutive
plain-language theorem explainer
The reverse tick map on the 8-tick phase space is an involution. Researchers deriving discrete CPT symmetries from ledger structures would cite it to confirm that time reversal squares to the identity. The proof is a direct modular-arithmetic reduction that uses the bound p.val < 8 together with omega to cancel the double application.
Claim. Let $r: {0,1,…,7} → {0,1,…,7}$ be defined by $r(p) = (7-p) mod 8$. Then $r(r(p)) = p$ for every phase $p$.
background
Phase is the finite set Fin 8 that labels the discrete steps of the eight-tick octave forced by the self-similar fixed point (T7). The reverseTick definition implements time reversal on this cycle by the rule $t ↦ 7-t$ (mod 8), which encodes the ledger’s forward-backward symmetry. The module QFT.CPTInvariance derives the full CPT operator from the combination of charge conjugation (J-cost duality), parity (D=3 lattice reflection), and this time reversal.
proof idea
Unfold reverseTick by simp, apply extensionality, then use the hypothesis p.isLt together with Nat.mod_eq_of_lt and omega to show that the double subtraction 7-(7-p.val) recovers p.val and that both intermediate results remain inside the modulus-8 range.
why it matters
The lemma supplies the T-component needed for cpt_involutive, cpt_mass_equality and cpt_lifetime_equality, which together establish that CPT is an involution and that particles and antiparticles share mass and lifetime. It therefore completes the discrete CPT theorem stated in the module’s paper proposition (PRL target) and rests on the eight-tick structure (T7) of the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.