planck_ratio_not_directly_phi
plain-language theorem explainer
The theorem shows that the observed Planck angular multipole ratio ℓ₂/ℓ₁ differs from the golden ratio φ. Cosmologists modeling acoustic peaks from the Recognition Science lattice cite it to separate bare wavenumber predictions from projected angular observations. The proof assumes equality for contradiction, substitutes into the numerical interval for the observed ratio, invokes the strict upper bound on φ, and reaches inconsistency by linear arithmetic.
Claim. Let $r$ denote the observed angular multipole ratio $ℓ_2/ℓ_1$ from Planck 2018 data. Then $r ≠ ϕ$, where $ϕ$ is the golden ratio.
background
The module derives φ-rational wavenumber ratios for the first three CMB acoustic peaks from the 8-tick lattice in StructureFormationFromBIT. The golden ratio ϕ satisfies 1.61 < ϕ < 1.62, with the lemma phi_lt_onePointSixTwo supplying the tighter upper bound ϕ < 1.62 (since √5 < 2.24). The observed ratio is defined as planck_ratio_2_1 := ℓ₂/ℓ₁, and the theorem planck_ratio_2_1_value establishes the concrete interval 2.45 < planck_ratio_2_1 < 2.46 using Planck values ℓ₁ = 220.0 and ℓ₂ = 540.3.
proof idea
Proof by contradiction. Assume planck_ratio_2_1 = phi. Rewrite the equality into planck_ratio_2_1_value to obtain 2.45 < phi < 2.46. Apply the lemma phi_lt_onePointSixTwo to obtain phi < 1.62. Linear arithmetic produces the contradiction.
why it matters
The result supplies the third conjunct in the master theorem cmb_acoustic_peak_ratios_one_statement, which packages the three structural facts: k₂/k₁ = ϕ in (1.61, 1.62), k₃/k₁ = ϕ² in (2.59, 2.63), and the observed angular ratio inequality. It implements the module docstring distinction that the φ-rational prediction holds at the bare wavenumber level while angular multipole ratios incorporate projection geometry. The declaration closes one clause of the CMB acoustic peak ratios master certificate and ties into the eight-tick octave structure underlying the peak ratios.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.