cpt_mass_bound
plain-language theorem explainer
The declaration sets the numerical upper limit on any CPT-violating relative mass difference between proton and antiproton at one part in a billion. Particle physicists comparing Recognition Science ledger predictions against precision CPT tests would cite this constant when stating experimental consistency. It is introduced as a direct rational assignment with no derivation or proof steps.
Claim. The CPT violation bound on the relative mass difference between proton and antiproton is defined as the rational number $1/10^9$.
background
The QFT-005 module derives CPT invariance from the double-entry ledger structure of Recognition Science. Charge conjugation arises from the J-cost symmetry J(x) = J(1/x), parity from the reflection symmetry of the three-dimensional voxel lattice, and time reversal from the bidirectional eight-tick cycle. The bound quantifies how tightly these symmetries are observed to hold for the proton-antiproton system.
proof idea
This is a one-line definition that directly assigns the rational constant 1/10^9 to cpt_mass_bound.
why it matters
It supplies the numerical threshold referenced by the downstream theorems cpt_bound_tight and no_observed_cpt_violation, which assert that current experiments show no CPT violation. The value anchors the theoretical claim of exact CPT conservation, forced by ledger symmetry in the Recognition Science framework, to the experimental precision of 10^{-9}.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.