cert
plain-language theorem explainer
Packages three elementary facts about the domain cost and the canonical threshold into a single certificate for RS structural module 4 (gap-45). Anyone citing the D=3 minimum-rung self-reference result uses this bundle. The definition is a pure structure assembly: three already-proved sibling lemmas fill the certificate fields.
Claim. There is a certificate asserting: (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 4 records the RS gap-45 identity $D^2(D+2)=9\cdot 5=45$, the minimum rung for stable self-reference once spatial dimension is fixed at $D=3$ (forcing chain T8). Status is structural: zero sorry, zero axioms.
The certificate structure demands three properties of a real-valued domain cost and a positive threshold. Domain cost is the local cost functional on measurement/expectation pairs; on the diagonal it must vanish (perfect match costs nothing), and off-diagonal it stays nonnegative. The canonical threshold is the positive cutoff used to mark the gap-45 rung.
Upstream, nonnegativity of recognition cost is already known from ObserverForcing: every recognition event has $J$-cost $\ge 0$, with the identity event at the $J$-minimum $x=1$. The three field lemmas in this module specialize that picture to domain cost and the threshold.
proof idea
Pure structure construction, not a tactic proof. The three fields of RSMTHStructural004Cert are filled by the sibling lemmas domainCost_at_eq (diagonal vanishing), domainCost_nonneg (nonnegativity for positive arguments), and canonicalThreshold_pos (strict positivity of the threshold). No further rewriting or case analysis occurs.
why it matters
This certificate is the packaged witness that the gap-45 structural facts hold: domain cost behaves like a genuine cost (zero on match, nonnegative otherwise) and the canonical threshold is a positive scale. It sits inside the Mathematics structural line that records $D^2(D+2)=45$ 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.
No downstream consumers are wired yet in the graph, so the certificate presently serves as the module-level inhabitance witness (paired with cert_inhabited). It closes the structural side of gap-45 without introducing axioms or sorry.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.