cert_inhabited
plain-language theorem explainer
The structural certificate for RS module 8 (rung spacing by factor φ) is inhabited: domain cost vanishes on equal nonzero arguments, is nonnegative on positive reals, and the canonical threshold is positive. Foundation authors cite this to discharge Nonempty obligations when wiring the certificate into larger forcing or mass-ladder arguments. Proof is a one-line term witness: the concrete value cert.
Claim. There exists a certificate packing three facts: (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 RS_FDN_Structural_008 packages the structural claim that adjacent RS rungs are separated by the golden ratio factor $\phi \approx 1.618$. Status is a pure structural theorem (zero sorry, zero axiom).
The certificate structure bundles three elementary properties of the local cost and threshold: diagonal vanishing of domain cost on nonzero reals, nonnegativity of domain cost on the positive quadrant, and positivity of the canonical threshold. Domain cost is the module-local cost functional (imported from Cost/Constants) used to score mismatch between a measured rung coordinate and an expected one on the $\phi$-ladder.
Upstream, the structure type itself only declares the three fields; inhabitance is what turns the interface into a usable witness for later foundation wiring.
proof idea
One-line term proof. The theorem goal is Nonempty RSFDNStructural008Cert. The proof supplies the already-constructed value cert as the witness via the anonymous constructor ⟨cert⟩, which is definitionally a term of type Nonempty _. No tactics, no rewriting, no further lemmas.
why it matters
Closes the inhabitance obligation for Foundation structural module 8, the rung-spacing package tied to $\phi$ as the self-similar fixed point (forcing landmark T6). Downstream use list is empty in the current graph, so this is a leaf certificate: it exists so that any later theorem needing a packaged proof of diagonal vanishing, cost nonnegativity, and threshold positivity can take a Nonempty hypothesis or Classical.choice without re-proving the three fields.
In the broader RS ledger this sits with the other FDN structural certificates that keep the forcing chain and mass-ladder scaffolding free of sorry. It does not itself derive $\phi$ or the eight-tick octave; it only certifies the local cost/threshold facts assumed when those landmarks are applied to rung geometry.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.