InflationPredictions
plain-language theorem explainer
Recognition Science inflation packages its outputs in the record InflationPredictions holding the scalar spectral index, tensor-to-scalar ratio, and non-Gaussianity for sixty e-foldings. Cosmologists working inside the framework cite this record when tabulating model outputs against Planck constraints. The declaration is a bare structure definition that introduces three real fields with no computational content or proof obligations.
Claim. The record type consists of three real numbers: the scalar spectral index $n_s$, the tensor-to-scalar ratio $r$, and the non-Gaussianity parameter $f_{NL}$, which together encode the predictions of Recognition Science inflation for $N=60$ e-foldings.
background
The Cosmology.Inflation module derives cosmic inflation from J-cost slow roll. The J-cost $J(x)=½(x+x^{-1})-1$ possesses a minimum at $x=1$; far from this point it grows linearly and supplies a nearly constant energy density that drives exponential expansion, solving the horizon, flatness, and monopole problems. The module documentation states that the inflaton is identified with the J-cost field itself and that inflation ends when the field reaches the minimum at $φ=1$.
proof idea
The declaration is a pure structure definition containing no proof body or tactics. It simply declares the three real-valued fields that are later instantiated by the downstream rsPredictions definition.
why it matters
The structure supplies the concrete record type consumed by rsPredictions, which populates the fields with the explicit values $n_s=1-2/60$, $r=8/60^2$, and $f_{NL}=0$. It realizes the COS-001 target of obtaining inflation from J-cost slow roll inside the Recognition Science framework, where the eight-tick octave and phi-ladder set the scale of the dynamics. The listed predictions match the Planck value for $n_s$ and lie below current observational bounds for $r$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.