CPTFalsifier
plain-language theorem explainer
The CPTFalsifier structure records a particle identifier together with real-valued mass and lifetime differences between particle and antiparticle, plus a disjunction asserting that at least one difference is nonzero. Experimental groups comparing Recognition Science ledger predictions to PDG data would cite the structure when tabulating candidate CPT violations. The declaration is a bare structure definition with no computational reduction or lemma application.
Claim. A structure consisting of a string $p$ for the particle type, real numbers $m$ and $t$ for the mass and lifetime differences, and a witness that $m = 0$ is false or $t = 0$ is false.
background
The module derives CPT invariance from the double-entry ledger of Recognition Science. Charge conjugation follows from the J-cost symmetry J(x) = J(1/x) established in PhiForcingDerived.of. Parity is forced by the three-dimensional voxel lattice in SpectralEmergence.of, while time reversal follows from the forward-or-backward eight-tick cycle in the imported EightTick module. Upstream LedgerFactorization.of supplies the factorization of the positive reals under multiplication that calibrates the cost function, and PrimitiveDistinction.from reduces the seven axioms to four structural conditions plus definitional facts.
proof idea
The declaration is a structure definition. It simply packages the four fields (particle string, two real differences, and the disjunctive violation condition) with no tactics or term reduction.
why it matters
The structure supplies the concrete observables needed to test the CPT theorem stated in the module header. It closes the interface between the ledger symmetries (C from J-cost, P from D=3 isotropy, T from the eight-tick octave) and experimental bounds. No downstream theorems yet reference it, leaving open the question of how PDG limits translate into RS-native units via the Mass abbrev and NucleosynthesisTiers.of densities.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.