RSBridge
plain-language theorem explainer
RSBridge extends the base Bridge on an RSLedger by adding fields that fix CKM mixing angles from geometric ledger counts. Researchers deriving quark masses or CKM phenomenology from Recognition Science cite it to replace free parameters with the dual-edge count 24 for V_cb and the phi-projection with radiative correction for V_us. The declaration is a plain structure definition that assembles the base bridge with four geometric fields and supplies defaults from sibling functions edgeDualCount, cabibboProjection and radiativeCoeff.
Claim. Let $L$ be an RSLedger. The structure $RSBridge(L)$ consists of a base bridge $toBridge : Bridge(L.toLedger)$, an integer edge-dual count $edgeDual$, a real fine-structure exponent $alphaExponent$, an integer golden-projection exponent $phiProj$, a rational radiative coefficient $radCoeff$, and a natural-number loop order $loopOrder$.
background
In Recognition Science the CKM matrix elements are obtained from ledger geometry rather than inserted as free parameters. The base Bridge on an RSLedger supplies the minimal ledger-to-physics map; RSBridge augments it with fields whose values are fixed by geometric counts: dual-edge number (default 24), fine-structure exponent, Cabibbo projection power (default -3), radiative coefficient (default 3/2), and loop order (default 5). Upstream LedgerFactorization.of calibrates the J-cost on the underlying ledger while CrystalStructure and PeriodicTable provide the discrete geometric scaffolding that later forces the gap function.
proof idea
The declaration is a structure definition that directly assembles the base Bridge with the listed geometric fields and assigns default values via the sibling definitions edgeDualCount, cabibboProjection and radiativeCoeff. No lemmas or tactics are invoked; the body simply declares the six fields and their optional defaults.
why it matters
RSBridge supplies the geometric coupling data consumed by downstream mass and gap calculations, notably the affine-log collapse theorems in GapFunctionForcing that identify the canonical gap with RSBridge.gap. It realizes the module claim that mixing angles are derived from 24-edge duals and phi-ladder projections rather than free parameters, feeding the quark mass ladder and CKM phenomenology. The structure closes the interface between the minimal Bridge and the phi-forced constants used in the T5-T8 forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.