Cosmology Baryon Asymmetry Derivation Eta B Small

The smallness bound

The baryon-to-photon ratio η_B is one of the most precisely measured numbers in cosmology: Big Bang nucleosynthesis gives (6.1 ± 0.3) × 10⁻¹⁰ and Planck 2018 CMB data give (6.12 ± 0.04) × 10⁻¹⁰. It says that for every billion photons left over from the Big Bang, there is about one proton or neutron. The number is small, and explaining why it is small, and why it is not zero, is a central problem in cosmology.

In the Recognition Science framework, the structural estimate for this ratio is built from two ingredients: a CP-violation measure J_CP and the number of relativistic degrees of freedom g★ = 106.75 at the electroweak scale. The framework's structural formula is η_B = J_CP / g★. With the framework's own value J_CP ≈ 3 × 10⁻⁵, this gives about 3 × 10⁻⁷, which is roughly 500 times larger than the observed value. The declaration eta_B_small (a theorem in the machine-checked library of formal theorems) proves only that this structural value is positive and less than 1. It does not claim to match the measured number.

What the theorem actually establishes is a weak bound: the structural estimate is below one. The proof is a short chain of inequalities: it uses the positivity of g★, the fact that J_CP is positive and less than g★, and the definition of g★ as 106.75. The theorem is part of a larger certificate that also proves the sign of the asymmetry is positive, meaning matter dominates antimatter. That sign result is the derived content of the module; the magnitude is not.

The framework is explicit that the structural scaffold is not the prediction. The observed value is instead matched by a separate hypothesis: η_B ≈ φ⁻⁴⁴·(1−φ⁻⁸)², where φ is the golden ratio, which lands within the Planck band. This expression contains no g★ and no washout factor, and the framework does not claim the two objects are connected. The missing physics, the order-parameter dynamics through the electroweak transition, is open. The smallness theorem is therefore a modest but real result: it proves the structural estimate is small in the weak sense of being less than one, and it leaves the precise magnitude unexplained.

/-- η_B is small: the structural value is below 1.
    (A weak bound; the honest magnitude statement is in the module header.) -/
theorem eta_B_small : eta_B_structural < 1 := by
  unfold eta_B_structural
  rw [div_lt_one (by norm_num [g_star] : (0:ℝ) < g_star)]
  linarith [(cp_small_but_nonzero).2, show g_star = 106.75 from rfl]

/-- The structural η_B: proportional to J_CP / g_★.
    SCAFFOLD ONLY — numerically ≈ 3×10⁻⁷, about 500× the observed value,
    because the order-one-suppressed washout constant c is not derived.
    Used solely for the sign theorem (η_B > 0) and the smallness bound. -/
noncomputable def eta_B_structural : ℝ := jarlskog_structural / g_star

/-- η_B is positive: matter dominates over antimatter.
    This follows directly from J_CP > 0 and is the genuine derived content
    (the SIGN of the asymmetry, not its magnitude). -/
theorem eta_B_positive : eta_B_structural > 0 := by
  unfold eta_B_structural
  apply div_pos jarlskog_positive
  norm_num [g_star]

What this page does not claim

The structural formula eta_B_structural does not match the observed baryon-to-photon ratio; it is about 500 times too large. The smallness theorem does not prove the magnitude of the baryon asymmetry; it only proves a weak bound below one. The φ⁻⁴⁴ rung assignment is a hypothesis, not a derived consequence of the framework's axioms.

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