V_ub_from_bridge
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.
claimFor 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 in Recognition Science
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.
scope and limits
- Does not derive or compute the numerical value of the fine-structure constant.
- Does not enforce bounds or positivity on the stored exponent.
- Does not incorporate higher-order radiative corrections beyond the stored coefficient.
- Does not construct the full CKM matrix or verify unitarity.
Lean usage
V_ub_from_bridge (canonicalRSBridge L)formal statement (Lean)
98noncomputable def V_ub_from_bridge (B : RSBridge L) : ℝ := B.alphaExponent / 2
proof body
Definition body.
99
100/-- V_us from golden projection with radiative correction: φ^{-3} - (3/2)α
101
102The Cabibbo angle is a golden projection minus electromagnetic correction.
103-/