Cosmology Baryon Asymmetry From Phi Ladder Phi8 Val

The eighth power of phi

The golden ratio, usually written φ, is the number that solves r² = r + 1, about 1.618. Its powers follow a tidy pattern: φ² is φ + 1, φ³ is 2φ + 1, and so on, each power expressible as a whole number times φ plus another whole number. The theorem phi8_val states the next step in that chain: φ⁸ = 21φ + 13. This is not a measurement or an approximation; it is an exact identity, proved from the defining equation of φ, and it is one small piece of a larger formal structure.

The identity matters because it feeds a bound. From φ⁸ = 21φ + 13, the framework's library derives that φ⁸ is greater than 46. Squaring that result gives φ¹⁶ greater than 2000, squaring again gives φ³² greater than 4,000,000, and one more multiplication gives φ⁴⁴ greater than 100,000,000. These are not separate guesses; each follows from the previous one by simple arithmetic, and the whole chain is checked in the machine-checked library of formal theorems.

In Recognition Science, this chain of inequalities supports a prediction about the universe's matter-antimatter imbalance. The framework models the ratio of ordinary matter to photons, a quantity cosmologists call η_B, as the reciprocal of φ⁴⁴. The bound φ⁴⁴ > 10⁸ then implies η_B < 10⁻⁸, which is the right order of magnitude for the measured value. The framework's library packs all of this into a single certificate object that records the rung, the positivity of η_B, and the two inequalities.

What phi8_val itself establishes is narrow: the exact algebraic identity and the numerical bound that follows. It does not, by itself, establish the baryon asymmetry prediction. The prediction requires the additional identification of η_B with φ⁻⁴⁴, a choice the framework makes, not a theorem it proves. The identity is proved; the cosmological link is a modeled prediction, and the match to observation is an empirical check, not a formal result.

/-- φ^8 = 21φ + 13 > 46. -/
theorem phi8_val : phi ^ 8 = 21 * phi + 13 := by
  have h2 := phi_sq_eq
  have h3 : phi ^ 3 = 2 * phi + 1 := by nlinarith
  have h4 : phi ^ 4 = 3 * phi + 2 := by nlinarith
  nlinarith [sq_nonneg (phi^4)]

theorem phi8_gt_46 : phi ^ 8 > 46 := by
  rw [phi8_val]; linarith [phi_gt_onePointSixOne]

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

/-- η_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

What this page does not claim

phi8_val does not by itself predict the baryon asymmetry; the prediction requires the additional identification of η_B with φ⁻⁴⁴. The framework does not prove that the measured η_B equals φ⁻⁴⁴; the match to observation is an empirical check, not a theorem. The framework does not provide a physical mechanism for baryogenesis; it offers a numerical scaling relation.

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: