spectral_index_observed
plain-language theorem explainer
This definition supplies the numerical value 0.9649 for the observed scalar spectral index n_s drawn from Planck 2018 CMB data. Researchers constructing the primordial power spectrum in Recognition Science cite it to fix the red tilt when assembling the full spectrum from J-cost fluctuations. The declaration is a direct noncomputable assignment with no derivation or lemmas.
Claim. The observed scalar spectral index is defined by $n_s = 0.9649$.
background
The Cosmology.PrimordialSpectrum module targets derivation of the primordial power spectrum from Recognition Science principles. Fluctuations originate in J-cost quantum fluctuations during inflation, with the phi-ladder fixing the spectral tilt to produce a nearly scale-invariant form P(k) ∝ k^(n_s - 1) that is slightly red. This definition supplies the Planck 2018 numerical anchor n_s ≈ 0.9649 for that construction.
proof idea
The declaration is a direct noncomputable definition that assigns the real number 0.9649 with no lemmas or tactics applied.
why it matters
It supplies the spectral_index field to the observedSpectrum definition that builds the complete PowerSpectrum object. This anchors the COS-009 target of matching RS predictions to CMB data and supports the proposed PRL paper on the spectral index from the golden ratio. In the framework it fixes the observed tilt for testing against phi-ladder derivations of n_s - 1.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.