cabibbo_parameter_pos
plain-language theorem explainer
The Cabibbo parameter equals phi to the power minus eleven and is strictly positive. Flavor physicists citing the Recognition Science derivation of CKM elements from torsion geometry rely on this to fix the sign of the leading mixing parameter. The proof is a one-line wrapper that unfolds the definition and invokes the positivity of integer powers of a positive base.
Claim. $0 < phi^{-11}$, where $phi$ is the golden ratio fixed point.
background
The CKM Derivation module addresses whether the CKM matrix elements can be derived from phi-geometry and the generation torsion schedule {0, 11, 17}. Mixing arises from torsion mismatch between up-type and down-type sectors on the Q3 cube, with the Cabibbo angle determined by sin(theta_C) approx phi^{-(tau1 - tau0)} = phi^{-11}. The upstream definition supplies cabibbo_parameter as phi raised to minus eleven.
proof idea
Unfold the definition of the Cabibbo parameter to obtain phi to the minus eleven, then apply the lemma establishing that a positive base raised to any integer power remains positive.
why it matters
This positivity result is invoked in the ckm_hierarchy theorem to prove the ordering rs_V_ub < rs_V_cb < rs_V_us and in ckm_unitarity_structural to bound the sum of squares below one. It fills the sign requirement in the CKM matrix derivation from Torsion Geometry (Q6), consistent with the phi-ladder and the self-similar fixed point phi in the Recognition Science forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.