cert_inhabited
plain-language theorem explainer
The certificate bundling diagonal vanishing of domain cost, its nonnegativity on positive arguments, and positivity of the canonical threshold is inhabited. Anyone packaging Foundation structural module 9 cites this existence fact. The proof is a one-line term witness: the already-constructed certificate instance.
Claim. There exists a certificate whose three fields assert: (i) the domain cost of any nonzero real against itself is zero; (ii) for positive reals $m,e$ the domain cost is nonnegative; (iii) the canonical threshold is strictly positive.
background
Module RS_FDN_Structural_009 sits in the Foundation forcing chain (T5 J-uniqueness through T8, $D=3$). It packages three elementary structural facts about a domain cost and a canonical threshold into a single certificate structure.
The structure RSFDNStructural009Cert has three fields: diagonal vanishing of domain cost on nonzero reals; nonnegativity of domain cost for positive measure and energy arguments; and strict positivity of the canonical threshold. Sibling lemmas in the same module establish each field separately and assemble them into a concrete certificate value.
Nonempty is the standard Mathlib existence type: a proof of Nonempty C is exactly a witness of type C.
proof idea
One-line term proof. The module already builds a concrete certificate cert : RSFDNStructural009Cert from the three sibling lemmas (diagonal vanishing, nonnegativity, threshold positivity). The theorem simply wraps that value as ⟨cert⟩, which is the canonical constructor of Nonempty.
why it matters
This is the existence seal for Foundation structural module 9. The module doc places it on the RS forcing chain T5 (J-uniqueness) → T6 (φ forced) → T7 (eight-tick octave) → T8 ($D=3$), and marks the file as a structural theorem with zero sorry and zero axioms. Downstream consumers that need a single inhabited certificate rather than three separate lemmas can depend on this fact. No further used-by edges are recorded yet; the declaration closes the module's public interface.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.