RSSTDStructural004Cert
plain-language theorem explainer
Certificate bundle for Standard Model structural module 4 (gap-45 at D=3): domain cost vanishes on equal nonzero arguments, is nonnegative for positive mass/energy pairs, and the canonical threshold is strictly positive. Downstream code builds a concrete inhabited instance. Pure structure definition packaging three Prop fields; no proof body.
Claim. A certificate is a triple of properties: (i) for every real $r \neq 0$, the domain cost at $(r,r)$ equals $0$; (ii) for all reals $m,e > 0$, the domain cost at $(m,e)$ is nonnegative; (iii) the canonical threshold is strictly positive.
background
Module RS_STD_Structural_004 treats the Recognition Science gap-45 identity $D^2(D+2)=9\cdot 5=45$ at spatial dimension $D=3$, described as the minimum rung for stable self-reference. Status is structural (zero sorry, zero axiom).
The certificate packages three elementary cost facts used in that setting. Domain cost is the real-valued cost assigned to a mass/energy pair $(m,e)$; the diagonal clause says equal nonzero arguments sit at zero cost. The canonical threshold is a fixed positive real used as a comparison scale in the module.
Upstream, ObserverForcing records that every recognition-event cost is nonnegative via the J-cost nonnegativity lemma (Cost.Jcost_nonneg on a positive state). The present fields are the domain-level analogues of that nonnegativity and of the identity minimum at equal arguments.
proof idea
No proof: this is a structure declaration whose three fields are propositions. Inhabitation is deferred to the sibling cert, which fills the fields by domainCost_at_eq, domainCost_nonneg, and canonicalThreshold_pos, and to cert_inhabited, which wraps that instance as Nonempty.
why it matters
Gives a single named type for the structural obligations of Standard Model module 4 so downstream code can demand or supply them uniformly. Used by the concrete cert instance and by cert_inhabited : Nonempty RSSTDStructural004Cert, which close the module's certificate interface.
In the RS forcing picture this sits under the D=3 landmark (T8) and the gap-45 count $D^2(D+2)=45$ as the minimum rung for stable self-reference. It does not itself derive the gap identity; it only packages the cost and threshold side-conditions the structural story relies on.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.