Cosmology Baryon Higher Order

The baryon asymmetry correction

The observable universe contains vastly more matter than antimatter. This imbalance, quantified by the baryon asymmetry parameter η_B, is one of cosmology's deep puzzles. In the standard model of particle physics, the known mechanisms do not obviously produce the observed value, so the number is a target for any theory that claims to explain cosmic origins.

The Planck 2018 cosmic microwave background measurements give η_B = (6.104 ± 0.058) × 10⁻¹⁰. The Recognition Science framework, which builds physical structure from a discrete record of recognition events, makes a leading-order prediction: η_B = φ⁻⁴⁴, where φ is the golden ratio (1.618...). This evaluates to about 6.376 × 10⁻¹⁰, which exceeds the measured value by roughly 4.5%. Since the framework has no free parameters, this gap cannot be tuned away by adjusting constants.

The module BaryonHigherOrder computes the first subleading correction. The physical picture: during the electroweak phase transition, sphaleron processes are active for about N_sph = φ⁸ ≈ 47 cycles of the framework's eight-tick cycle. Each cycle reduces the defect by a factor δ = φ⁻⁸ ≈ 0.0147. The net washout factor is (1 − δ) ≈ 0.9853. The corrected prediction is η_B^(1) = φ⁻⁴⁴ × (1 − φ⁻⁸), which evaluates to about 6.28 × 10⁻¹⁰, roughly halving the gap to the CMB value.

The module proves, in a machine-checked library of formal theorems, that the correction factor lies strictly between 0 and 1, that the corrected value remains positive, and that it is strictly smaller than the leading term. These are formal facts about the definitions. The physical mechanism itself is a hypothesis with explicit falsifiers: if precision measurements establish η_B outside [5.5, 7.5] × 10⁻¹⁰ at greater than 5σ, the leading-order prediction is falsified; if η_B is outside [6.0, 6.5] × 10⁻¹⁰ at greater than 3σ, the corrected prediction is falsified.

What this means for a reader: the framework's zero-parameter prediction is close to the observed value, and the first correction moves it closer. The gap is not eliminated, but the direction and size of the correction are fixed by the framework's internal structure. Whether this counts as a successful derivation or a near miss depends on future measurements and on whether the washout mechanism survives scrutiny.

/-- The leading-order baryon asymmetry: φ⁻⁴⁴. -/
theorem eta_B_leading : eta_B_phi_scale = phi ^ (-44 : ℤ) := rfl

/-- The correction factor lies strictly in (0, 1). -/
theorem correction_factor_in_interval :
    0 < correction_factor ∧ correction_factor < 1 :=
  ⟨correction_factor_pos, correction_factor_lt_one⟩

/-- The corrected prediction is less than the leading term.
    The 8-tick washout reduces η_B. -/
theorem corrected_lt_leading : eta_B_corrected < eta_B_phi_scale := by
  unfold eta_B_corrected
  have h1 : 0 < eta_B_phi_scale := eta_B_leading_pos
  have h2 : correction_factor < 1 := correction_factor_lt_one
  calc eta_B_phi_scale * correction_factor
      < eta_B_phi_scale * 1 := by
        apply mul_lt_mul_of_pos_left h2 h1
    _ = eta_B_phi_scale := mul_one _

/-- HYPOTHESIS: The 8-tick washout mechanism.
    Physical basis: during the EW phase transition, sphalerons are active
    for N_sph ≈ φ⁸ recognition cycles. Each cycle, R̂ reduces the baryon
    excess by a factor δ = φ⁻⁸.
    Epistemic status: HYPOTHESIS with falsifier
    (η_B outside [6.0, 6.5] × 10⁻¹⁰ at > 3σ would falsify this). -/
structure BaryonCorrectionCert where
  /-- Leading term -/
  leading : eta_B_phi_scale = phi ^ (-44 : ℤ)
  /-- Correction factor -/
  correction : correction_factor = 1 - phi ^ (-8 : ℤ)
  /-- Corrected prediction -/
  corrected_def : eta_B_corrected = eta_B_phi_scale * correction_factor
  /-- Correction is positive -/
  correction_pos : 0 < correction_factor
  /-- Correction is less than 1 -/
  correction_lt_one : correction_factor < 1
  /-- Corrected prediction is smaller -/
  corrected_smaller : eta_B_corrected < eta_B_phi_scale
  /-- Corrected prediction is positive -/
  corrected_pos : 0 < eta_B_corrected
  /-- The correction term is at rung -52 -/
  correction_rung : eta_B_phi_scale * delta_washout = phi ^ (-52 : ℤ)

What this page does not claim

The module does not prove that the washout mechanism is physically real. The module does not eliminate the gap to the measured value. The module does not derive the baryon asymmetry from first principles without the washout hypothesis.

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