InflatonMass3Cert
plain-language theorem explainer
Certificate packing three structural properties used by the RS inflaton-mass argument: diagonal domain cost vanishes off zero, domain cost is nonnegative for positive mass and energy, and the canonical threshold is positive. Cosmology modules that inhabit the phi-ladder mass scale cite this bundle. It is a pure structure definition; the inhabitant wires the sibling lemmas.
Claim. A certificate consists of three facts: for every nonzero real $r$, the domain cost of $(r,r)$ is zero; for all positive reals $m,e$, the domain cost of $(m,e)$ is nonnegative; and the canonical threshold is strictly positive.
background
The module treats the inflaton mass as a structural output of the phi-ladder: $m_{\mathrm{inflaton}} = \varphi^k E_{\mathrm{coh}}$. With $E_{\mathrm{coh}} \approx 0.121,\mathrm{MeV}$ and rung $k \approx 57$, the scale lands near $10^{13},\mathrm{GeV}$ (the usual slow-roll window). Status is structural: zero sorry, zero axiom.
Domain cost is the local cost functional on mass/energy pairs used in this cosmology file (siblings prove it vanishes on the diagonal and is nonnegative). Canonical threshold is the positive cutoff against which that cost is compared. Upstream, recognition-event cost is already known nonnegative via $J$-cost nonnegativity on positive states (cost_nonneg in ObserverForcing).
proof idea
No proof body: this is a structure whose fields are propositions. Downstream cert fills the three fields by the sibling lemmas domainCost_at_eq, domainCost_nonneg, and canonicalThreshold_pos. cert_inhabited then packages ⟨cert⟩ as Nonempty.
why it matters
Gives a single named interface for the cost/threshold side conditions of the inflaton-mass-from-phi-ladder claim. Parents are cert (the concrete inhabitant) and cert_inhabited (nonemptiness). That closes the structural half of Plan v7 pass 116: mass as $\varphi^k E_{\mathrm{coh}}$ on the ladder, without numerical floating-point claims inside Lean. Ties to the broader RS mass formula (yardstick times $\varphi^{\mathrm{rung}-8+\mathrm{gap}(Z)}$) and to $J$-cost nonnegativity from the forcing chain, while remaining a thin certificate rather than a full inflationary dynamics derivation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.