InflationParam5Cert
plain-language theorem explainer
Certificate packing three structural properties of the inflation-parameter domain cost: it vanishes on the equal-argument diagonal for nonzero reals, stays nonnegative for positive mass and energy arguments, and the canonical threshold is strictly positive. Cosmology code cites the inhabited instance when discharging RS inflation checks on n_s and r. Pure structure definition; no proof body.
Claim. A record of three facts: (i) for every nonzero real $r$, the domain cost of the pair $(r,r)$ is zero; (ii) for all positive reals $m$ and $e$, the domain cost of $(m,e)$ is nonnegative; (iii) the canonical threshold is strictly positive.
background
The module packages RS inflation parameters as a structural theorem block (zero sorry, zero axiom). Target observables are the scalar spectral index $n_s$ and the tensor-to-scalar ratio $r$. The status note records observed $n_s \approx 0.9649$ with $r < 0.036$, against RS predictions $n_s = 1-2/45 = 0.9556$ (about 2.1 sigma) and $r = 2/(45\phi^2) \approx 0.0169$.
Domain cost is the local cost on mass-energy pairs that gates the inflation-parameter regime. The canonical threshold is the positive cutoff used with that cost. Upstream, any recognition-event cost is nonnegative because J-cost is nonnegative on positive states (ObserverForcing.cost_nonneg).
proof idea
No proof: this is a structure whose fields are Prop-valued requirements. Inhabitation is supplied by the sibling definition that fills the three fields with domainCost_at_eq, domainCost_nonneg, and canonicalThreshold_pos. Nonemptiness is then a one-constructor theorem wrapping that inhabitant.
why it matters
Gives the typed certificate that cert and cert_inhabited inhabit, closing the structural side of Inflation_Parameters5. That package underwrites the module's RS_PASS claim on $r$ and the 2.1-sigma $n_s$ comparison. Cost nonnegativity ties back to the J-cost minimum used throughout the forcing chain; the certificate itself does not re-derive $\phi$, the eight-tick octave, or $D=3$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.