row_V_us
plain-language theorem explainer
The theorem certifies that the Recognition Science geometric prediction for the CKM element V_us lies inside the one-sigma experimental band. A physicist constructing CKM fits or testing mixing-angle derivations from the golden ratio would invoke this check. The entire proof consists of a direct reference to the matching result already proved in the geometry submodule.
Claim. The inequality holds: $|V_{us}^{pred} - 0.22500| < 0.00067$, where $V_{us}^{pred} = φ^{-3} - (3/2)α$.
background
The CKMElementScoreCard module collects row theorems that verify the three leading CKM magnitudes against PDG data. V_us_pred is defined in the imported CKMGeometry module as the difference between the torsion overlap and the Cabibbo radiative correction, which simplifies to φ^{-3} - (3/2)α. The constants V_us_exp = 0.22500 and V_us_err = 0.00067 are hard-coded numerical values.
proof idea
This is a one-line wrapper that applies the theorem V_us_match from CKMGeometry. The proof term is exactly the identifier V_us_match, which discharges the goal without further reduction.
why it matters
The result populates the vus component of the certificate produced by ckmElementScoreCardCert_holds. It thereby contributes to the partial theorem status for the CKM predictions listed in the module documentation. The construction relies on the Recognition Science constants phi and alpha lying in their certified intervals, consistent with the eight-tick octave and D=3 spatial dimensions of the underlying forcing chain. The module notes that Wolfenstein packings remain separate.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.