observedSpectrum
plain-language theorem explainer
observedSpectrum records the Planck 2018 best-fit values as a PowerSpectrum instance with amplitude 2.1e-9 and index 0.9649 at pivot 0.05 Mpc^{-1}. Cosmologists testing Recognition Science derivations of the primordial spectrum against CMB data would reference this definition to anchor J-cost fluctuation predictions. The construction is a direct record literal whose positivity fields are discharged by norm_num after unfolding the observed constants.
Claim. The observed primordial power spectrum is the structure with amplitude $A_s = 2.1 times 10^{-9}$, spectral index $n_s = 0.9649$, and pivot scale $k_* = 0.05$ Mpc$^{-1}$, satisfying $A_s > 0$ and $k_* > 0$.
background
The module COS-009 derives the primordial power spectrum from J-cost fluctuations during inflation, with the phi-ladder fixing the spectral tilt. PowerSpectrum is the structure whose fields are amplitude, spectral_index, pivot_scale together with the positivity proofs amplitude > 0 and pivot_scale > 0; its power at wavenumber k is given by A_s (k/k_*)^(n_s - 1). Upstream, scalar_amplitude_observed supplies the constant 2.1e-9 and spectral_index_observed supplies 0.9649, both drawn from Planck 2018 as stated in their doc-comments.
proof idea
The definition builds the PowerSpectrum record by direct field assignment of the two observed constants and the fixed pivot 0.05, then discharges the positivity obligations via norm_num after unfolding the referenced observed constants.
why it matters
This definition supplies the fixed observational target for the COS-009 derivation of the primordial spectrum from J-cost fluctuations and the phi-ladder tilt. It anchors the paper proposition PRL on CMB Spectral Index from Golden Ratio by providing the measured n_s - 1 ≈ -0.035 against which phi-predictions such as 1/(8 phi^3) are compared. In the Recognition framework it closes the interface between the observed red spectrum and the eight-tick octave forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.