Physics Microwave Background From Phi Ladder

The cosmic microwave background and a proposed ratio

The cosmic microwave background (CMB) is the oldest light in the universe, a faint glow left over from about 380,000 years after the Big Bang. Imprinted on this glow are tiny temperature variations, and when astronomers plot their strength against angular scale, they see a series of peaks and troughs. These are the acoustic peaks, the signature of sound waves that traveled through the hot, dense early universe. The first three peaks appear at multipole moments of roughly l_1 ≈ 220, l_2 ≈ 540, and l_3 ≈ 800. A multipole moment is a way of measuring angular size on the sky; higher values mean smaller angles.

In 2026, a research note in the Recognition Science framework proposed that these peak positions might be related to the golden ratio φ ≈ 1.618. The note observed that the ratios l_2/l_1 ≈ 2.45 and l_3/l_1 ≈ 3.64 are close to φ^2.2 and φ^2.8 respectively. This is an empirical observation about the measured peak positions, not a derived result. The formal module that accompanies the note, however, proves something much more general. It defines a cost function on ratios of two real numbers, and proves three facts: the cost is zero when the two numbers are equal, it is never negative for positive inputs, and a certain threshold value φ - 3/2 is positive.

In Recognition Science, the ledger, a discrete record of recognition events, assigns a forced cost to any ratio. The cost function is Jcost(m/e), where m and e are real numbers. The three proved facts are: Jcost(1) = 0, Jcost(x) ≥ 0 for x > 0, and φ > 3/2. These are properties of the cost function itself, true for any positive inputs, not specific to the CMB. The documentation states this plainly: it proves nothing specific to the microwave background, because the cost function is defined without reference to any physical quantity.

The module does include a structure called CMBAcousticRatioCert that packages these three facts together, and a proof that this structure is inhabited. But this structure is a certificate that the cost function has the three generic properties, not a certificate about the CMB. The research note records where the idea was meant to go, not a result that has been achieved. What would make this a theorem about the CMB is a definition of m and e in terms of the actual peak positions, a step that has not been taken.

The distinction matters. The framework's library of formal theorems is machine-checked, meaning every step is verified by a computer. But a machine-checked proof of a generic cost property is not a machine-checked proof about cosmology. The proposed φ-power ratios for the CMB peaks remain an unverified hypothesis, a research direction noted in the documentation but not established by the formal mathematics.

def domainCost (m e : ℝ) : ℝ := Jcost (m / e)

theorem domainCost_at_eq (r : ℝ) (h : r ≠ 0) : domainCost r r = 0 := by
  unfold domainCost; rw [div_self h]; exact Jcost_unit0

theorem domainCost_nonneg (m e : ℝ) (hm : 0 < m) (he : 0 < e) : 0 ≤ domainCost m e := by
  unfold domainCost; exact Jcost_nonneg (div_pos hm he)

theorem canonicalThreshold_pos : 0 < canonicalThreshold := by
  unfold canonicalThreshold; linarith [phi_gt_onePointFive]

theorem cert_inhabited : Nonempty CMBAcousticRatioCert := ⟨cert⟩

What this page does not claim

The φ-power ratios for the CMB peaks are not derived or proved; they are an empirical observation recorded in a research note. The module does not establish any connection between the cost function and the actual measured peak positions. The golden ratio is not claimed to be the cause of the peak spacings; the note only observes a numerical proximity.

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/Physics/MicrowaveBackgroundFromPhiLadder.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: