cert_inhabited
plain-language theorem explainer
The structural certificate packing three elementary domain-cost and threshold facts is nonempty. Anyone citing the RS mathematics structural pack for module 9 uses this as the existence witness. The proof is a one-line term that packages the already-built certificate value.
Claim. There exists a certificate asserting: (i) the domain cost vanishes on the diagonal, $C(r,r)=0$ for all $r\neq 0$; (ii) $C(m,e)\ge 0$ whenever $m>0$ and $e>0$; (iii) the canonical threshold is strictly positive.
background
Module RS_MTH_Structural_009 sits in the mathematics layer of the Recognition Science forcing chain (T5 J-uniqueness through T8 forcing $D=3$). It packages elementary positivity and normalization facts about a domain cost $C$ and a canonical threshold used downstream in structural arguments.
The certificate structure bundles three propositions: diagonal vanishing of domain cost for nonzero reals, nonnegativity of domain cost on the positive quadrant, and positivity of the canonical threshold. Sibling lemmas in the module establish each field separately; the structure is only a packaging type.
Local status is a structural theorem with zero sorry and zero axioms, importing Mathlib together with the RS Constants and Cost modules.
proof idea
Term-mode one-liner. The module already constructs a concrete value cert of type RSMTHStructural009Cert whose three fields are filled by the sibling lemmas on diagonal vanishing, nonnegativity, and threshold positivity. The proof is simply the anonymous constructor ⟨cert⟩, which is the standard Lean witness for Nonempty.
why it matters
Gives a single inhabited certificate object for the three elementary cost/threshold facts of structural module 9. In the RS forcing narrative this module is tagged against the chain T5 (J-uniqueness) through T8 ($D=3$), so the pack is meant as a reusable structural handle rather than a deep new identity.
No downstream consumers are recorded in the graph yet; the declaration exists so later structural or physics lemmas can assume one object instead of three separate hypotheses. It closes the existence side of the module's certificate interface without adding axioms.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.