V_us_exp
plain-language theorem explainer
V_us_exp supplies the experimental central value 0.22500 for the CKM matrix element |V_us| in the Recognition Science derivation of quark mixing angles. It functions as the benchmark datum against which the geometric prediction V_us_pred = phi^{-3} - (3/2) alpha is tested inside CKMElementScoreCardCert and row_V_us. The declaration is a direct constant assignment with no internal derivation or lemmas.
Claim. The experimental central value of the Cabibbo-Kobayashi-Maskawa matrix element satisfies $|V_{us}|_exp = 0.22500$.
background
The CKMGeometry module formalizes T11, deriving CKM elements from cubic ledger geometry and the fine-structure constant. The hypothesis gives |V_us| (theta_12, Cabibbo angle) via the golden projection |V_us| = phi^{-3} - (3/2) alpha, yielding the numerical prediction 0.2251. V_us_exp supplies the measured central value 0.22500 for direct comparison; the associated error bound appears in the sibling V_us_err. Upstream interval results on phi^{-3} and alpha (from PhiBounds and AlphaBounds) are invoked only in the downstream matching theorem.
proof idea
One-line definition that directly assigns the real constant 0.22500. No lemmas, tactics, or reductions are applied.
why it matters
This definition supplies the experimental anchor for the T11 CKM geometry claim that mixing angles arise from ledger couplings rather than free parameters. It is referenced by CKMElementScoreCardCert (which certifies all three elements within error) and by row_V_us (which reduces to V_us_match). The construction closes the comparison loop between the phi-ladder prediction and observed quark mixing, consistent with the eight-tick octave and D=3 spatial structure of the parent framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.