cert
plain-language theorem explainer
Packages three structural facts for the Physics domain at recognition rung 36 into one certificate: domain cost vanishes on the diagonal, is nonnegative for positive mass/energy arguments, and the canonical threshold is positive. Anyone needing an inhabited Physics-mod-36 structural certificate cites this witness. The body is pure field assembly from three sibling lemmas.
Claim. There is a structural Physics certificate at recognition rung 36 consisting of: (i) $\mathrm{domainCost}(r,r)=0$ for all $r\neq 0$; (ii) $\mathrm{domainCost}(m,e)\ge 0$ whenever $m>0$ and $e>0$; (iii) the canonical threshold is strictly positive.
background
This module states a structural Recognition Science prediction for the Physics domain at recognition rung 36 (Plan v7, 120th pass). Status is a structural theorem: zero sorry, zero axioms.
The certificate structure asks for three properties of the local domain cost and threshold. Domain cost is the Physics-side cost functional on pairs of real arguments (mass/energy style); the diagonal condition says equal arguments incur zero cost, matching the J-cost minimum at identity. Nonnegativity mirrors the global fact that recognition-event cost is nonnegative (from ObserverForcing via $J$-cost nonnegativity). The canonical threshold is the positive cutoff used for the structural pass/fail test at this rung.
Upstream, cost_nonneg on recognition events records that every event cost is $\ge 0$ because $J$ is nonnegative on positive states. Here the analogous nonnegativity is specialized to the Physics domain cost.
proof idea
Definitional construction of the certificate structure. Each field is filled by a named sibling lemma already proved in-module: diagonal vanishing by the domain-cost-at-equality lemma, nonnegativity by the domain-cost-nonnegativity lemma, and strict positivity of the threshold by the canonical-threshold-positivity lemma. No extra tactics or algebraic work; pure structure inhabitation.
why it matters
Gives a single named witness that the Physics structural certificate at rung 36 is inhabited, which is the module's stated deliverable (structural RS prediction, 0 sorry / 0 axiom). Downstream use list is empty in the graph, so this is a terminal packaging object rather than a lemma in a longer chain; the sibling cert_inhabited is the natural consumer.
In the broader framework it sits in the Physics domain layer that applies forced cost structure (J-uniqueness / T5, nonnegative recognition cost) to a concrete rung. It does not itself force $\varphi$, the eight-tick octave, or $D=3$; it only certifies the local cost/threshold package at mod 36.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.