scalar_amplitude_observed
plain-language theorem explainer
scalar_amplitude_observed supplies the numerical value 2.1 × 10^{-9} for the scalar amplitude A_s in the primordial power spectrum. Cosmologists matching Recognition Science J-cost fluctuation models to CMB data cite it when assembling the observed spectrum. The definition is a direct constant assignment with no lemmas or reductions.
Claim. The observed scalar amplitude of the primordial power spectrum is given by $A_s = 2.1 × 10^{-9}$.
background
The COS-009 module derives the primordial power spectrum from Recognition Science principles, with J-cost quantum fluctuations during inflation supplying the fluctuations and the φ-ladder fixing the spectral tilt. The CMB exhibits a nearly scale-invariant spectrum P(k) ∝ k^{n_s-1} whose amplitude is fixed by observation at A_s ≈ 2.1 × 10^{-9} to seed all cosmic structure. This definition supplies that observed amplitude for direct use in constructing the full PowerSpectrum object.
proof idea
The declaration is a noncomputable definition that directly assigns the real number 2.1e-9. No tactics, lemmas, or reductions are applied; it functions as a constant embedding.
why it matters
It supplies the amplitude field to the observedSpectrum definition, which assembles the best-fit PowerSpectrum together with the spectral index and pivot scale. This anchors the COS-009 target of matching J-cost fluctuations to Planck data and permits comparison with φ-ladder predictions for the tilt inside the eight-tick octave and D = 3 framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.