canonical_V_us
plain-language theorem explainer
The theorem states that the Cabibbo mixing element extracted from the canonical recognition bridge on any ledger equals phi to the power minus three minus three-halves times the locked fine-structure constant. Researchers deriving CKM parameters from geometric ledger counts in Recognition Science would cite this when confirming the golden-projection formula. The proof is a direct simplification that unfolds the bridge definition and the canonical parameter settings.
Claim. For any recognition ledger $L$, the Cabibbo mixing element obtained from the canonical recognition-science bridge evaluated at the golden ratio $phi$ equals $phi^{-3} - (3/2) alpha_lock$, where $alpha_lock$ is the locked fine-structure constant $(1 - 1/phi)/2$.
background
The RSBridge module constructs a geometric structure whose parameters encode ledger edge counts and phi-ladder projections to derive CKM mixing angles. V_us_from_bridge extracts the first-second generation mixing as a golden projection minus a radiative correction term proportional to the locked fine-structure constant. The module documentation states that V_us arises specifically as phi to the minus three minus three-halves alpha, matching the observed Cabibbo angle near 0.225, while V_cb and V_ub follow from separate edge-dual and alpha couplings.
proof idea
The proof is a one-line wrapper that applies simp to unfold V_us_from_bridge and canonicalRSBridge, substituting the fixed phi-projection exponent minus three, the radiative coefficient three-halves, and the alphaLock definition directly into the target equality.
why it matters
This result supplies the explicit V_us formula inside the RSBridge construction, confirming that the Cabibbo angle follows from phi-ladder projection with electromagnetic correction rather than being inserted by hand. It completes the geometric derivation of all three CKM elements listed in the module documentation and aligns with the Recognition Science landmarks of phi self-similarity and the alpha band. No downstream theorems currently reference it.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.