module module

`IndisputableMonolith.Gravity.SevenGaps.Gap5MomentumMagnitudeBridge`

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.Gap5EnergyEqualsCostDerivation module_import

depends on (2)

Lean names referenced from this declaration's body.

IndisputableMonolith.Gravity.SevenGaps.DynamicStructureBracket module_import
IndisputableMonolith.Gravity.SevenGaps.Gap5MomentumAdditivity module_import

declarations in this module (32)

lemma sum_zmod2 L64
def EnergyEqualsCost L74
def KineticOnOpenPositiveQuadrant L77
def KineticOnClosedPositiveQuadrant L80
theorem exp_log_div_two L85
theorem sqrt_mul_sqrt_div L96
theorem exp_neg_log_div_two L111
theorem orbit_fst L120
theorem orbit_snd L124
theorem orbit_coverage L132
theorem energy_equals_cost_implies_kinetic_on_open_positive L147
theorem balance_vanishing_on_positive_diagonal_of_energy_equals_cost L157
theorem continuous_imbalance L168
theorem kinetic_extends_to_closed_positive_quadrant L172
theorem energy_equals_cost_continuous_implies_kinetic_on_closed L203
theorem swap_odd_preserves_kinetic_pointwise L211
theorem swap_maps_open_positive_to_itself L217
theorem orbitPoint_nonneg L222
theorem negative_quadrant_not_on_orbit L228
theorem hamDyn_decoy_value L239
theorem hamDyn_gradient_sector_nonzero_at_zero_momenta L257
theorem Jlog_ne_half_sq L268
theorem chart_product_sq_form L321
theorem exact_cost_profile_recovers_chart_product L337
theorem energy_equals_cost_of_imbalance L356
theorem chart_product_fails_for_imbalance_at_unit_lam L364
theorem orbitPoint_pos L386
theorem open_positive_kinetic_iff_energy_equals_cost L396
theorem two_imbalance_fails_energy_equals_cost L413
theorem two_imbalance_package L440
structure MomentumMagnitudeBridgeVerdict L461
theorem momentumMagnitudeBridgeVerdict L514