n_s_55_value
plain-language theorem explainer
The theorem fixes the spectral index at exactly 55 e-folds to 1 minus 2 over 55 under the J-cost inflaton. Cosmologists matching Recognition Science predictions against Planck CMB data would cite this numerical anchor point. The proof is a direct reflexivity reduction to the definition of spectral_index.
Claim. The spectral index at 55 e-folds satisfies $n_s = 1 - 2/55$.
background
The module derives the inflaton potential from the Recognition Composition Law, showing that J-cost in logarithmic coordinates yields the plateau form G(t) = cosh(t) - 1. This potential produces the standard slow-roll parameters ε and η, with the spectral index following the α-attractor relation n_s = 1 - 2/N. The upstream definition spectral_index (N : ℝ) := 1 - 2/N supplies the general slow-roll formula used here.
proof idea
One-line term proof that applies the definition of spectral_index directly via reflexivity.
why it matters
This supplies the concrete N=55 evaluation referenced in the module doc-comment as part of n_s_from_jcost. It anchors the J-cost derivation of alpha-attractor predictions inside the Recognition Science framework, where the inflaton arises from the Recognition Composition Law and yields n_s ≈ 0.9636 inside Planck 1σ. The result closes one numerical step toward the master certificate InflationFromJCostCert.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.