module module

`IndisputableMonolith.Gravity.SevenGaps.Gap5MomentumAdditivityComposition`

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

depends on (2)

Lean names referenced from this declaration's body.

IndisputableMonolith.Cost.SymplecticAction module_import
IndisputableMonolith.Gravity.SevenGaps.Gap5EnergyEqualsCostDerivation module_import

declarations in this module (26)

theorem chart_cost_satisfies_composition_law L101
theorem composition_law_ignores_momentum L107
theorem imbalance_unit L113
theorem imbalance_balance_vanishing L116
theorem abs_imbalance_continuous L120
theorem abs_imbalance_balance_vanishing L123
theorem abs_imbalance_unit L128
theorem abs_imbalance_not_additive L135
theorem imbalance_additive_package L149
theorem abs_imbalance_package L164
theorem momentum_additivity_independent_of_composition_law L186
def nlPUnit L204
theorem nlPUnit_continuous L206
theorem nlPUnit_swap_odd L211
theorem nlPUnit_balance_vanishing L218
theorem nlPUnit_unit L224
theorem nlPUnit_not_additive L227
theorem nlPUnit_package L243
def ReadsNetImbalance L256
def AdditiveOnDebitAxis L260
theorem balance_vanishing_of_net_imbalance_reading L264
theorem continuous_additive_real L278
theorem energyEqualsCost_of_net_imbalance_reading_additive_unit L298
theorem imbalance_reads_net_and_additive_on_axis L330
structure MomentumAdditivityCompositionVerdict L352
theorem momentumAdditivityCompositionVerdict L381