canonicalRSBridge
plain-language theorem explainer
The canonical RS bridge for ledger L supplies the geometric parameters edge dual count 24, alpha exponent alphaLock, phi projection -3 and radiative coefficient 3/2 that fix the CKM mixing angles from ledger geometry. Researchers deriving CKM matrix elements from Recognition Science geometry cite this definition. It is a direct structure construction that assigns the standard values without further computation.
Claim. Let $L$ be an RSLedger. The canonical RS bridge is the RSBridge structure whose underlying bridge comes from the ledger, with edge dual count 24, fine-structure exponent $alphaLock = (1 - 1/phi)/2$, golden projection exponent -3, and radiative correction coefficient $3/2$.
background
The module defines RSBridge as a structure extending the minimal Bridge with geometric fields that determine CKM mixing angles from ledger geometry rather than arbitrary parameters. RSBridge carries toBridge : Bridge L.toLedger, edgeDual : Nat (default edgeDualCount), alphaExponent : Real, phiProj : Int (default cabibboProjection), and radCoeff : Real (default 3/2). The local setting states that V_ub equals alphaLock/2 from the fine-structure coupling, V_cb equals 1/24 from the cube dual edge count, and V_us equals phi^{-3} minus (3/2) alphaLock from the golden projection with radiative correction.
proof idea
This is a direct definition that constructs the RSBridge record by assigning toBridge to the ledger bridge, edgeDual to 24, alphaExponent to alphaLock, phiProj to -3, and radCoeff to 3/2.
why it matters
This definition supplies the canonical parameters used by downstream results such as canonical_V_cb which shows V_cb = 1/24, canonical_V_ub showing V_ub = alphaLock/2, canonical_V_us showing the phi^{-3} formula, and canonical_g2FromLoops deriving g-2 = 1/phi^5. It fills the geometric coupling step in the Recognition Science derivation of CKM angles from ledger geometry rather than arbitrary parameters, consistent with the phi-ladder and alpha band in the framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.