IndisputableMonolith.Gravity.SevenGaps.Gap5NetImbalanceDerivation

declarations in this module (25)

• def PostingIncidence L58
• theorem axisOdd_of_swapOdd L63
• theorem state_eq_netDebit_plus_balanced L70
• theorem balanced_snd_pair L77
• theorem posting_form_of_incidence_swap L85
• theorem readsNet_iff_additiveOnDebit_of_posting L96
• theorem energyEqualsCost_of_posting_incidence_additive_unit L127
• theorem energyEqualsCost_of_posting_incidence_readsNet_unit L142
• theorem imbalance_posting_incidence L158
• theorem imbalance_swap_odd L163
• theorem imbalance_inhabits_posting_package L168
• def cubeDiff L182
• theorem cubeDiff_posting_incidence L184
• theorem cubeDiff_swap_odd L189
• theorem cubeDiff_continuous L194
• theorem cubeDiff_balance_vanishing L197
• theorem cubeDiff_unit L203
• theorem cubeDiff_not_additiveOnDebitAxis L206
• theorem cubeDiff_not_readsNetImbalance L216
• theorem posting_incidence_does_not_force_debit_axis_additivity L234
• theorem abs_imbalance_not_posting_incidence L247
• theorem nlPUnit_not_posting_incidence L255
• theorem prior_nogo_witnesses_fail_posting_incidence L267
• structure NetImbalanceDerivationVerdict L279
• theorem netImbalanceDerivationVerdict L310