module module high

`IndisputableMonolith.RecogSpec.RSBridge`

The RSBridge module supplies geometric definitions including the cube's 12 edges, dual edge counts, Cabibbo projection, and radiative coefficients to connect Recognition Science structures to CKM mixing angles. It defines an RSBridge object and extraction functions for V_cb, V_ub, and V_us. The module is imported by BridgeDerivation to produce canonical mixing angles. All content consists of definitions with no proofs.

claimThe module defines a cube with 12 edges, an associated dual count, a Cabibbo projection map, a radiative coefficient, and an RSBridge structure from which the CKM elements $V_{cb}$, $V_{ub}$, and $V_{us}$ are extracted via bridge geometry.

background

Constants supplies the RS time quantum $ au_0 = 1$ tick. RSLedger states: "This module defines the rich ledger structure needed for deriving mass ratios from generation torsion rather than defining them as $\phi$-formulas. In Recognition Science, particle masses occupy discrete rungs on the $\phi$-ladder." Core provides supporting recognition primitives. The RSBridge module builds on these imports to introduce cube-based geometry for mixing-angle extraction.

proof idea

this is a definition module, no proofs

why it matters in Recognition Science

This module feeds BridgeDerivation, which derives the canonical mixing-angle payload CkmMixingAngles with mixingAngles = { vus := V_us, vcb := V_cb, vub := V_ub } and g-2 from RSBridge geometry. It supplies the geometric layer required for CKM parameters within the Recognition Science framework.

scope and limits

Does not derive numerical values for the mixing angles.
Does not construct the full CKM matrix.
Does not address g-2 or anomalous magnetic moments.
Does not connect directly to the $\phi$-ladder mass formulas.

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