ckm_unitarity_structural
plain-language theorem explainer
The theorem establishes that the sum of squares of the RS-derived CKM elements V_us, V_cb, V_ub is strictly less than one. Flavor physicists comparing geometric quark-mixing predictions to experimental unitarity bounds would cite this result. The proof unfolds the three element definitions, invokes the bound cabibbo_parameter < 1 derived from one_lt_phi, and closes with a single nlinarith invocation on non-negative squares.
Claim. Let $c = phi^{-11}$. Define the RS CKM elements by $V_{us} := c$, $V_{cb} := c^2$, $V_{ub} := c^3$. Then $V_{us}^2 + V_{cb}^2 + V_{ub}^2 < 1$.
background
The module derives CKM matrix elements from torsion mismatch on the Q3 cube using the generation schedule {0, 11, 17}. The Cabibbo parameter is defined as phi^{-11} and the three RS elements are obtained by successive powers: rs_V_us equals the parameter itself, rs_V_cb its square, and rs_V_ub its cube. The local setting is the torsion-geometry approach to flavor mixing described in the module header, which treats sin theta_C as phi^{-(tau1 - tau0)}.
proof idea
The tactic proof first unfolds rs_V_us, rs_V_cb, rs_V_ub. It obtains cabibbo_parameter_pos and then proves cabibbo_parameter < 1 by rewriting the negative exponent and applying inv_lt_one_of_one_lt together with one_lt_phi and ring normalization. The final step applies nlinarith to the three non-negative squares of cabibbo_parameter, cabibbo_parameter^2, and cabibbo_parameter^3.
why it matters
The inequality supplies the unitarity_bound field of the CKMCert record constructed by the downstream theorem ckm_cert_exists. It closes one structural requirement in the CKM derivation from phi-geometry and the eight-tick octave, confirming that the torsion-derived hierarchy remains inside the unit disk. The result sits inside the broader program that obtains all particle masses and mixings from the phi-ladder without additional parameters.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.