pith. sign in
module module high

IndisputableMonolith.RecogSpec.RSBridge

show as:
view Lean formalization →

RSBridge supplies geometric constructions from the 3-cube to CKM mixing angles inside Recognition Science. It defines cubeEdges as the 12 edges together with dual counts, cabibboProjection, radiativeCoeff, and the V_xx_from_bridge maps that link the φ-tier ledger to observable parameters. The module is cited by derivations of mixing angles and g-2. Its content is a set of definitions and short equalities that connect the rich ledger to bridge geometry.

claimCube edge count equals 12. Projections from dual edge counts on the 3-cube yield Cabibbo angle and CKM elements $V_{us}$, $V_{cb}$, $V_{ub}$ via the φ-ladder ledger.

background

The module sits inside RecogSpec and imports Constants (where τ₀ equals one RS tick), Core, and RSLedger. RSLedger supplies the rich ledger in which particle masses occupy discrete rungs on the φ-ladder and mass ratios arise from generation torsion rather than explicit φ-formulas. Core supplies the underlying specification language. The bridge geometry uses the 3-cube whose 12 edges and dual counts furnish projections for mixing angles.

proof idea

This is a definition module. It introduces cubeEdges as the edge count of the 3-cube, states edgeDualCount together with its equality lemma, then defines cabibboProjection and radiativeCoeff, and assembles the RSBridge object and the three V_xx_from_bridge functions.

why it matters in Recognition Science

The module feeds BridgeDerivation, which derives the canonical mixing-angle payload CkmMixingAngles and g-2 from RSBridge geometry with mixingAngles = { vus := V_us, vcb := V_cb, vub := V_ub }. It supplies the geometric step that converts the φ-ladder ledger into CKM parameters inside the Recognition framework.

scope and limits

used by (1)

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

depends on (3)

Lean names referenced from this declaration's body.

declarations in this module (19)