n_s_at_44
plain-language theorem explainer
The declaration evaluates the spectral index at exactly 44 e-folds to obtain 1 minus 2 over 44. Cosmologists testing alpha-attractor models against CMB spectra would cite this concrete instance. The proof is a direct substitution into the definition of spectral_index via reflexivity.
Claim. The spectral index at 44 e-folds equals $1 - 2/44$.
background
The module establishes that the Recognition Composition Law forces the inflaton potential to be the J-cost function J(x) = ½(x + x⁻¹) − 1. In logarithmic coordinates t = ln(x) this becomes G(t) = cosh(t) − 1, the Starobinsky-style plateau whose curvature at the minimum supplies the slow-roll parameters. The upstream definition states: Spectral index: n_s ≈ 1 - 2/N (standard slow-roll result).
proof idea
One-line wrapper that applies the definition of spectral_index by reflexivity.
why it matters
This supplies a numerical evaluation of the spectral index derived from J-cost curvature, listed among the main results in the module documentation. It instantiates the general n_s_from_jcost relation for direct comparison with Planck data at a specific N. No downstream theorems yet reference it.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.