V_us_from_bridge
plain-language theorem explainer
V_us_from_bridge computes the Cabibbo mixing angle from a golden-ratio projection minus a linear radiative correction. It is invoked in derivations of the full CKM matrix from ledger geometry and in the canonical specialization theorem. The definition is a direct one-line arithmetic expression on the phiProj, radCoeff, and alphaExponent fields of an RSBridge structure.
Claim. $V_{us}(B,φ) = φ^{k} - c·α^{e}$, where $k$ is the golden projection exponent of bridge $B$, $c$ its radiative correction coefficient, and $e$ its fine-structure exponent. For the standard parameters this yields $φ^{-3} - (3/2)α$.
background
The RSBridge structure augments a minimal Bridge with geometric fields that fix the CKM angles: edgeDual (default 24), alphaExponent for V_ub, phiProj (default -3) for the Cabibbo angle, and radCoeff (default 3/2). The module states that mixing angles are derived from ledger geometry rather than introduced as free parameters. Upstream, the canonical ledger L and the arithmetic canonical object supply the invariant arithmetic content used to interpret the exponents.
proof idea
One-line definition that directly evaluates the arithmetic expression φ raised to B.phiProj minus B.radCoeff times B.alphaExponent, using the three relevant fields of the supplied RSBridge structure.
why it matters
The definition supplies the V_us component to mixingFromCycles, which assembles the full CkmMixingAngles triple, and is specialized by the theorem canonical_V_us to the explicit formula φ^{-3} - (3/2)α. It thereby realizes the module claim that the Cabibbo angle arises from φ-ladder projection with electromagnetic correction, consistent with the phi fixed-point and eight-tick octave of the Recognition framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.