Cosmology Primordial Spectrum Amplitude Derivation

The amplitude claim

The cosmic microwave background (CMB) is the oldest light in the universe, a faint glow left over from 380,000 years after the Big Bang. Across the sky, its temperature is almost perfectly uniform at about 2.7 kelvin, but it carries tiny variations, roughly one part in 100,000. These variations are the primordial fluctuations, the seeds from which galaxies, clusters, and the large-scale structure of the cosmos grew. Cosmologists describe these seeds with a power spectrum, a function that says how much fluctuation exists at each spatial scale. The standard model of cosmology fits the observed spectrum with two key numbers: a spectral index n_s ≈ 0.965, which measures how the fluctuation strength changes with scale, and an amplitude A_s ≈ 2.1 × 10⁻⁹, which sets the overall size of the ripples.

The amplitude is not predicted by the standard model; it is a free parameter, fixed by measurement. In Recognition Science, the framework's library of machine-checked formal theorems contains a declaration called amplitude_derivation. In plain terms, the declaration asserts that the 10⁻⁹ amplitude comes from inflation plus quantum fluctuations. The framework models primordial fluctuations as arising from fluctuations in its core cost function, the forced price of a recognition event, during an inflationary epoch. The theorem itself, however, is a formal placeholder: it proves the statement True, meaning it records the intended claim rather than deriving the number from deeper principles. It does not compute 2.1 × 10⁻⁹ from the framework's constants or from the golden ratio φ.

What the framework does offer is a set of related predictions, each tagged as a hypothesis or a definition, not a theorem. It predicts a spectral tilt, n_s − 1, close to 1/(8φ³) ≈ 0.0047, which would give n_s ≈ 0.995, about 3% higher than the observed 0.9649. It predicts a tensor-to-scalar ratio r ≈ 0.02 from (φ−1)⁴, though the library notes the correct value would be (2−φ)⁴ ≈ 0.021, not (φ−1)⁴ ≈ 0.146. It also predicts negligible running of the spectral index and negligible non-Gaussianity. These are testable predictions, and the library defines a falsifier structure: if the spectral index shows no φ connection, or if the tensor ratio contradicts the prediction, the framework's account is falsified.

The honest verdict is that the amplitude derivation is a target, not an achievement. The declaration establishes the framework's intention to derive the primordial spectrum's amplitude from its cost-fluctuation mechanism, but it does not yet carry out that derivation. The observed values of n_s, A_s, and r are entered as definitions, not as consequences of the framework's axioms. The gap between prediction and measurement, especially for the spectral index, remains open. What a reader can take away is a clear picture of how a derivation would look: quantum fluctuations in the cost function during inflation, mapped to density perturbations, mapped to the power spectrum. That picture is coherent, but the numbers are not yet forced.

/-- The amplitude A_s ≈ 2 × 10⁻⁹ from RS:

    A_s ~ (H/m_P)² ~ (V/m_P⁴) ~ (E_inflation / E_P)⁴

    If E_inflation ~ E_GUT ~ 10¹⁶ GeV:
    A_s ~ (10¹⁶/10¹⁹)⁴ = 10⁻¹² (too small!)

    Need quantum effects: A_s ~ (H τ₀)² × (φ-corrections) -/
theorem amplitude_derivation :
    -- The 10⁻⁹ amplitude comes from inflation + quantum
    True := trivial

/-- The amplitude A_s ≈ 2 × 10⁻⁹ from RS:

    A_s ~ (H/m_P)² ~ (V/m_P⁴) ~ (E_inflation / E_P)⁴

    If E_inflation ~ E_GUT ~ 10¹⁶ GeV:
    A_s ~ (10¹⁶/10¹⁹)⁴ = 10⁻¹² (too small!)

    Need quantum effects: A_s ~ (H τ₀)² × (φ-corrections) -/
theorem amplitude_derivation :
    -- The 10⁻⁹ amplitude comes from inflation + quantum
    True := trivial

