cert_inhabited
plain-language theorem explainer
The fifth inflation-parameter certificate type is nonempty: a witness packs diagonal vanishing of the domain cost, its nonnegativity on positive arguments, and positivity of the canonical threshold. Cosmologists checking the RS n_s and tensor-to-scalar bounds cite this existence fact. The proof is a one-line term that exhibits the prebuilt certificate.
Claim. The set of inflation-parameter certificates is nonempty. Equivalently, there exists a triple of facts: the domain cost vanishes on the diagonal for every nonzero real $r$; the domain cost is nonnegative whenever both arguments are positive; and the canonical threshold is strictly positive.
background
Module Inflation_Parameters5 packages a structural certificate for RS inflation observables. Status is a structural theorem (zero sorry, zero axiom). Reported targets are $n_s = 0.9649$ with $r < 0.036$; RS gives $n_s = 1 - 2/45 = 0.9556$ (about $2.1\sigma$) and $r = 2/(45\varphi^2) \approx 0.0169$, which passes the $r$ cut and sits inside $3\sigma$ on $n_s$.
The certificate structure bundles three elementary cost properties: diagonal vanishing of domainCost off zero, nonnegativity of domainCost on the positive quadrant, and strict positivity of canonicalThreshold. Those three props are the only data the nonempty claim cares about; numerical $n_s$ and $r$ live in the surrounding module narrative, not in this type.
proof idea
One-line term proof. The module already constructs a concrete value cert : InflationParam5Cert. The theorem is the standard Lean inhabitation witness ⟨cert⟩, i.e. Nonempty.intro cert. No tactics, no further lemmas.
why it matters
Gives a machine-checkable existence token that the cost side-conditions used by the fifth inflation-parameter package are simultaneously satisfiable. Downstream consumers (none listed yet in the graph) can assume a certificate without rebuilding the three props. In the broader RS cosmology story this sits under the structural claim that RS predicts $n_s = 1-2/45$ and $r = 2/(45\varphi^2)$ inside current observational windows, tying the cost calculus (J-cost lineage via the Cost import) to inflation observables. It does not itself derive the spectral index or the tensor ratio; it only certifies the supporting cost inequalities.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.