CPT3Cert
plain-language theorem explainer
Packages the three analytic conditions that turn J-cost into a CPT certificate: domain cost vanishes on the diagonal, is nonnegative off it for positive arguments, and the canonical threshold is positive. Anyone citing the structural CPT theorem from J-cost will reference this bundle. It is a pure structure definition; inhabitants are built by wiring the sibling lemmas.
Claim. A CPT certificate is a triple of properties: (i) for every nonzero real $r$, the domain cost of the pair $(r,r)$ is zero; (ii) for all positive reals $m,e$, the domain cost of $(m,e)$ is nonnegative; (iii) the canonical threshold is strictly positive.
background
The module develops CPT invariance inside Recognition Science as a structural theorem with no sorry and no axioms. In RS language, C is charge conjugation ($\sigma \mapsto -\sigma$), P is spatial reflection on the forced $D=3$ axes, and T is reversal of the recognition tick; CPT is the claim that the J-cost is invariant under the combined action.
Domain cost is the real-valued cost assigned to a mass/energy (or measure/event) pair; the certificate asks that it vanish when the two arguments coincide and stay nonnegative when both are positive. The canonical threshold is the positive cutoff used to separate trivial from nontrivial recognition events. Upstream, nonnegativity of recognition-event cost is already known from ObserverForcing via $J$-cost nonnegativity on positive states.
proof idea
No proof body: this is a structure declaration. The three fields are Prop-valued requirements on domainCost and canonicalThreshold. Concrete inhabitants are assembled elsewhere by supplying the sibling lemmas domainCost_at_eq, domainCost_nonneg, and canonicalThreshold_pos.
why it matters
This is the interface type for the CPT-from-J-cost development. Downstream, cert builds a canonical inhabitant by wiring the three sibling lemmas, and cert_inhabited records Nonempty CPT3Cert. That inhabitation is the structural content of the module's CPT theorem: once domain cost (built from J-cost) meets diagonal vanishing, nonnegativity, and a positive threshold, the CPT package is certified. It sits in the Foundation layer that connects the forcing chain (T5 J-uniqueness, T8 $D=3$) to discrete symmetry statements without extra axioms.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.