PowerSpectrum
plain-language theorem explainer
PowerSpectrum packages the parameters of the primordial power spectrum as a positive amplitude A_s, spectral index n_s, and positive pivot scale k_*, matching the form P(k) = A_s (k/k_*)^(n_s-1). Cosmologists deriving CMB fluctuations from Recognition Science J-cost mechanisms during inflation would cite this packaging. The declaration is a plain structure definition with four fields and two positivity proofs.
Claim. A power spectrum consists of amplitude $A_s > 0$, spectral index $n_s$, and pivot scale $k_* > 0$ such that the power at wavenumber $k$ satisfies $P(k) = A_s (k/k_*)^{n_s-1}$.
background
Module COS-009 targets derivation of the primordial spectrum from RS principles. Fluctuations arise from J-cost quantum fluctuations during inflation, with the phi-ladder fixing the spectral tilt so that n_s - 1 is phi-related. The structure collects the standard observable parameters: amplitude at the pivot, spectral index, and pivot scale (0.05 Mpc^{-1}) together with positivity constraints.
proof idea
This is a structure definition that bundles amplitude, spectral_index, pivot_scale, and the two positivity proofs amplitude_pos and pivot_pos.
why it matters
The definition supports observedSpectrum and power in the same module, enabling the connection from the RS J-cost mechanism to CMB observables. It advances the COS-009 target and the associated PRL proposition on the CMB spectral index from the golden ratio. It positions the phi-ladder as the origin of the observed tilt near 0.965.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.