/-- Analysis of n_s - 1 ≈ -0.035:

    Possible φ-connections:
    1. |n_s - 1| = (φ - 1)² = 0.382² = 0.146 (too large)
    2. |n_s - 1| = (φ - 1)³ = 0.236 × 0.382 = 0.090 (still large)
    3. |n_s - 1| = 1/(2φ³) = 1/(2 × 4.236) = 0.118 (too large)
    4. |n_s - 1| = 1/(8φ³) = 0.030 (close!)
    5. |n_s - 1| = 1/(φ⁸) = 1/46.98 = 0.021 (too small)

    Best fit: |n_s - 1| ≈ 1/(8φ³) ≈ 0.030 (vs observed 0.035) -/
noncomputable def phi_prediction_tilt : ℝ := 1 / (8 * phi^3)

theorem spectral_tilt_phi_connection :
    -- |n_s - 1| ≈ 1/(8φ³) within 15%
    -- This connects spectral tilt to 8-tick and φ
    True := trivial

/-- RS prediction for r:

    r may be φ-related. Possible predictions:
    - r = (φ - 1)⁴ = 0.021 (testable by CMB-S4!)
    - r = 1/(8φ⁵) = 0.011
    - r = 1/φ⁸ = 0.021

    All these are in the observable range! -/
noncomputable def rs_prediction_r : ℝ := (phi - 1)^4

theorem r_prediction :
    -- r ≈ 0.02 is a testable RS prediction
    -- NOTE: The comment "(φ-1)⁴ = 0.382⁴" is incorrect.
    -- φ - 1 ≈ 0.618 (the golden ratio conjugate), so (φ-1)⁴ ≈ 0.146.
    -- The correct value 0.021 would be (2-φ)⁴ = 0.382⁴.
    -- For now, we prove a weaker bound: 0.1 < (φ-1)⁴ < 0.2
    0.1 < rs_prediction_r ∧ rs_prediction_r < 0.2 := by
  unfold rs_prediction_r
  -- φ - 1 ≈ 0.618, so (φ-1)⁴ ≈ 0.146
  -- Using bounds: 1.61 < φ < 1.62, so 0.61 < φ-1 < 0.62
  have h_phi_gt : phi - 1 > 0.61 := by
    have h := phi_gt_onePointSixOne
    linarith
  have h_phi_lt : phi - 1 < 0.62 := by
    have h := phi_lt_onePointSixTwo
    linarith
  -- 0.61^4 ≈ 0.138 > 0.1, 0.62^4 ≈ 0.148 < 0.2
  have h_low : (0.61 : ℝ)^4 > 0.1 := by norm_num
  have h_high : (0.62 : ℝ)^4 < 0.2 := by norm_num
  have h_phi_pos : phi - 1 > 0 := by linarith [one_lt_phi]
  constructor
  · calc 0.1 < (0.61 : ℝ)^4 := h_low
       _ < (phi - 1)^4 := by
           apply pow_lt_pow_left₀ h_phi_gt (by norm_num) (by norm_num)
  · calc (phi - 1)^4 < (0.62 : ℝ)^4 := by
           apply pow_lt_pow_left₀ h_phi_lt (le_of_lt h_phi_pos) (by norm_num)
       _ < 0.2 := h_high

/-- The scalar spectral index n_s ≈ 0.9649 (Planck 2018). -/
noncomputable def spectral_index_observed : ℝ := 0.9649

/-- The scalar amplitude A_s ≈ 2.1 × 10⁻⁹. -/
noncomputable def scalar_amplitude_observed : ℝ := 2.1e-9

/-- The tensor-to-scalar ratio r < 0.06 (Planck + BICEP/Keck). -/
noncomputable def tensor_to_scalar_upper_bound : ℝ := 0.06

What this page does not claim

The amplitude 2.1 × 10⁻⁹ is not derived from framework constants or from φ in the current library. The spectral index prediction does not match the observed value within the stated 15% tolerance. The declaration does not prove that inflation occurred in the framework; it only asserts the amplitude's origin.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Cosmology/PrimordialSpectrum.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: