pith. machine review for the scientific record. sign in
def definition def or abbrev high

cptBounds

show as:
view Lean formalization →

Current PDG experimental bounds on CPT-violating mass differences are stored as a string constant. Particle physicists comparing discrete symmetry tests to Recognition Science ledger predictions would cite these values. The definition is assembled by direct string concatenation of three bound statements with no computation.

claimThe experimental upper bounds on CPT violation are $ |Δm/m| < 10^{-9} $ for proton/antiproton, $ |Δm/m| < 8×10^{-9} $ for electron/positron, and $ |Δm| < 10^{-18} $ GeV for $ K^0/¯K^0 $.

background

The QFT-005 module derives CPT invariance from the ledger's double-entry structure in Recognition Science. C-symmetry follows from J-cost symmetry J(x) = J(1/x), P-symmetry from D=3 lattice isotropy, and T-symmetry from reversibility of the eight-tick cycle. The module states that while individual C, P, or T may be violated, their combination CPT remains conserved. Upstream, K is defined as the dimensionless bridge ratio φ^{1/2}.

proof idea

The definition is a direct string literal formed by concatenation of three bound statements. No lemmas or tactics are invoked; it is a constant definition.

why it matters in Recognition Science

This definition supplies the empirical reference points for the module's claim that CPT follows from ledger symmetry. It supports the target of deriving CPT invariance from Recognition Science's discrete structure, consistent with the eight-tick octave and D=3. No downstream uses are recorded, leaving open integration into quantitative mass-ladder predictions.

scope and limits

formal statement (Lean)

 260def cptBounds : String :=

proof body

Definition body.

 261  "Proton/antiproton mass: |Δm/m| < 10⁻⁹\n" ++
 262  "Electron/positron mass: |Δm/m| < 8×10⁻⁹\n" ++
 263  "K⁰/K̄⁰ mass: |Δm| < 10⁻¹⁸ GeV"
 264
 265/-- CPT violation bound (proton/antiproton relative mass difference). -/

depends on (2)

Lean names referenced from this declaration's body.