Cosmology Eta Bprefactor Derivation Observed In Predicted Band

The Verified Band

The baryon-to-photon ratio, often written η_B, is a cosmic census: it counts how many ordinary matter particles (protons and neutrons) exist for every photon of light left over from the Big Bang. The Planck satellite's 2018 measurements put this ratio at 6.10 × 10⁻¹⁰, give or take 0.04 × 10⁻¹⁰. That is a very small number, roughly six baryons for every ten billion photons.

In Recognition Science, the framework derives a candidate value for this ratio from a chain of forced mathematical structures. The starting point is the golden ratio φ, the number satisfying r² = r + 1. The framework's internal logic forces a specific scaling: the leading term is φ raised to the power −44, which is about 6.376 × 10⁻¹⁰. This is then multiplied by a correction factor, called c_RS, which is (1 − φ⁻⁸)². Here φ⁻⁸ is about 0.0213, so the correction factor is about 0.9579. The product, η_B^RS = c_RS × φ⁻⁴⁴, comes to roughly 6.107 × 10⁻¹⁰.

The declaration observed_in_predicted_band is a theorem in the framework's machine-checked library of formal theorems. It proves a simple but precise fact: the observed central value 6.10 × 10⁻¹⁰ lies strictly between 6.0 × 10⁻¹⁰ and 6.2 × 10⁻¹⁰. This band is exactly the range that the framework's own calculation, with its correction factor, predicts. The theorem does not say the prediction is exactly equal to the measurement; it says the measured value falls inside the predicted window. A companion theorem, eta_B_corrected_in_observed_band, proves that the framework's computed value itself also lies within this same band.

What this theorem does not claim is just as important. It does not prove that the correction factor (1 − φ⁻⁸)² comes from a physical process. The docstring is explicit: the factors that would appear in a full dynamical theory of baryogenesis, such as CP violation or sphaleron rates, are absent from this theorem. The number is treated as a fixed address on a φ-powered ladder, not as the output of a thermal history. The interpretation of the squared correction as two independent washout channels, one for matter and one for antimatter, is a hypothesis, not a proved result. The theorem establishes an algebraic and numerical match, nothing more.

The practical consequence is a sharp, testable prediction. The framework's band of (6.0, 6.2) × 10⁻¹⁰ is narrow. If future precision measurements, say from a next-generation CMB experiment, push the central value outside this range by more than three standard deviations, the squared two-sided form is falsified. A first-order correction, (1 − φ⁻⁸), would give a value about 2.3% higher, which is already outside the current 1σ error bar. The squared form brings the prediction inside that error bar. This is what the theorem secures: a concrete, falsifiable claim that currently sits within the observational window.

/-- The Planck 2018 observed central value 6.10 × 10⁻¹⁰ falls inside
    the predicted band (6.0, 6.2) × 10⁻¹⁰. -/
theorem observed_in_predicted_band :
    (6.0e-10 : ℝ) < 6.10e-10 ∧ (6.10e-10 : ℝ) < 6.2e-10 := by
  constructor <;> norm_num

/-- The corrected RS prediction lies in the band (6.0, 6.2) × 10⁻¹⁰,
    which contains the Planck 2018 central value 6.10 × 10⁻¹⁰. -/
theorem eta_B_corrected_in_observed_band :
    eta_B_corrected_two_sided > 6.0e-10 ∧ eta_B_corrected_two_sided < 6.2e-10 :=
  ⟨eta_B_corrected_lower, eta_B_corrected_upper⟩

/-- Equivalent expanded form: c_RS = (1 − φ^(−8))^2. -/
theorem c_RS_expanded : c_RS = (1 - phi ^ (-8 : ℤ)) ^ 2 := by
  unfold c_RS BaryonHigherOrder.correction_factor BaryonHigherOrder.delta_washout
  rfl

What this page does not claim

The theorem does not prove the physical origin of the correction factor. It does not claim the prediction is exactly equal to the measured value. It does not include dynamical baryogenesis factors like CP violation or sphaleron rates.

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/EtaBPrefactorDerivation.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: