V_us_match
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 in Recognition Science
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.
scope and limits
- Does not derive the expression for V_us_pred from the ledger axioms.
- Does not compute the numerical value of phi or alpha inside the proof.
- Does not extend the match beyond the supplied experimental error bar.
- Does not address higher-order radiative corrections.
formal statement (Lean)
165theorem V_us_match : abs (V_us_pred - V_us_exp) < V_us_err := by
proof body
Tactic-mode proof.
166 have h_alpha_lower := alpha_lower_bound
167 have h_alpha_upper := alpha_upper_bound
168 have h_phi3_lower := phi_inv3_lower_bound
169 have h_phi3_upper := phi_inv3_upper_bound
170 simp only [V_us_pred, V_us_exp, V_us_err, torsion_overlap, cabibbo_radiative_correction]
171 -- V_us_pred = phi^(-3) - 1.5*alpha
172 -- phi^(-3) ∈ (0.2360, 0.2361)
173 -- 1.5*alpha ∈ (0.010935, 0.010965)
174 -- V_us_pred ∈ (0.2360 - 0.010965, 0.2361 - 0.010935) = (0.225035, 0.225165)
175 have h_correction_lower : (0.010935 : ℝ) < (3/2) * Constants.alpha := by linarith
176 have h_correction_upper : (3/2) * Constants.alpha < (0.010965 : ℝ) := by linarith
177 have h_pred_lower : (0.225035 : ℝ) < Constants.phi ^ (-3 : ℤ) - (3/2) * Constants.alpha := by linarith
178 have h_pred_upper : Constants.phi ^ (-3 : ℤ) - (3/2) * Constants.alpha < (0.225165 : ℝ) := by linarith
179 -- |V_us_pred - 0.22500| ≤ max(|0.225035 - 0.22500|, |0.225165 - 0.22500|)
180 -- = max(0.000035, 0.000165) = 0.000165 < 0.00067
181 rw [abs_lt]
182 constructor <;> linarith
183
184/-! ## Certificate -/
185
186/-- T11 Certificate: V_cb from cube edge geometry. -/