Cosmology Eta Binterval Cert Phi Pow Neg44 Lower

The interval certificate

The baryon-to-photon ratio η_B is one of cosmology's fundamental numbers: it counts, for every photon left over from the Big Bang, how many protons and neutrons exist. The observed value, from the Planck satellite's 2018 data release, is (6.10 ± 0.04) × 10⁻¹⁰. That is a tiny number, and its origin is a long-standing puzzle. The Recognition Science framework's machine-checked library of formal theorems addresses this puzzle with a claim that is both precise and testable: the golden ratio φ, the number satisfying φ² = φ + 1 and approximately equal to 1.618, when raised to the power −44, falls inside the interval (5.5 × 10⁻¹⁰, 7.5 × 10⁻¹⁰).

The declaration phi_pow_neg44_lower establishes the lower half of that interval: it proves, as a formal theorem, that φ⁻⁴⁴ > 5.5 × 10⁻¹⁰. The proof is a short chain of arithmetic. It uses the Fibonacci identity φ⁴⁴ = F(44) × φ + F(43), with F(44) = 701408733 and F(43) = 433494437. Since φ is known to lie between 1.61 and 1.62, the theorem bounds φ⁴⁴ between 1.5 × 10⁹ and 1.6 × 10⁹, and inverting that bound gives the lower limit on φ⁻⁴⁴. The companion declaration phi_pow_neg44_upper proves the matching upper bound, and the two together form the interval certificate eta_B_interval.

The framework's library also contains a separate theorem, observed_eta_in_interval, that checks the measured value 6.1 × 10⁻¹⁰ sits strictly between 5.5 × 10⁻¹⁰ and 7.5 × 10⁻¹⁰. That is an arithmetic fact about the numbers, not a measurement. The physical claim, that the framework's predicted interval contains the observed ratio, is an empirical check. The framework models the number 44 as a product of two structural integers: a Gray-code flip count and a torsion gap. This same 44 appears in the framework's expression for the fine-structure constant, a coincidence the framework treats as a clue about a shared origin.

What the declaration does not claim is just as important. It does not prove that the baryon-to-photon ratio must equal φ⁻⁴⁴, nor that the framework's model of the number 44 is the correct physical explanation. It proves only the interval bound on the pure mathematical quantity φ⁻⁴⁴, and it records that the measured value falls inside that interval. The structural connection behind the number 44 is a separate theorem about the framework's own definitions, and the step from that structure to the physics of the early universe remains a target for future work.

/-- φ^(-44) > 5.5 × 10⁻¹⁰. -/
theorem phi_pow_neg44_lower : phi ^ (-(44 : ℝ)) > 5.5e-10 := by
  rw [Real.rpow_neg phi_pos.le, phi_rpow_44]
  have hupper : phi ^ (44 : ℕ) < 1.6e9 := phi_pow_44_upper
  have hpos : (0 : ℝ) < phi ^ (44 : ℕ) := pow_pos phi_pos 44
  have h1 : (phi ^ (44 : ℕ))⁻¹ > (1.6e9 : ℝ)⁻¹ := by
    rw [gt_iff_lt, inv_lt_inv₀ (by norm_num : (0:ℝ) < 1.6e9) hpos]
    exact hupper
  have h2 : (1.6e9 : ℝ)⁻¹ ≥ 5.5e-10 := by norm_num
  linarith

/-- φ^(-44) < 7.5 × 10⁻¹⁰. -/
theorem phi_pow_neg44_upper : phi ^ (-(44 : ℝ)) < 7.5e-10 := by
  rw [Real.rpow_neg phi_pos.le, phi_rpow_44]
  have hlower : phi ^ (44 : ℕ) > 1.5e9 := phi_pow_44_lower
  have hpos : (0 : ℝ) < phi ^ (44 : ℕ) := pow_pos phi_pos 44
  have h1 : (phi ^ (44 : ℕ))⁻¹ < (1.5e9 : ℝ)⁻¹ := by
    rw [inv_lt_inv₀ hpos (by norm_num : (0:ℝ) < 1.5e9)]
    exact hlower
  have h2 : (1.5e9 : ℝ)⁻¹ ≤ 7.5e-10 := by norm_num
  linarith

/-- φ^(-44) ∈ (5.5 × 10⁻¹⁰, 7.5 × 10⁻¹⁰).
    The observed η_B = (6.10 ± 0.04) × 10⁻¹⁰ falls inside this interval. -/
theorem eta_B_interval :
    phi ^ (-(44 : ℝ)) > 5.5e-10 ∧ phi ^ (-(44 : ℝ)) < 7.5e-10 :=
  ⟨phi_pow_neg44_lower, phi_pow_neg44_upper⟩

/-- The observed η_B ≈ 6.1 × 10⁻¹⁰ is inside the predicted RS interval. -/
theorem observed_eta_in_interval :
    (5.5e-10 : ℝ) < 6.1e-10 ∧ (6.1e-10 : ℝ) < 7.5e-10 := by
  norm_num

/-- **STRUCTURAL THEOREM**: 44 = flip_count(axis 0) × |Δτ₁₂|.
    The rung of the baryon asymmetry is the product of:
    - The chirality asymmetry of the Gray code (flip count of preferred axis)
    - The generation torsion gap (CW filtration level difference)

    This is the SAME "44" that appears in α⁻¹ = 44π × exp(-w₈ ln φ / 44π). -/
theorem rung_44_equals_flip_times_torsion :
    (44 : ℕ) = bitFlipCount 0 * (torsionGap 0 1).natAbs := by
  simp only [bitFlipCount, torsionGap, τ]
  native_decide

What this page does not claim

The declaration does not prove that the baryon-to-photon ratio must equal φ⁻⁴⁴. The declaration does not establish that the framework's structural model of the number 44 is the correct physical explanation for the observed asymmetry. The declaration does not derive the value of the fine-structure constant.

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