cert
plain-language theorem explainer
Packages three structural facts about the domain cost and the canonical threshold into a single AllPhysics5 certificate. Anyone citing the zero-parameter AllPhysics5 structural claim uses this object as the inhabited witness. The body is a pure structure instance: three already-proved sibling lemmas are wired into the three fields.
Claim. There is a certificate recording that (i) the domain cost vanishes on the diagonal, $\mathrm{domainCost}(r,r)=0$ for every $r\neq 0$; (ii) the domain cost is nonnegative for positive mass and energy arguments; and (iii) the canonical threshold is strictly positive.
background
The module AllPhysics5 is the absolute final session of the Recognition Science foundation: a structural theorem (zero sorry, zero axiom) asserting that gravity, electromagnetism, weak and strong sectors, Higgs data, matter masses, and cosmology all descend from the single cost $J(x)$, with no free parameters.
The certificate structure bundles three elementary properties of the local domain cost (the cost comparing mass and energy scales) and of the canonical threshold used to gate recognition events. Domain cost on the diagonal is zero away from the origin; it is nonnegative on the positive orthant; and the threshold that separates sub-threshold from above-threshold events is positive.
Upstream, nonnegativity of recognition-event cost is already known from ObserverForcing: every recognition event has cost at least zero because $J$ itself is nonnegative on the positive reals. The present certificate lifts that style of fact to the domain-cost and threshold layer used by AllPhysics5.
proof idea
One-line structure instance. The three fields of the certificate are filled by the three sibling lemmas already proved in the same module: diagonal vanishing of domain cost, nonnegativity of domain cost on positive arguments, and positivity of the canonical threshold. No new calculation occurs; the definition only packages those lemmas under a single name.
why it matters
AllPhysics5 claims the entire physical content of Recognition Science from $J(x)$ alone (Lambda and GR, alpha and the photon, weak mixing and $W/Z$, strong coupling as $J(\phi)$ with confinement, Higgs mass and VEV, the full mass ladder, and cosmological parameters). The certificate is the inhabited structural witness that the cost and threshold layer used by that claim is well-formed.
It sits next to the inhabitedness lemma for the same certificate type and is the natural object any downstream AllPhysics5 consumer would open. Framework landmarks in view are T5 ($J$-uniqueness), the Recognition Composition Law, and the zero-parameter stance of the forcing chain. No open scaffold remains here: the module status is structural with zero sorry.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.