power
plain-language theorem explainer
The power definition evaluates the primordial power spectrum at wavenumber k for a PowerSpectrum record holding amplitude, spectral index, and pivot scale. Cosmologists working on CMB fluctuations seeded by J-cost quantum fluctuations would cite this when linking the phi-ladder to the observed tilt. It is a direct one-line algebraic instantiation of the standard form P(k) = A_s (k/k_*)^(n_s - 1).
Claim. Let P be a primordial power spectrum record with amplitude A_s > 0, spectral index n_s, and pivot scale k_* > 0. The power at wavenumber k > 0 is A_s (k / k_*)^(n_s - 1).
background
Module COS-009 targets derivation of the primordial power spectrum from Recognition Science, with fluctuations arising from J-cost quantum fluctuations during inflation and the phi-ladder fixing the spectral tilt. The referenced PowerSpectrum structure parametrizes the standard form P(k) = A_s (k/k_)^(n_s - 1), where k is wavenumber (inverse length), k_ is the pivot scale, A_s the amplitude at pivot, and n_s the spectral index near 0.965.
proof idea
One-line definition that multiplies the amplitude field by the power-law term (k / pivot_scale) raised to the exponent (spectral_index - 1).
why it matters
This supplies the concrete evaluation map for the primordial spectrum, feeding downstream results such as costCompose_power_assoc and powerMap in RecognitionCategory. It realizes the COS-009 target of a PRL paper deriving the CMB spectral index from the golden ratio, connecting to the phi-ladder and T5 J-uniqueness landmarks. Open questions remain on exact phi-prediction for the tilt value.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.