V_us_match
plain-language theorem explainer
The theorem establishes that the predicted Cabibbo element |V_us| obtained from the golden projection phi to the minus three minus three-halves alpha lies inside the experimental one-sigma interval of width 0.00067 centered at 0.22500. CKM phenomenology groups would cite the result when testing ledger-derived mixing angles against measured values. The proof extracts four pre-proved interval bounds on alpha and phi inverse three, simplifies the target expression, and closes the absolute-difference inequality by linear arithmetic.
Claim. $|V_{us}^{pred} - V_{us}^{exp}| < V_{us}^{err}$ where $V_{us}^{pred} = phi^{-3} - (3/2) alpha$, $V_{us}^{exp} = 0.22500$ and $V_{us}^{err} = 0.00067$.
background
In the CKM Geometry module the Cabibbo element is defined as the golden projection torsion_overlap minus the radiative correction cabibbo_radiative_correction, which the module comment identifies with phi to the minus three minus three-halves alpha. The module derives the three CKM magnitudes from geometric couplings on the cubic ledger, with V_us corresponding to the golden projection. Upstream results supply the interval theorems alpha_lower_bound, alpha_upper_bound, phi_inv3_lower_bound and phi_inv3_upper_bound; these bounds are required because alpha and phi involve transcendental functions outside the reach of norm_num.
proof idea
The proof first obtains the four interval theorems alpha_lower_bound, alpha_upper_bound, phi_inv3_lower_bound and phi_inv3_upper_bound. It simplifies the goal with the definitions of V_us_pred, V_us_exp, V_us_err, torsion_overlap and cabibbo_radiative_correction. Four auxiliary inequalities bounding the predicted value between 0.225035 and 0.225165 are established by linarith. The absolute-value form is rewritten via abs_lt and the final comparison is discharged by linarith.
why it matters
This result supplies the V_us row of the CKM element scorecard, confirming the golden-projection formula matches experiment to better than one sigma. It completes the T11 CKM Matrix Geometry verification alongside the exact rational V_cb = 1/24 and the alpha-derived V_ub. The parent theorem row_V_us directly invokes it. Within the Recognition framework it closes one of the three CKM predictions required by the cubic-ledger geometry of T11.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.