V_ub_from_bridge
plain-language theorem explainer
V_ub_from_bridge extracts the up-bottom CKM mixing element directly as half the fine-structure exponent stored inside an RSBridge. Researchers deriving CKM parameters from ledger geometry in Recognition Science would cite this when assembling mixing angles from geometric couplings. The definition performs a single field projection followed by division by two.
Claim. For an RSBridge $B$, the up-bottom CKM element is given by $V_{ub}(B) = alpha_B / 2$, where $alpha_B$ is the fine-structure exponent field of $B$.
background
The RSBridge structure augments a basic ledger bridge with geometric coupling fields, including edgeDual (default 24), alphaExponent for the smallest mixing angle, phiProj for the Cabibbo projection, and a radiative correction coefficient. In this module, CKM mixing angles are obtained from ledger geometry rather than free parameters: V_ub comes from the fine-structure coupling, V_cb from the cube-dual edge count, and V_us from a golden projection minus electromagnetic correction. Upstream results on primitive distinctions and simplicial ledgers supply the geometric counts that justify storing these exponents inside the bridge.
proof idea
The definition is a one-line field projection that returns the alphaExponent component of the supplied RSBridge divided by two.
why it matters
This definition supplies the V_ub component to mixingFromCycles, which assembles the full set of CKM angles from bridge cycle structure. It realizes the module claim that mixing angles derive from geometric counts (24 edges, phi-ladder projection) instead of arbitrary parameters, consistent with Recognition Science extraction of constants from the phi-ladder and eight-tick octave. The canonical_V_ub theorem later specializes the same expression to the locked alpha value.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.