StructPhysicsM76Cert
plain-language theorem explainer
Certificate bundle for Recognition Science structural physics at rung 76. It packages three Prop fields: diagonal domain-cost vanishes off zero, domain-cost is nonnegative on positive pairs, and the canonical threshold is strictly positive. Downstream `cert` and `cert_inhabited` inhabit it. Pure structure definition; no proof body.
Claim. A structural physics certificate at recognition rung 76 is a record of three claims: (1) for every real $r \neq 0$, the domain cost of the pair $(r,r)$ equals $0$; (2) for all positive reals $m,e$, the domain cost of $(m,e)$ is nonnegative; (3) the canonical threshold is strictly positive.
background
Module Structural_Physics_mod76 is a Plan-v7 structural certificate for the Physics domain at recognition rung 76. Status is structural theorem material with zero sorry and zero axiom at the module level. The certificate is the type that packages the local claims.
Domain cost is the RS cost functional specialized to this physics domain (pairs of positive reals, typically mass/energy-style arguments). Its diagonal vanishing and nonnegativity mirror the global J-cost story: the Recognition Composition Law forces $J(x)=(x+x^{-1})/2-1$, minimized at the identity $x=1$ with $J\ge 0$. Upstream, ObserverForcing records that every recognition event has nonnegative cost via Cost.Jcost_nonneg.
The canonical threshold is the positive cutoff used by this module's structural prediction (sibling lemmas prove it is positive). The structure does not compute rung-76 numerics; it only names the three structural obligations.
proof idea
No proof: this is a structure declaration whose fields are propositions. Inhabitation is deferred. The sibling definition cert fills the three fields by domainCost_at_eq, domainCost_nonneg, and canonicalThreshold_pos. The theorem cert_inhabited then wraps that witness as Nonempty StructPhysicsM76Cert.
why it matters
Gives a single named type for the rung-76 physics structural obligations so downstream code can demand one certificate object rather than three loose lemmas. Immediate consumers are the module's own cert (the concrete witness) and cert_inhabited (nonemptiness). In the RS ledger this is the Physics-domain structural certificate at recognition rung 76, aligned with the cost-nonnegativity strand of the forcing chain (J-cost minimum and nonnegativity) rather than with T5–T8 uniqueness steps themselves. It does not close open mass-ladder or alpha-band numerics; it only standardizes the structural side conditions those predictions sit on.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.