module module

`IndisputableMonolith.Gravity.SevenGaps.Gap5MomentumBridge`

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.Gravity.SevenGaps.Gap5MomentumBridgeHostileProbe module_import

depends on (1)

Lean names referenced from this declaration's body.

IndisputableMonolith.Gravity.SevenGaps.Gap5NetImbalanceDerivation module_import

declarations in this module (28)

def scaledImbalance L106
theorem scaledImbalance_continuous L110
theorem scaledImbalance_swapOdd L113
theorem scaledImbalance_additive L119
theorem scaledImbalance_balance_vanishing L125
theorem scaledImbalance_postingIncidence L131
theorem scaledImbalance_readsNet L138
theorem scaledImbalance_additiveOnDebitAxis L143
theorem scaledImbalance_conjugate_bracket L154
theorem scaledImbalance_unit_sq L161
theorem kineticCondition_on_ray_iff L167
theorem energyEqualsCost_on_ray_iff L182
theorem unit_norm_on_ray_iff L212
structure ScaleFreeMomentumPackage L222
theorem scaleFreePackage_on_ray L244
theorem bridge_not_forced_by_scale_free_package L267
theorem exhibited_pair_disagrees_on_bridge L291
theorem sign_not_forced_with_unit_scale L306
theorem chart_product_of_stipulated_chart L332
theorem imbalance_orbitPoint_at_two_arsinh_one L348
theorem lam_of_signed_bridge L359
theorem lam_of_signed_bridge_at_stipulated_chart L378
theorem lam_sq_of_magnitude_bridge L390
theorem constants_cluster_of_magnitude_bridge L427
theorem lam_ground_state_of_signed_bridge L438
theorem ground_state_cluster_of_signed_bridge L446
structure MomentumBridgeVerdict L464
theorem momentumBridgeVerdict L509