cert_inhabited
plain-language theorem explainer
The first cosmology structural certificate is inhabited: a witness exists packing diagonal vanishing of domain cost, nonnegativity for positive arguments, and positivity of the canonical threshold. Cosmology auditors cite it to confirm the certificate type is realizable inside the RS structural stack. The proof is a one-line term injecting the concrete certificate value.
Claim. The type of structural certificates is nonempty: there exists a witness 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) the canonical threshold is strictly positive.
background
This module records the first RS structural cosmology package: the cost is the standard J-form $J(x)=\frac12(x+1/x)-1$, $\varphi$ is the golden ratio, and $D=3$ is forced. Status is a pure structural theorem (zero sorry, zero axiom).
The certificate structure bundles three elementary facts about the local domain cost and threshold. Domain cost vanishes on the diagonal for nonzero real arguments, stays nonnegative when both mass-like and energy-like inputs are positive, and the canonical threshold used as a cutoff is strictly positive.
Those three fields are exactly the content of the certificate type; inhabitation means a concrete Lean value already discharges all three simultaneously.
proof idea
One-line term proof. The concrete certificate value already constructed in-module is injected as the witness for Nonempty, via the standard constructor ⟨cert⟩. No further rewriting or case analysis is required.
why it matters
Inhabitation closes the certificate layer of Cosmology Structural Module 1. Downstream consumers that demand a nonempty certificate (rather than an open Prop) can now import a realized witness without re-proving diagonal vanishing, nonnegativity, or threshold positivity.
Framework-wise this sits under the structural forcing chain: T5 uniqueness of $J(x)=\frac12(x+x^{-1})-1$, T6 forcing of $\varphi$, and T8 forcing of $D=3$. The module header advertises exactly those landmarks. No open scaffolding remains here; the certificate is fully discharged.
No parent theorems currently list this declaration as a dependency, so its role is local completeness of the structural package rather than a stepping stone in a longer proof chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.