cert
plain-language theorem explainer
Packages the three structural physics properties at recognition rung 96 into one certificate: domain cost vanishes on the diagonal, is nonnegative for positive arguments, and the canonical threshold is positive. Cite when a downstream argument needs a single inhabited structural-physics certificate rather than the three lemmas separately. Construction is a pure structure assembly from three sibling proofs.
Claim. There is a structural physics certificate at recognition rung 96 whose three fields assert: (i) $\mathrm{domainCost}(r,r)=0$ for every real $r\neq 0$; (ii) $\mathrm{domainCost}(m,e)\ge 0$ whenever $m>0$ and $e>0$; (iii) the canonical threshold is strictly positive.
background
The module states a structural Recognition Science prediction for the Physics domain at recognition rung 96, with status structural theorem (zero sorry, zero axiom). The certificate type bundles three elementary cost and threshold facts that any such prediction must satisfy.
Domain cost is the local cost functional on pairs of positive reals used in this physics module; the diagonal identity $\mathrm{domainCost}(r,r)=0$ says matched measure and expectation carry zero cost. Nonnegativity for positive arguments is the physics-side shadow of the global fact that every recognition event has nonnegative cost (the upstream $J$-cost nonnegativity theorem). The canonical threshold is the positive cutoff against which domain cost is compared in structural checks.
The certificate structure is the interface: three named propositions, no extra data.
proof idea
One-line structure constructor. The three fields are filled by the sibling lemmas already proved in-module: diagonal vanishing of domain cost, nonnegativity of domain cost on positive pairs, and positivity of the canonical threshold. No new algebra is done here; the definition only witnesses that those three results inhabit the certificate type.
why it matters
Gives a single named inhabitant of the structural physics certificate at rung 96, so later arguments can depend on one object rather than three separate lemmas. Fits the module's role as a structural RS prediction for the Physics domain (Plan v7, 120th pass), with the cost side ultimately resting on $J$-cost nonnegativity from the observer-forcing layer. No downstream users are recorded yet; the natural consumer is any theorem that assumes an inhabited StructPhysicsM96Cert (including the sibling inhabitedness wrapper). Does not itself advance the T0–T8 forcing chain, but supplies the cost/threshold hygiene those physics-side structural claims need.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.