IndisputableMonolith.Gravity.SevenGaps.Gap5PhysicalMomentum

declarations in this module (19)

• def physicalMomentum L95
• theorem physicalMomentum_eq_imbalance L97
• theorem physicalMomentum_def L100
• theorem physicalMomentum_posting_incidence L108
• theorem physicalMomentum_on_debit_axis L118
• theorem physicalMomentum_additiveOnDebitAxis L125
• theorem physicalMomentum_readsNetImbalance L132
• theorem physicalMomentum_swap_odd L138
• theorem physicalMomentum_continuous L143
• theorem physicalMomentum_unit L146
• theorem physicalMomentum_balance_vanishing L151
• theorem physicalMomentum_additive L157
• theorem energyEqualsCost_of_physicalMomentum L170
• theorem physicalMomentum_inhabits_posting_package L185
• theorem over L204
• theorem cubeDiff_is_not_physicalMomentum L209
• theorem net_charge_selected_among_incident L217
• structure PhysicalMomentumVerdict L234
• theorem physicalMomentumVerdict L255