module module

`IndisputableMonolith.RecogSpec.BridgeDerivation`

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

depends on (3)

Lean names referenced from this declaration's body.

IndisputableMonolith.Constants module_import
IndisputableMonolith.RecogSpec.ObservablePayloads module_import
IndisputableMonolith.RecogSpec.RSBridge module_import

declarations in this module (5)

def mixingFromCycles L39
def g2FromLoops L48
theorem mixingFromCycles_Vcb_canonical L52
theorem g2FromLoops_canonical L57
theorem canonical_g2FromLoops L63