InflationFromJCostCert
plain-language theorem explainer
The structure assembles the properties showing that the J-cost in logarithmic coordinates yields the Starobinsky plateau potential, forcing the spectral index formula and slow-roll bounds with no free parameters. Cosmologists studying alpha-attractor models would cite it to anchor inflationary predictions in the Recognition Composition Law. It bundles prior lemmas on the cosh form of G, vacuum conditions, curvature calibration, and the n_s(N) expression into one certificate.
Claim. A certificate consisting of: the equality $G(t) = 1/2(e^t + e^{-t}) - 1$ for all real $t$, where $G$ is the J-cost reparametrized by $t = ln x$; $G(0) = 0$; the slow-roll parameter satisfies $epsilon(0) = 0$; $epsilon(t) leq 1/2$ for all $t$; the calibration identity $cosh(0) = 1$; the attractor parameter obeys $alpha = phi^2$; the spectral index is given by $n_s(N) = 1 - 2/N$; and the numerical bound $0.96 < n_s(55) < 0.97$.
background
In Recognition Science the J-cost is the unique function satisfying the Recognition Composition Law, written $J(x) = 1/2(x + x^{-1}) - 1$. Reparametrizing to logarithmic coordinates $t = ln x$ produces the inflaton potential $G(t) = cosh t - 1$, which has a minimum at the vacuum with $G(0) = 0$ and second derivative $G''(0) = 1$. This module derives the slow-roll parameters $epsilon = (G')^2 / (2G^2)$ and $eta = G''/G$ directly from the curvature of this form, recovering the alpha-attractor predictions of the imported Inflation module.
proof idea
The declaration is a structure definition that collects the required properties. Each field is discharged by a direct reference to a prior lemma: the functional form follows from the definition of G, the vacuum condition from G_at_zero, the vanishing of epsilon from slow_roll_epsilon_vanishes, the bound from epsilon_le_half, the calibration from the identity cosh 0 = 1, the alpha relation from self-similarity of the phi fixed point, and the spectral index from the curvature calculation in the module.
why it matters
This certificate supplies the complete chain from the Recognition Composition Law through J-uniqueness (T5) to the inflationary observables, feeding directly into the theorem inflation_from_jcost_cert. It closes the loop on the inflaton potential derivation in the Gravity module, confirming that the eight-tick octave and phi-ladder force the observed spectral index band without adjustable parameters. The result touches the open question of deriving the precise inflaton scale from the phi fixed point.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.