cert
plain-language theorem explainer
Certificate that the inflaton domain cost vanishes on the diagonal, stays nonnegative for positive mass and energy, and that the canonical threshold is positive. Cosmologists citing the RS phi-ladder mass for the inflaton (~10^13 GeV) use this as the inhabited structural witness. Proof is a structure instance wiring three local lemmas.
Claim. There is a certificate asserting: the domain cost $C$ satisfies $C(r,r)=0$ for every $r\neq 0$; $C(m,e)\geq 0$ whenever $m>0$ and $e>0$; and the canonical threshold $T$ obeys $T>0$.
background
The module treats the inflaton mass as a structural consequence of the Recognition Science 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 product lands near $10^{13},\mathrm{GeV}$, the standard inflationary scale. Status is structural (zero sorry, zero axiom).
The certificate structure packages three elementary properties of a domain cost $C(m,e)$ on positive reals: diagonal vanishing (zero self-cost), nonnegativity, and a strictly positive canonical threshold. Nonnegativity of recognition cost is the global RS fact that $J$-cost is nonnegative on positive states (ObserverForcing), specialized here to the cosmology domain cost.
Sibling lemmas supply the three fields: equality of domain cost on equal arguments, its nonnegativity for positive mass and energy, and positivity of the canonical threshold used as the rung gate.
proof idea
One-line structure instance. The three fields of InflatonMass3Cert are filled by the local lemmas domainCost_at_eq, domainCost_nonneg, and canonicalThreshold_pos. No further tactic work; the def is pure packaging of already-proved facts.
why it matters
Gives an inhabited certificate for the structural half of the inflaton-mass claim in the Cosmology domain: the cost geometry and threshold that underwrite placing the inflaton on the phi-ladder at the PeV–$10^{13},\mathrm{GeV}$ window. Module doc frames this as Plan v7 116th pass, structural theorem.
No downstream consumers are recorded yet; the natural parent is any theorem that needs a witness that the domain cost is a genuine cost (zero on match, nonnegative, positive threshold) before identifying $m_{\mathrm{inflaton}}=\varphi^k E_{\mathrm{coh}}$. Ties to the broader RS mass formula (yardstick times $\varphi^{\mathrm{rung}}$) and to $J$-cost nonnegativity from the forcing chain, without yet fixing the exact rung or matching observational bounds.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.