Cosmology Inflation Spectral Index From Jcost Ns Rs Band

The spectral index band

In cosmology, the spectral index n_s is a number that describes how the density fluctuations of the early universe vary with scale. A value of exactly 1 means the fluctuations are perfectly scale-invariant, the same at every size. The Planck satellite measured n_s = 0.965 ± 0.004, a value slightly less than 1, which tells cosmologists that the very early universe underwent a period of rapid expansion called inflation, and that the details of that expansion left a faint imprint on the cosmic microwave background.

The framework's machine-checked library of formal theorems contains a definition that produces a specific value for this index. The definition, called nsRS, is built from a single number: 45. It sets n_s = 1 - 2/45, which evaluates to approximately 0.9556. The theorem nsRS_band proves, with no unproven assumptions, that this value lies strictly between 0.955 and 0.957. This is the entire content of the declaration: a precise, verified statement about where a particular formula places the spectral index.

The framework's library also proves that this value is close to the Planck measurement. A separate theorem, nsRS_near_planck, shows that the absolute difference between the framework's value and the measured 0.965 is less than 0.015. The honesty of this claim is in its weakness: the band is within 0.01 of the measured central value, but the measurement's own error is only ±0.004. The framework's number is close, but it is not inside the error bars of the observation.

What the declaration does not claim is just as important as what it proves. The theorem nsRS_band does not say that the framework's value matches the Planck result. It does not derive the number 45 from any deeper principle within the framework; the definition simply chooses 45 as a starting point. The theorem proves the arithmetic of the band, not the physical origin of the number that defines it. The framework's value is a prediction from a chosen definition, not a derived consequence of the framework's core axioms.

/-- n_s_RS ∈ (0.955, 0.957). -/
theorem nsRS_band : (0.955 : ℝ) < nsRS ∧ nsRS < 0.957 := by
  rw [nsRS_val]; norm_num

theorem nsRS_near_planck : |nsRS - nsPlanck| < 0.015 := by
  rw [nsRS_val]
  unfold nsPlanck
  rw [abs_lt]
  constructor <;> norm_num

What this page does not claim

The theorem does not claim the framework's value matches the Planck measurement within its error bars. The declaration does not derive the number 45 from the framework's axioms. This answer does not claim that the framework's spectral index is a prediction from first principles.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Cosmology/InflationSpectralIndexFromJCost.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: