cert
plain-language theorem explainer
Packages three elementary facts about the domain cost and the canonical threshold into a single certificate for structural module 4 (the RS gap-45 package). Anyone citing the D=3 minimum-rung self-reference claim can point at this bundle rather than the three lemmas separately. The body is a pure structure inhabitant: it wires already-proved equalities and inequalities into the certificate fields.
Claim. There is a certificate recording that (i) the domain cost vanishes on the diagonal: $\mathrm{domainCost}(r,r)=0$ for all $r\neq 0$; (ii) the domain cost is nonnegative for positive arguments: $0\le\mathrm{domainCost}(m,e)$ whenever $m>0$ and $e>0$; and (iii) the canonical threshold is strictly positive.
background
Module 4 is the structural package for the RS gap-45 identity $D^2(D+2)=9\cdot 5=45$, read as the minimum rung for stable self-reference once spatial dimension is fixed at $D=3$ (forcing chain T8). Status is structural: zero sorry, zero axiom.
The certificate type bundles three Prop-valued fields about a real bivariate cost domainCost and a positive real canonicalThreshold. The diagonal vanishing field says equal measure and expectation carry zero cost. Nonnegativity is the cost axiom for positive inputs. Threshold positivity keeps the gap cutoff strictly above zero.
Upstream, ObserverForcing already records that every recognition-event cost is nonnegative via the J-cost nonnegativity lemma (Cost.Jcost_nonneg). The present certificate is the module-local packaging of the analogous statements for domainCost.
proof idea
One-line structure inhabitant. The three fields are filled by the sibling lemmas domainCost_at_eq, domainCost_nonneg, and canonicalThreshold_pos respectively. No new algebra is performed; the definition only assembles those proofs into RSFDNStructural004Cert.
why it matters
Gives a single named witness that the gap-45 structural hypotheses hold, so downstream foundation material can depend on one object rather than three scattered lemmas. The module frames this as the minimum rung for stable self-reference at $D=3$, tying directly to forcing-chain T8 (three spatial dimensions) and the eight-tick octave context of the broader foundation. No used_by edges are recorded yet; the natural consumers are later structural or mass-ladder arguments that need a nonnegative diagonal-vanishing domain cost and a positive cutoff. Closes the certificate side of RS_FDN_Structural_004 without introducing axioms.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.