cert
plain-language theorem explainer
Packages three proved properties of the inflation domain cost (vanishes on the diagonal, is nonnegative off the axes, and has a positive canonical threshold) into a single certificate record. Cosmologists citing the RS inflation-parameter session use this object as the structural witness that the cost setup is well-formed. The body is a pure structure constructor wiring three sibling lemmas.
Claim. There is a certificate for the RS inflation-parameter cost setup consisting of: (i) $\mathrm{domainCost}(r,r)=0$ for all $r\neq 0$; (ii) $\mathrm{domainCost}(m,e)\ge 0$ whenever $m>0$ and $e>0$; (iii) the canonical threshold is strictly positive.
background
This module is the absolute-final RS inflation-parameters session. It records the structural side of the comparison $n_s=1-2/45\approx 0.9556$ (about $2.1\sigma$ from the observational $0.9649$) and $r=2/(45\varphi^2)\approx 0.0169<0.036$, with an RS_PASS on $r$ and on $n_s$ inside $3\sigma$.
The certificate structure bundles three cost axioms used throughout that comparison. The domain cost is the local cost functional on positive mass/energy-like coordinates; its diagonal vanishing and off-axis nonnegativity mirror the global J-cost nonnegativity from ObserverForcing ("the cost of any recognition event is non-negative"), specialized to the inflation domain. The canonical threshold is the positive cutoff against which the domain cost is compared when scoring the parameter point.
proof idea
One-line structure construction. The three fields of InflationParam5Cert are filled by the already-proved sibling lemmas domainCost_at_eq, domainCost_nonneg, and canonicalThreshold_pos. No additional algebra is performed; the definition is pure packaging.
why it matters
Gives a single inhabited certificate that the inflation domain-cost setup is structurally sound (zero diagonal cost, nonnegative cost, positive threshold). The module status line marks the whole session as a structural theorem with 0 sorry and 0 axioms; this definition is the named witness object for that claim. Downstream, cert_inhabited and any consumer that needs an InflationParam5Cert instance can point here rather than re-proving the three properties. It does not itself derive $n_s$ or $r$; those numerical RS predictions sit in the module narrative and use the cost apparatus this certificate legitimates. Framework context: cost nonnegativity is the same J-cost positivity that appears in the forcing chain and ObserverForcing, specialized to cosmology.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.