module module

`IndisputableMonolith.Gravity.SevenGaps.Gap5MomentumAdditivity`

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

depends on (1)

Lean names referenced from this declaration's body.

IndisputableMonolith.Gravity.SevenGaps.Gap5ChartFromLedgerMomentum module_import

declarations in this module (21)

def KineticCondition L99
def SwapOdd L105
theorem imbalance_swap L108
theorem imbalance_add L113
theorem imbalance_smul L118
theorem imbalance_seg_pos L125
theorem imbalance_seg_neg L144
theorem no_sign_change_on_unit_interval L165
theorem sign_const_pos L195
theorem sign_const_neg L240
theorem balance_vanishing_of_kinetic L291
theorem kinetic_root_classification L305
theorem kinetic_root_mem_four L332
theorem kinetic_root_additive_iff L393
theorem kinetic_root_additive_iff_swap_odd L427
theorem momentum_additivity_from_swap L461
theorem kinetic_on_orbit L486
theorem nlP_countermodel L500
theorem abs_countermodel L533
structure MomentumAdditivityVerdict L563
theorem momentumAdditivityVerdict L604