canonical_V_ub
plain-language theorem explainer
The declaration shows that the up-bottom CKM element extracted from the canonical rich bridge equals half the locked fine-structure constant. A physicist deriving CKM parameters from Recognition Science ledger geometry would cite this to fix V_ub at the predicted value alphaLock/2. The proof reduces immediately to the definitions of the bridge constructor and the V_ub extractor by a single simplification step.
Claim. For any RSLedger $L$, if $B$ is the canonical rich bridge over $L$, then the up-bottom mixing element satisfies $V_{ub}(B) = {alphaLock}/2$, where $alphaLock := (1 - phi^{-1})/2$ is the locked fine-structure constant.
background
The RSBridge module constructs a rich bridge structure that encodes geometric couplings for CKM mixing angles rather than treating them as free parameters. The extractor V_ub_from_bridge is defined to return the bridge's alphaExponent divided by two, while alphaLock supplies the explicit algebraic form $(1 - 1/phi)/2$ for the fine-structure constant in RS units. The canonical bridge is assembled from the arithmetic canonical object together with forcing and gap-beat structures.
proof idea
The proof applies the simp tactic directly to the definitions of V_ub_from_bridge and canonicalRSBridge. This unfolds the alphaExponent field of the canonical bridge to alphaLock and performs the division by two, producing the equality with no additional lemmas or computation.
why it matters
This result supplies the explicit leading value for the smallest CKM element, realizing the geometric prediction V_ub = alpha/2 stated in the module. It completes the derivation of the three mixing angles from ledger counts (24 edges for V_cb, phi-projection for V_us) and feeds the alpha band of the Recognition framework. The declaration closes the canonical case for the first-to-third generation mixing without introducing new hypotheses.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.