IndisputableMonolith.Gravity.SevenGaps.Gap2JEhrhartSpan

declarations in this module (60)

• structure the L11
• theorem below L63
• def outdeg L108
• def indeg L113
• def vertexImbalance L119
• def imbalanceSq L123
• theorem indeg_eq_sum L126
• theorem outdeg_eq_sum L131
• def jCost L145
• theorem jCost_inl L150
• theorem jCost_edge L153
• theorem jCost_tet L156
• theorem historyCost_jCost L162
• theorem jCost_vanishes_on_balanced_vertex L174
• theorem indeg_relabel L185
• theorem outdeg_relabel L198
• theorem vertexImbalance_relabel L211
• theorem jCost_equivariant L217
• def pointComplex L235
• def edgeComplex L246
• def pathComplex L257
• def twoEdgeComplex L268
• theorem imbalance_point L278
• theorem imbalance_edge_zero L281
• theorem imbalance_edge_one L283
• theorem imbalance_path_zero L285
• theorem imbalance_path_one L287
• theorem imbalance_path_two L289
• theorem path_middle_balanced_ends_not L295
• theorem blockSum_point L303
• theorem blockSum_edge L307
• theorem blockSum_path L315
• theorem jCost_not_fixedKindTotals L328
• theorem jCost_not_a_valuation L352
• def mV4 L377
• def mE4 L381
• def mT4 L384
• def mC4 L387
• def mJ4 L390
• def cert4 L394
• def dot4 L396
• theorem cert4_annihilates_census L398
• theorem cert4_sees_J4 L404
• theorem J4_not_in_census_span L411
• theorem J4_not_in_census_span_with_const L422
• def mV3 L434
• def mE3 L435
• def mT3 L436
• def mC3 L437
• def mJ3 L440
• def cert3 L442
• def dot3 L444
• theorem cert3_annihilates_counts L446
• theorem cert3_sees_J3 L451
• theorem J3_not_in_census_span L457
• theorem census3_det L468
• theorem census3_with_const_is_onto L482
• theorem j0_ne_cV_3D L493
• structure JEhrhartSpanVerdict L506
• theorem jEhrhartSpanVerdict L534