phi3_eq
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.
claimLet φ = (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 in Recognition Science
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.
scope and limits
- Does not prove that λ equals 1/φ³ exactly.
- Does not derive the full CKM matrix or the A parameter.
- Does not address higher-order corrections beyond the leading phi-ladder term.
Lean usage
rw [phi3_eq]formal statement (Lean)
52theorem phi3_eq : phi ^ 3 = 2 * phi + 1 := by nlinarith [phi_sq_eq]
proof body
Term-mode proof.
53
54/-- 1/φ³ ∈ (0.225, 0.240) — contains PDG λ = 0.2247. -/