cert_inhabited
plain-language theorem explainer
The structural certificate for RS gap-45 is inhabited: domain cost vanishes on the diagonal, is nonnegative for positive arguments, and the canonical threshold is positive. Cite this when packaging the three gap-45 structural facts as a single Nonempty witness. The proof is a one-line term that feeds the bundled cert into the structure constructor.
Claim. There exists a certificate packing three structural facts: for every nonzero real $r$, the domain cost of $(r,r)$ is zero; for all positive reals $m,e$, the domain cost of $(m,e)$ is nonnegative; and the canonical threshold is strictly positive.
background
Module RS_FDN_Structural_004 records the gap-45 structural theorem: $D^2(D+2)=9\cdot 5=45$, the minimum rung for stable self-reference at spatial dimension $D=3$. Status is a pure structural theorem (no sorry, no axiom).
The certificate structure bundles three properties of the local domain cost and threshold. Domain cost is the cost functional restricted to the mass-energy pair used in this module; on the diagonal it must vanish for nonzero equal arguments, and it must stay nonnegative when both arguments are positive. The canonical threshold is the positive cutoff tied to that cost geometry.
Upstream, the structure type itself only declares those three fields. Sibling lemmas in the module establish each field separately; this declaration only asserts that a full inhabitant exists.
proof idea
Term-mode one-liner. The proof supplies the already-constructed value cert as the unique field of Nonempty RSFDNStructural004Cert, written ⟨cert⟩. No tactics, no further lemmas: inhabitance is immediate from the bundled certificate object defined earlier in the module.
why it matters
Gap-45 is the RS landmark for the lowest rung at which self-reference is stable in $D=3$ (from the forcing chain, T8 forces three spatial dimensions; the octave and phi-ladder sit upstream). Packaging the three cost/threshold facts into a single Nonempty certificate lets downstream foundation code treat the structural package as one hypothesis rather than three separate lemmas.
No used-by edges are recorded yet, so this is presently a leaf witness inside the structural-004 module. It closes the inhabitance obligation for the certificate type and keeps the module at zero sorry. Anyone assembling a larger foundation certificate chain that requires gap-45 cost geometry would import this Nonempty fact.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.