PowerSpectrum
plain-language theorem explainer
PowerSpectrum is a record packaging amplitude, spectral index, and pivot scale for the primordial power spectrum together with positivity constraints. Cosmologists deriving the CMB spectrum from J-cost fluctuations in Recognition Science would cite it when connecting inflation to observed fluctuations. The declaration is a plain structure definition with no computational content or proof obligations.
Claim. The primordial power spectrum is a structure containing 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
The module derives the primordial spectrum from Recognition Science J-cost fluctuations during inflation, with the phi-ladder fixing the spectral tilt. The CMB is described by a nearly scale-invariant form P(k) proportional to k to the power (n_s - 1), with n_s slightly less than 1 and amplitude around 2.1 times 10 to the minus 9. Upstream results supply the spectral index as 1 minus 2 over N from slow-roll inflation and amplitude as the S-matrix element or double-slit path sum.
proof idea
This is a structure definition with no proof body. It directly encodes the standard power-law parametrization of the primordial spectrum using the supplied fields and positivity hypotheses.
why it matters
The structure is the central data type feeding the observed best-fit spectrum and the power function at wavenumber k. It fills the COS-009 target of deriving the CMB spectrum from RS principles and links to the paper proposition on the spectral index from the golden ratio via the phi-ladder and forcing chain steps T5 through T8.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.