lambda_RS_interval
plain-language theorem explainer
The RS Cabibbo parameter λ_RS = (φ−1)²/φ = φ⁻³ lies strictly in (0.234, 0.238). CKM and forcing-chain work cites this as the certified numerical window for the structural Wolfenstein λ before the pending Berry correction. The proof unfolds the definition and squeezes via the certified bounds 1.61 < φ < 1.62 plus φ² = φ+1.
Claim. Let $\varphi$ be the golden ratio and set $\lambda_{\mathrm{RS}} = (\varphi-1)^2/\varphi$ (equivalently $\varphi^{-3}$). Then $0.234 < \lambda_{\mathrm{RS}} < 0.238$.
background
Module CKMExact derives Wolfenstein CKM parameters from Q₃ geometry: Gray-code flip counts [4,2,2], generation torsion {0,11,17}, and face-flux Berry corrections. The headline result is A_corrected = 9/11 within 0.6σ of PDG; the same skeleton supplies a structural Cabibbo angle.
Here λ_RS is the pure geometric prediction (φ−1)²/φ. Because φ−1 = 1/φ, this collapses to φ⁻³ ≈ 0.236. PDG 2024 quotes λ_PDG ≈ |V_us| ≈ 0.2265, so the structural value sits a few percent high; a geometric Berry integral over the CW filtration of Q₃ is expected to supply an O(1) factor ≈ 0.960, analogous to the A_structural → A_corrected fix.
Upstream constants supply the squeeze fuel: φ > 1.61, φ < 1.62, and the identity φ² = φ+1 from the minimal polynomial.
proof idea
Unfold λ_RS to (φ−1)²/φ. Import the certified bounds φ > 1.61, φ < 1.62 and the identity φ² = φ+1. Two nlinarith goals establish the cross-multiplied inequalities 0.234·φ < (φ−1)² and (φ−1)² < 0.238·φ. Split the conjunction; each side rewrites by lt_div_iff₀ / div_lt_iff₀ using φ > 0, then finishes by linarith.
why it matters
Pins the numerical window for the structural Cabibbo angle that the module identifies with φ⁻³, confirming the prediction sits within one generation (~5%) of PDG |V_us|. Downstream, lambda_structural_discrepancy uses both sides of the interval to prove |λ_RS − λ_PDG|/λ_PDG < 0.06. The certificate bundle ckmExactCert packages the exact A-side results alongside this λ infrastructure. Higher up, t8_to_gauge_standard_model_bridge_holds routes T8 (D=3 cube/spinor skeleton) into gauge and Standard Model surfaces, so this bound is part of the SM bridge evidence. Open gap flagged in-module: the exact Berry-phase correction that would move 0.236 → ~0.2265 is not yet formalized.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.