lambda_RS_pos
plain-language theorem explainer
The RS Cabibbo parameter λ_RS = (φ − 1)²/φ is strictly positive. Anyone using the φ-ladder formula for the Wolfenstein λ needs this for ratio bounds and inequality chains in the CKMExact development. Proof is a one-line div_pos after nlinarith from φ > 1 and φ > 0.
Claim. If $\varphi$ denotes the golden ratio and $\lambda_{\mathrm{RS}} := (\varphi-1)^2/\varphi$, then $0 < \lambda_{\mathrm{RS}}$.
background
In the CKMExact module the Wolfenstein parameters are read off Q₃ geometry (Gray-code flip counts and generation torsion) and a φ-ladder expression for the Cabibbo angle. The local definition is
$$\lambda_{\mathrm{RS}} := (\varphi-1)^2/\varphi.$$
The golden ratio satisfies $\varphi>1$ (lemma one_lt_phi, already proved in Constants / PhiSupport) and $\varphi>0$. The module’s headline result is the fully proved identity $A_{\mathrm{corrected}}=9/11$ for the Wolfenstein $A$, within $0.6\sigma$ of PDG; §8 then introduces the Cabibbo $\lambda$ from the same φ-ladder.
proof idea
One-line term proof. Mathlib div_pos needs a positive numerator and a positive denominator. The denominator is phi_pos. The numerator $(\varphi-1)^2$ is handled by a short nlinarith call on phi_pos and one_lt_phi: $\varphi>1$ forces $\varphi-1>0$, so the square is positive. No further lemmas are required.
why it matters
Positivity of $\lambda_{\mathrm{RS}}$ is the elementary gate for any subsequent inequality or normalisation that treats the φ-ladder Cabibbo angle as a positive scale in the CKMExact development. The parent module derives Wolfenstein $A$ from Q₃ face-flux correction ($A_{\mathrm{corrected}}=9/11$) and ties the same chirality data to $\alpha^{-1}$ and $\eta_B$ via the factor 44. The φ that appears here is the self-similar fixed point forced at T6 of the UnifiedForcingChain. No downstream theorems currently cite this lemma (used_by empty), so it is infrastructure for the §8 Cabibbo block rather than a cited step in a larger proved chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.