module module

`IndisputableMonolith.RecogSpec.RSBridge`

show as: view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

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