cert_inhabited
plain-language theorem explainer
The structural certificate for Cosmology module 6 is inhabited: there exists a bundle asserting diagonal vanishing and nonnegativity of the domain cost together with positivity of the canonical threshold. Cosmology and forcing-chain readers cite it to discharge Nonempty obligations when wiring phi-uniqueness structure into larger developments. The proof is a one-line term that wraps the prebuilt 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) positivity of the canonical threshold, is nonempty.
background
Module RS_COS_Structural_006 is a structural cosmology unit on RS phi uniqueness: phi is the self-similar fixed point of the continued fraction $1+1/(1+1/(1+\cdots))$. Status is a closed structural theorem (no sorry, no axioms).
The certificate structure packages three facts about the local cost and threshold: domain cost vanishes when both arguments equal a nonzero real; domain cost is nonnegative on the positive quadrant; and the canonical threshold is strictly positive. Those three fields are the only content of the certificate type.
In the broader RS forcing chain, T6 forces phi as that self-similar fixed point. This module sits in the cosmology layer that records structural consequences of that uniqueness for cost and threshold data used downstream in cosmological bookkeeping.
proof idea
Term-mode one-liner. The module already defines a concrete value cert of type RSCOSStructural006Cert. The proof is the anonymous constructor ⟨cert⟩, which is the standard Lean witness that a type is nonempty. No tactics, no further lemmas.
why it matters
Gives a single Nonempty handle on the module-6 structural bundle so callers need not reopen the three component lemmas. In the Recognition framework it sits under the T6 phi-uniqueness landmark (self-similar fixed point) inside the cosmology structural series. No downstream uses are recorded in the graph yet; the declaration exists so later cosmology or forcing-chain theorems can assume the certificate without re-proving diagonal vanishing, nonnegativity, and threshold positivity. It closes the inhabitedness obligation for a zero-sorry structural module rather than advancing a new physical claim.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.