pith. machine review for the scientific record. sign in
structure definition def or abbrev high

InflationPredictions

show as:
view Lean formalization →

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.

claimThe 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 in Recognition Science

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$.

scope and limits

formal statement (Lean)

 195structure InflationPredictions where
 196  n_s : ℝ  -- Scalar spectral index
 197  r : ℝ    -- Tensor-to-scalar ratio
 198  f_NL : ℝ -- Non-Gaussianity parameter
 199
 200/-- RS predictions for N = 60 e-foldings. -/

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (2)

Lean names referenced from this declaration's body.