phi3_eq
plain-language theorem explainer
The golden ratio satisfies the cubic identity φ³ = 2φ + 1. Particle physicists modeling CKM Wolfenstein parameters via the phi-ladder would cite this to relate the Cabibbo angle to 1/φ³. The proof is a one-line wrapper that reduces the cubic directly to the quadratic identity φ² = φ + 1 via nonlinear arithmetic.
Claim. Let φ = (1 + √5)/2 be the golden ratio. Then φ³ = 2φ + 1.
background
In the CKM Lambda from Phi-Ladder module the Wolfenstein λ parameter is approximated by the inverse cube of the golden ratio arising from the phi-ladder lattice. The local setting treats λ as lying between 1/φ³ and nearby phi-ladder values, with the explicit goal of showing 1/φ³ lies inside the PDG interval (0.225, 0.240). Upstream, the quadratic identity φ² = φ + 1 is proved in Constants.phi_sq_eq from the minimal polynomial x² - x - 1 = 0 and is re-proved in NumberTheory.PhiLadderLattice.phi_sq_eq.
proof idea
This is a one-line wrapper that applies the quadratic identity phi_sq_eq via the nlinarith tactic to verify the cubic relation.
why it matters
The identity is used directly by cabibbo_in_band to place 1/φ³ inside the PDG band for λ and by ckmlambdaCert to certify the RS prediction for the Cabibbo angle. It fills the leading-order phi-ladder step in the CKM hierarchy, connecting to the self-similar fixed point φ forced in the T0-T8 chain and to the Recognition Composition Law that governs J-costs on the ladder.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.