RSFDNStructural004Cert
plain-language theorem explainer
Certificate bundle for RS structural module 4 (gap-45): diagonal domain cost vanishes, domain cost is nonnegative on positive arguments, and the canonical threshold is strictly positive. Anyone citing the gap-45 self-reference floor at D=3 uses this as the typed witness. It is a pure structure definition; inhabitation is discharged downstream by packing three sibling lemmas.
Claim. A structural certificate for gap-45 consists of three properties: (i) for every nonzero real $r$, the domain cost of the matched pair $(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 RS_FDN_Structural_004 packages the gap-45 structural claim: $D^2(D+2)=9\cdot 5=45$ is the minimum rung for stable self-reference in $D=3$. Status is structural (zero sorry, zero axiom).
The certificate fields refer to two local quantities. Domain cost is a real-valued cost on a pair of positive reals (measure and energy style arguments); the diagonal identity says matched arguments cost nothing. The canonical threshold is a fixed positive real used as the comparison scale for that cost. Upstream, ObserverForcing already records that every recognition-event cost is nonnegative via $J$-cost nonnegativity (Cost.Jcost_nonneg), which is the same nonnegativity pattern this certificate re-exports at the domain-cost level.
proof idea
No proof body: this is a structure whose three fields are propositions. Inhabitation is not proved here. The sibling definition cert fills the fields by direct assignment of domainCost_at_eq, domainCost_nonneg, and canonicalThreshold_pos. The theorem cert_inhabited then wraps that value as Nonempty.
why it matters
This declaration is the typed interface for structural module 4. Downstream, cert builds a concrete inhabitant and cert_inhabited records nonemptiness, so later foundation code can depend on a single certificate object rather than three loose lemmas.
In the Recognition forcing chain the module sits at the D=3 self-reference floor (T8 forces three spatial dimensions; gap-45 is the stated minimum rung $D^2(D+2)$ for stable self-reference). The cost fields echo the J-cost minimum and nonnegativity pattern from T5/RCL, specialized to the domain-cost presentation used in this structural layer. It closes no open physics claim by itself; it standardizes the witness that the gap-45 package is fully discharged.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.