cabibboPhi
plain-language theorem explainer
cabibboPhi defines the real number φ^{-3} as a proxy for the Cabibbo mixing angle λ in the CKM matrix. Researchers checking Recognition Science predictions against PDG data would cite this value when verifying the interval (0.225, 0.240). The definition is a direct abbreviation that invokes the golden-ratio identity φ³ = 2φ + 1.
Claim. The Cabibbo angle proxy is the real number $φ^{-3}$, where $φ$ is the golden ratio satisfying $φ^3 = 2φ + 1$.
background
The CKM Lambda Parameter from Phi-Ladder module studies the Wolfenstein parametrisation of the CKM matrix. It records the RS prediction A = 9/11 for the Wolfenstein A parameter and introduces the Cabibbo proxy as 1/φ³ ≈ 0.236, to be compared with the PDG value λ ≈ 0.2247. The module states that the honest structural claim places λ between 1/φ³ and 1/φ^{2.9} and sets the Lean goal of proving membership in the open interval (0.225, 0.240).
proof idea
The declaration is a definition that directly assigns (phi ^ 3)^{-1} to cabibboPhi. It is a one-line abbreviation relying on the algebraic identity φ³ = 2φ + 1 stated in the accompanying comment; no lemmas or tactics are applied.
why it matters
This definition supplies the concrete value used by the theorem cabibbo_in_band, which proves 1/φ³ lies inside the PDG band, and by the structure CKMLambdaCert, which certifies both A = 9/11 and the Cabibbo proxy in band. It realises the Recognition Science prediction for the Cabibbo angle from the phi-ladder, connecting to the self-similar fixed point φ forced at step T6 of the unified forcing chain. The module leaves open the precise J-cost correction needed to reach the exact PDG number 0.2247.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.