pith. machine review for the scientific record. sign in
def definition def or abbrev high

power

show as:
view Lean formalization →

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).

claimLet 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 in Recognition Science

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.

scope and limits

formal statement (Lean)

  70noncomputable def power (ps : PowerSpectrum) (k : ℝ) (hk : k > 0) : ℝ :=

proof body

Definition body.

  71  ps.amplitude * (k / ps.pivot_scale)^(ps.spectral_index - 1)
  72
  73/-- The observed best-fit spectrum. -/

used by (40)

From the project-wide theorem graph. These declarations reference this one in their body.

… and 10 more

depends on (4)

Lean names referenced from this declaration's body.