module module

`IndisputableMonolith.Gravity.SevenGaps.LedgerBridgeNoGo`

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 (2)

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

IndisputableMonolith.Gravity.SevenGaps.CampaignLedger module_import
IndisputableMonolith.Gravity.SevenGaps.RecognitionRatioBridge module_import

depends on (3)

Lean names referenced from this declaration's body.

IndisputableMonolith.Cost module_import
IndisputableMonolith.Gravity.LedgerToGeometryBridge module_import
IndisputableMonolith.Gravity.RecognitionLedger module_import

declarations in this module (16)

theorem bridge_forces_nonneg_geometricDeficit L73
theorem no_bridge_matches_negative_deficit_spec L89
theorem Jcost_ratio_parity L109
def jRatioCellCost L118
def jRatioDeficit L125
theorem jRatioCellCost_even L131
theorem jRatioDeficit_even L145
theorem even_and_odd_forces_zero L153
theorem no_jRatio_deficit_linear_response L169
theorem ledger_family_deficit_even_of_ratio_parity L193
theorem no_ledger_family_linear_response L212
def twoCellStrain L243
theorem twoCell_jRatioDeficit L249
structure LedgerBridgeNoGoStatus L272
def ledgerBridgeNoGoStatus L284
theorem ledgerBridgeNoGoStatus_flags L290