vus_derived
plain-language theorem explainer
The declaration establishes that the predicted Cabibbo matrix element equals the golden projection overlap minus the radiative correction term. CKM modelers working in the Recognition Science geometric program cite it to anchor the origin of |V_us| in cubic ledger topology. The proof is a one-line wrapper that unfolds the three definitions and closes by reflexivity.
Claim. $|V_{us}| = phi^{-3} - (3/2) alpha$, where $phi^{-3}$ is the overlap of the 3-generation torsion constraint on the cubic ledger and $(3/2) alpha$ is the radiative correction fixed by the six faces of the cube.
background
The module derives CKM and PMNS mixing elements from the cubic ledger via edge-dual coupling of 8-tick windows. Torsion overlap encodes the geometric factor from the 3-generation constraint on the simplicial ledger. The radiative correction coefficient 3/2 arises directly from cube-face topology. Upstream, the definition of V_us_pred in CKMGeometry sets the predicted value exactly as this difference. Related upstream results include the phi-ladder finite-N correction for quantum channel capacity and the simplicial ledger edge-length theorem.
proof idea
The term-mode proof unfolds V_us_pred, torsion_overlap, and cabibbo_radiative_correction, then applies reflexivity to obtain the equality.
why it matters
This supplies the explicit equality invoked by the downstream CKMElementScoreCard row that verifies geometric predictions against data. It completes the |V_us| derivation step in the Phase 7.2 mixing-matrix program, connecting to the eight-tick octave and cubic topology that force three spatial dimensions. The parent scorecard theorem applies it directly to populate the verification row.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.