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

ns_from_inflation

show as:
view Lean formalization →

ns_from_inflation supplies the approximate scalar spectral index n_s from the inflationary potential using the Recognition Science phi parameter. Cosmologists checking framework predictions against CMB data cite this when evaluating consistency with observed n_s values near 0.96. The implementation is a direct one-line algebraic expression without further derivation or lemmas.

claim$n_s (phi) = 1 - 2 / (60 (phi - 1))$, where phi denotes the self-similar fixed point.

background

The Recognition Science framework derives all physics from one functional equation, with phi arising as the self-similar fixed point forced by the T0-T8 chain. The Cosmology.Predictions module generates testable claims by importing measurement data and constants, building on the upstream theorem that reduces seven independent axioms to four substantive structural conditions plus three definitional facts.

proof idea

This is a one-line definition that directly encodes the approximate formula from the inflation potential. No lemmas are applied; the body consists of the explicit arithmetic expression.

why it matters in Recognition Science

The definition supplies the n_s value consumed by verify_ns, which checks agreement with CMB measurements within error bounds. It fills a prediction slot in the cosmology module, connecting the phi-ladder and inflation potential to observables. The placement ties to the self-similar fixed point and constant derivations in the broader forcing chain.

scope and limits

formal statement (Lean)

  11noncomputable def ns_from_inflation (φ : ℝ) : ℝ :=

proof body

Definition body.

  12  1 - 2 / (60 * (φ - 1))  -- Approximate formula from potential
  13
  14/-- Verify against CMB data. -/

used by (1)

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

depends on (1)

Lean names referenced from this declaration's body.