module module moderate

`IndisputableMonolith.RecogSpec.RSBridge`

RSBridge supplies definitions for cube edge counts and bridge projections that map the Recognition Science phi-ladder to CKM mixing angles. Researchers deriving first-principles mixing parameters cite these constructs. The module contains multiple definitions and lemmas that link the ledger to observable angles without complex proofs.

claimThe cube has 12 edges. The RS bridge structure yields mixing angles $V_{us}$, $V_{cb}$, $V_{ub}$ via Cabibbo projection and radiative coefficients applied to the ledger.

background

The module imports the time quantum $ au_0 = 1$ tick from Constants and the rich ledger from RSLedger. The ledger places particle masses on discrete rungs of the $\phi$-ladder derived from generation torsion rather than as explicit $\phi$-formulas. It introduces cube edge count, dual counts, Cabibbo projection, radiative coefficient, the RSBridge object itself, and extraction functions for the mixing angles.

proof idea

this is a definition module, no proofs

why it matters in Recognition Science

The module supplies the RSBridge geometry that BridgeDerivation uses to derive the canonical mixing-angle payload CkmMixingAngles and g-2. It provides the bridge between the phi-ladder and observable mixing angles in the Recognition Science framework.

scope and limits

Does not include proofs of the mixing angle derivations.
Does not specify numerical predictions for the angles.
Does not connect to the full CKM matrix unitarity.
Does not address g-2 anomaly directly.

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

IndisputableMonolith.RecogSpec.BridgeDerivation module_import

depends on (3)

Lean names referenced from this declaration's body.

IndisputableMonolith.Constants module_import
IndisputableMonolith.RecogSpec.Core module_import
IndisputableMonolith.RecogSpec.RSLedger module_import

declarations in this module (19)

def cubeEdges L42
def edgeDualCount L45
theorem edgeDualCount_eq L47
def cabibboProjection L50
def radiativeCoeff L53
structure RSBridge L62
def V_cb_from_bridge L84
theorem V_cb_canonical L87
def V_cb_real L92
def V_ub_from_bridge L98
def V_us_from_bridge L104
def canonicalRSBridge L110
theorem canonicalRSBridge_edgeDual L118
theorem canonicalRSBridge_alpha L122
theorem canonical_V_cb L128
theorem canonical_V_ub L133
theorem canonical_V_us L138
theorem mixingAngles_geometric_origin L154
theorem V_cb_approx L166