cert
plain-language theorem explainer
Packages three structural facts for the Physics domain at recognition rung 86 into one certificate record: domain cost vanishes on the diagonal, is nonnegative for positive arguments, and the canonical threshold is positive. Cite when a single inhabited certificate object is needed rather than the three lemmas separately. Construction is a structure literal that wires three already-proved sibling lemmas into the fields.
Claim. There is a structural physics certificate at recognition rung 86 consisting of three facts: (i) for every real $r \neq 0$, the domain cost of $(r,r)$ is zero; (ii) for all $m,e > 0$, the domain cost of $(m,e)$ is nonnegative; (iii) the canonical threshold is strictly positive.
background
This module records a structural Recognition Science prediction for the Physics domain at recognition rung 86. The module status is a closed structural theorem: zero sorry, zero axioms.
The certificate type is a three-field structure. The first field asserts that the domain cost vanishes on the diagonal away from zero (equal measure and equal energy give zero cost). The second asserts nonnegativity of domain cost for positive measure and energy. The third asserts that the canonical threshold used as a comparison scale is strictly positive.
Upstream, nonnegativity of recognition cost is already known in ObserverForcing: "The cost of any recognition event is non-negative," via the J-cost minimum. Here the analogous nonnegativity is specialized to the Physics-domain cost function and packaged with the diagonal and threshold facts.
proof idea
Pure structure construction, not a tactic proof. The definition is a StructPhysicsM86Cert literal whose three fields are filled by the sibling lemmas domainCost_at_eq, domainCost_nonneg, and canonicalThreshold_pos. No further rewriting or case analysis occurs at this site.
why it matters
Gives a single named inhabitant of the Physics rung-86 structural certificate so downstream code can depend on one object rather than three separate lemmas. The module frames this as a structural RS prediction for the Physics domain at recognition rung 86, in the Plan v7 structural-certificate series.
No used_by edges are recorded yet; the immediate sibling cert_inhabited is the natural consumer, witnessing that the certificate type is nonempty. Within the broader framework this sits in the Physics domain layer that rests on the J-cost and forcing chain (T5 J-uniqueness and related cost nonnegativity), not on a new dynamical law.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.