cert
plain-language theorem explainer
Packages three structural facts for the physics-domain cost at recognition rung 76 into one certificate: diagonal vanishing, nonnegativity on positive arguments, and a positive canonical threshold. Cited wherever a single witness that the physics cost structure is well-formed is needed. Assembled by filling the three structure fields from prior local lemmas.
Claim. There is a structural physics certificate at recognition rung 76 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 records a structural Recognition Science prediction for the Physics domain at recognition rung 76 (Plan v7, 120th pass). Status is a structural theorem: zero sorry, zero axioms.
The certificate type bundles three properties of a domain cost functional on positive reals. Domain cost is the local cost comparison used in the physics structural layer; it is expected to vanish on the diagonal (equal arguments) and stay nonnegative off it, mirroring the global J-cost nonnegativity from ObserverForcing (cost_nonneg: the cost of any recognition event is non-negative).
The third field asserts positivity of the module's canonical threshold, the cutoff against which structural cost comparisons are judged at this rung.
proof idea
One-line structure instance. The three fields of StructPhysicsM76Cert are filled by the sibling lemmas domainCost_at_eq (diagonal vanishing), domainCost_nonneg (nonnegativity for positive arguments), and canonicalThreshold_pos (strict positivity of the threshold). No further reasoning; pure packaging of already-proved facts.
why it matters
Gives a single named witness that the physics-domain cost structure at rung 76 is well-formed: zero on equal nonzero arguments, nonnegative for positive mass/energy, and gated by a positive threshold. That is the structural content the module advertises as a 0-sorry RS prediction for Physics.
No downstream consumers are recorded yet; the sibling cert_inhabited is the natural next step (inhabitation of the certificate type). In the broader framework this sits with the cost layer built on J-cost nonnegativity and the rung/ladder organization of structural physics claims, not with the T0–T8 forcing chain itself.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.