cert
plain-language theorem explainer
Packages three elementary domain-cost facts into a single CPT certificate: diagonal vanishing, nonnegativity for positive mass/energy, and a positive canonical threshold. Anyone citing the structural CPT theorem from J-cost will point here for the inhabited certificate. The construction is a pure structure instance wiring three sibling lemmas.
Claim. There is a CPT certificate whose three fields hold: for every nonzero real $r$, the domain cost of $(r,r)$ is zero; for all positive reals $m,e$, the domain cost of $(m,e)$ is nonnegative; and the canonical threshold is strictly positive.
background
The module treats CPT invariance as a structural theorem of Recognition Science: C is charge conjugation ($\sigma\mapsto -\sigma$), P is spatial reflection on the forced $D=3$ axes, and T is recognition-tick reversal. Combined CPT is identified with invariance of the J-cost under those three maps.
The certificate structure CPT3Cert packages the three numerical properties needed downstream: domain cost vanishes on the diagonal away from zero, is nonnegative on the positive quadrant, and the canonical threshold is positive. Domain cost is the RS cost functional restricted to the mass/energy domain used by the CPT argument; it inherits nonnegativity from the global J-cost (the unique cost forced by the Recognition Composition Law, $J(x)=(x+x^{-1})/2-1$).
Upstream, ObserverForcing already records that every recognition event has nonnegative cost via Jcost_nonneg. The present certificate specializes that fact to the domain-cost interface used by the CPT theorem.
proof idea
One-line structure instance. The three fields of the certificate are filled by the sibling lemmas domainCost_at_eq (diagonal vanishing), domainCost_nonneg (nonnegativity on positive arguments), and canonicalThreshold_pos (strict positivity of the threshold). No additional algebra is performed here.
why it matters
This is the inhabited certificate that turns the three domain-cost lemmas into a single object the CPT structural theorem can consume. The module is marked structural (zero sorry, zero axiom): CPT invariance is read as J-cost invariance under C, P, and T, sitting on the forcing chain after T5 (J-uniqueness) and T8 ($D=3$). With no downstream users yet recorded, the declaration is the local packaging step that closes the certificate interface for later CPT corollaries. It does not itself prove full CPT for QFT fields; it certifies the cost-side hypotheses those arguments need.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.