cert_inhabited
plain-language theorem explainer
The module-5 forcing-chain certificate is inhabited: the three packed properties (diagonal vanishing of domain cost, nonnegativity for positive arguments, and positivity of the canonical threshold) hold simultaneously. Anyone citing structural completeness of this cost/threshold package would use it. The proof is a one-line term witness from the concrete certificate value.
Claim. The type of certificates packing (i) $\mathrm{domainCost}(r,r)=0$ for all $r\neq 0$, (ii) $\mathrm{domainCost}(m,e)\ge 0$ whenever $m>0$ and $e>0$, and (iii) $\mathrm{canonicalThreshold}>0$, is nonempty.
background
Module 5 sits in the RS forcing-chain series (T0–T8), whose structural theorems are claimed complete in Lean with zero sorry and zero extra axioms. The local certificate structure packages three elementary facts about a real bivariate cost and a fixed positive threshold.
domainCost is the module’s cost on pairs of reals (imported cost infrastructure plus local definitions). The first field requires that cost vanish on the diagonal away from zero; the second that it be nonnegative on the positive quadrant. canonicalThreshold is a named positive real constant of the module; the third field is simply its positivity.
Upstream, the structure itself is only a Prop-carrying record: inhabitation is the theorem that turns the three sibling lemmas into a single witness.
proof idea
Term-mode one-liner. The concrete value cert (built elsewhere in the module from the three sibling proofs of diagonal vanishing, nonnegativity, and threshold positivity) is supplied as the witness of Nonempty, via the standard constructor ⟨cert⟩. No further rewriting or case analysis.
why it matters
Gives a single inhabited certificate object for module 5 of the RS forcing chain, so downstream consumers can depend on one Nonempty fact rather than three separate lemmas. The module doc frames the whole file as part of the T0–T8 structural spine (J-uniqueness through D=3) with zero sorry. No used_by edges are recorded yet; the declaration is the terminal packaging step of this file rather than a lemma consumed elsewhere in the graph.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.