cpt_bound_tight
plain-language theorem explainer
The theorem establishes that the CPT mass bound from Recognition Science ledger symmetry is strictly less than 10^{-8}. Experimental physicists checking discrete symmetries would cite it to match the lack of observed CPT violation at current precision. The proof is a one-line numerical normalization that directly evaluates the bound constant.
Claim. The bound on CPT-violating mass differences satisfies $cpt_mass_bound < 10^{-8}$ in natural units.
background
In the QFT-005 module, CPT invariance emerges from the ledger's double-entry structure. Charge conjugation follows from the J-cost symmetry J(x) = J(1/x), parity from 3D lattice reflection forced by D=3, and time reversal from the bidirectional 8-tick cycle. The upstream cpt_mass_bound supplies the quantitative bound on violation arising from these symmetries. The module targets derivation of CPT conservation from discrete ledger structure, noting that the combination remains conserved even when individual symmetries break.
proof idea
The proof is a one-line term-mode wrapper that applies norm_num to the cpt_mass_bound definition, reducing the inequality to direct numerical evaluation.
why it matters
This result confirms the experimental tightness of the CPT bound inside the Recognition Science framework and supports the ledger-symmetry derivation of CPT invariance. It aligns with the eight-tick octave (T7) and D=3 from the forcing chain. No downstream uses appear, but the declaration closes the loop on the paper claim for CPT from discrete ledger structure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.