Cosmology Baryon Asymmetry From Phi Ladder Baryon Rung Gap45

The baryon rung

The baryon asymmetry of the universe is the observed excess of matter over antimatter in the cosmos. The standard measure, η_B, is the ratio of the number of baryons (protons and neutrons) to the number of photons in the cosmic microwave background. The measured value is about six parts per billion, a small number that cosmologists have struggled to explain from first principles.

In Recognition Science, the framework's account of this asymmetry is a prediction, not a derivation. The framework models the asymmetry as the inverse of the golden ratio raised to a specific power. The golden ratio, φ, is the number approximately equal to 1.618, the positive solution to the equation x² = x + 1. The framework's model chooses the power 44, defining the predicted value as η_B = φ^(-44).

The declaration baryonRung_gap45 establishes a formal fact about this model. It proves, within the framework's machine-checked library of formal theorems, that the chosen power is exactly 44. This is a definitional identity, a statement that the symbol for the rung is equal to the number 44. The declaration also proves that φ^44 is greater than 10^8, which means the predicted η_B is less than 10^(-8), a small number consistent with the observed order of magnitude.

In Recognition Science, the framework derives the value of the golden ratio from its foundational cost function, and it derives the structure of the phi-ladder on which particle masses sit. The choice of the 44th rung for the baryon asymmetry is an identification, a hypothesis about which rung corresponds to this cosmological quantity. The framework's library proves the arithmetic facts about this choice, but it does not prove that the choice is the correct one for the universe.

The declaration does not claim that the framework has derived the baryon asymmetry from more fundamental principles. It does not claim that the measured value of η_B is exactly φ^(-44). The framework's prediction is a target for comparison with observation, not a theorem about the cosmos. The declaration's proof is about the internal consistency of the model, not about the external validity of its identification.

theorem baryonRung_gap45 : baryonRung = 44 := rfl

/-- φ^44 > 10^8. -/
theorem phi44_gt_1e8 : phi ^ 44 > (10:ℝ)^8 := by
  have h12 : phi ^ 12 > 321 := by
    have h2 := phi_sq_eq
    have h3 : phi ^ 3 = 2 * phi + 1 := by nlinarith
    have h4 : phi ^ 4 = 3 * phi + 2 := by nlinarith
    have h5 : phi ^ 5 = 5 * phi + 3 := by nlinarith
    have h6 : phi ^ 6 = 8 * phi + 5 := by nlinarith
    have h8 := phi8_val
    have h12v : phi ^ 12 = phi ^ 6 * phi ^ 6 := by ring
    rw [h12v]; nlinarith [phi_gt_onePointSixOne]
  have h44 : phi ^ 44 = phi ^ 32 * phi ^ 12 := by ring
  rw [h44]
  norm_num
  nlinarith [mul_pos (by linarith [phi32_gt_4M] : (0:ℝ) < phi^32) (by linarith : (0:ℝ) < phi^12),
             phi32_gt_4M, h12]

/-- η_B < 10^(-8). -/
theorem etaB_small : etaB_RS * (10:ℝ)^8 < 1 := by
  unfold etaB_RS baryonRung
  rw [inv_mul_lt_iff₀ (pow_pos phi_pos 44)]
  simp only [mul_one]
  exact phi44_gt_1e8

def baryonRung : ℕ := 44

noncomputable def etaB_RS : ℝ := (phi ^ baryonRung)⁻¹

What this page does not claim

The declaration does not derive the baryon asymmetry from the framework's foundational cost function. The declaration does not claim that the measured value of η_B is exactly φ^(-44). The declaration does not provide a physical mechanism for baryogenesis.

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