cert
plain-language theorem explainer
Packages three structural facts about the physics-domain recognition cost at rung 56 into a single certificate record: diagonal vanishing, non-negativity on positive arguments, and a strictly positive canonical threshold. Anyone citing the rung-56 structural physics prediction uses this inhabited certificate. The body is a pure field assembly of three already-proved sibling lemmas.
Claim. There is a structural physics certificate at recognition rung 56 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
Module status is a structural theorem for the Physics domain at recognition rung 56 (Plan v7, 120th pass): zero sorry, zero axiom. The certificate type bundles three Prop-valued fields that any valid domain-cost model must satisfy.
Domain cost is the local cost functional on pairs of positive reals used for this physics rung; on the diagonal it must vanish (perfect match costs nothing), and off-diagonal it must stay non-negative. The canonical threshold is the positive cutoff against which domain-cost comparisons are judged.
Upstream, non-negativity of recognition-event cost is already forced in ObserverForcing via the J-cost: "The cost of any recognition event is non-negative," proved from $J$-cost non-negativity at positive state. The present certificate lifts that discipline to the physics-domain cost pair $(m,e)$.
proof idea
One-line structure inhabitant. Each field of StructPhysicsM56Cert is filled by the matching sibling lemma: diagonal vanishing by domainCost_at_eq, non-negativity by domainCost_nonneg, and threshold positivity by canonicalThreshold_pos. No extra tactics or algebraic work; the def is pure record assembly.
why it matters
This is the inhabited structural certificate for Physics at rung 56. Downstream consumers (none yet wired in the graph) and the sibling cert_inhabited treat it as the single object proving the module's structural claim is realized. It sits in the physics branch of the Recognition forcing stack: cost non-negativity traces to the J-cost uniqueness chain (T5), while the rung index 56 is a concrete step on the phi-ladder mass/yardstick hierarchy. Closing this certificate keeps the module's "0 sorry, 0 axiom" structural status honest.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.