lambda_structural_bounds
plain-language theorem explainer
Structural Wolfenstein λ equals φ^{-3} exactly, so it lies in [φ^{-3}, φ^{-2}]. Anyone checking the RS Cabibbo-scale prediction for the CKM matrix cites this. The proof rewrites the structural definition to φ^{-3} via φ−1=φ^{-1}, then compares powers using φ^{-1}<1.
Claim. The structural Wolfenstein parameter satisfies $\varphi^{-3} \le \lambda_{\mathrm{struct}} \le \varphi^{-2}$. In fact the lower bound is equality: $\lambda_{\mathrm{struct}} = \varphi^{-3}$.
background
This module builds the CKM quark-mixing matrix from Q₃ cube geometry, generation torsion {0,11,17}, and Gray-code chirality. Mass-basis overlaps are suppressed by φ to the torsion gap, while weak eigenstates come from even-sign-flip SU(2) generators on the cube. Mixing angles then scale as flip-count ratios times φ^{−|Δτ|}.
Wolfenstein λ sets the Cabibbo scale (roughly |V_us|). Here the structural definition of that scale is forced by the same φ-ladder that appears throughout Recognition Science. The golden ratio obeys φ² = φ+1 (hence φ−1 = φ^{-1}) and 1 < φ, so 0 < φ^{-1} < 1. Those two facts alone pin the numerical window around the observed λ ≈ 0.225 (φ^{-3} ≈ 0.236).
Upstream lemmas used are the constant identities one_lt_phi and phi_sq_eq from Constants.
proof idea
First prove the structural definition equals φ^{-3}: unfold it, replace φ−1 by φ^{-1} via eq_inv_of_mul_eq_one_right and nlinarith on phi_sq_eq, then rewrite the resulting division as a successor power. After that rewrite, the claimed conjunction is immediate: the lower bound is le_refl, and the upper bound is pow_le_pow_of_le_one applied to 0 ≤ φ^{-1} ≤ 1 with exponents 3 ≥ 2 (norm_num).
why it matters
In the Wolfenstein parameterization, λ is the leading Cabibbo-scale entry of the CKM matrix. Pinning it exactly at φ^{-3} (with a trivial upper envelope φ^{-2}) is the first quantitative bridge from the Q₃/torsion story to a measured mixing parameter. The same φ-ladder and torsion gaps that force mass hierarchies (T5–T6 landmarks, J-cost suppression) now fix the CKM hierarchy scale.
No downstream theorems currently depend on this bound (used_by is empty), so it stands as a self-contained structural claim inside CKMFromCube, ready for later assembly into full V_ij predictions alongside the A, ρ, η siblings documented in the module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.