StructPhysicsM96Cert
plain-language theorem explainer
A certificate bundle for structural physics at recognition rung 96: diagonal domain cost vanishes, domain cost is nonnegative for positive arguments, and the canonical threshold is strictly positive. Downstream code cites it to inhabit the structural physics certificate and prove Nonempty. The declaration is a pure structure type; witnesses are supplied by sibling lemmas in the same module.
Claim. A structural physics certificate at rung 96 consists of three properties: (i) for every nonzero real $r$, the domain cost of $(r,r)$ is zero; (ii) for all positive reals $m,e$, the domain cost of $(m,e)$ is nonnegative; (iii) the canonical threshold is strictly positive.
background
Module Structural_Physics_mod96 packages a structural Recognition Science prediction for the Physics domain at recognition rung 96. Status is structural theorem: zero sorry, zero axiom. The local objects are a domain cost domainCost (a real-valued cost on pairs of reals, used as a physics-domain stand-in for recognition cost) and a canonicalThreshold (a fixed positive scale against which domain costs are compared).
Upstream, ObserverForcing records that every recognition event has nonnegative cost via the J-cost nonnegativity of Cost (0 ≤ e.cost from Jcost_nonneg on a positive state). The certificate fields mirror that nonnegativity and the identity minimum (cost zero on the diagonal) in the physics-domain specialization.
Rung 96 sits on the RS phi-ladder mass/yardstick hierarchy; the certificate does not re-derive the ladder, only the cost and threshold structural facts needed for the physics-domain structural claim.
proof idea
No proof body: this is a structure definition, not a theorem. The three fields are Prop-valued requirements. Inhabitation is deferred to the sibling cert, which fills them by domainCost_at_eq, domainCost_nonneg, and canonicalThreshold_pos. Those siblings are the actual proofs; this declaration only names the interface.
why it matters
Gives a single named bundle for the structural physics claim at mod-96 so downstream can treat "physics structural certificate holds" as one object. Used by cert (the concrete witness) and cert_inhabited (Nonempty StructPhysicsM96Cert), which close the module's structural theorem status.
In the RS forcing picture this is bookkeeping for the physics domain at a fixed rung, not a new step of T0–T8. It ties domain cost behavior to the same nonnegativity and identity-minimum pattern as the foundation J-cost (RCL / T5 uniqueness background), specialized to physics-domain arguments. No open scaffold: claim_status is definition; the inhabited certificate is already constructed in-module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.