PowerSpectrum
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.
claimThe 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 in Recognition Science
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.
scope and limits
- Does not derive numerical values for amplitude or spectral index from first principles.
- Does not address tensor-to-scalar ratio or non-Gaussian features.
- Does not incorporate explicit J-cost fluctuation statistics beyond the power-law form.
Lean usage
noncomputable def example (ps : PowerSpectrum) (k : ℝ) (hk : k > 0) : ℝ := power ps k hkformal statement (Lean)
62structure PowerSpectrum where
63 amplitude : ℝ
64 spectral_index : ℝ
65 pivot_scale : ℝ
66 amplitude_pos : amplitude > 0
67 pivot_pos : pivot_scale > 0
68
69/-- Power at wavenumber k. -/