IndisputableMonolith.Gravity.SevenGaps.Gap2JDiamondRank · Recognition explainer

used by (2)

From the project-wide theorem graph. These declarations reference this one in their body.

IndisputableMonolith.Gravity.SevenGaps.Gap2JDiamondRankHostileProbe module_import
IndisputableMonolith.Gravity.SevenGaps.Gap2LedgerGenerated module_import

depends on (1)

Lean names referenced from this declaration's body.

IndisputableMonolith.Gravity.SevenGaps.Gap2JEhrhartSpan module_import

declarations in this module (117)

structure Subcomplex L105
def subIndeg L112
def subOutdeg L116
def subImbalance L122
def subCharge L127
def diamondDefect L133
theorem subImbalance_eq_zero_of_not_mem L138
theorem subImbalance_union L154
theorem diamondDefect_eq_neg_two_inner L173
theorem diamondDefect_eq_zero_of_inter_empty L239
theorem diamondDefect_eq_zero_of_interface_balanced L250
theorem sum_vertexImbalance L271
theorem imbalanceSq_even L304
def forkComplex L331
def threePathComplex L342
def outStarComplex L353
def loopPointComplex L366
theorem imbalance_fork_zero L376
theorem imbalance_fork_one L378
theorem imbalance_fork_two L380
theorem imbalance_threePath_zero L382
theorem imbalance_threePath_one L384
theorem imbalance_threePath_two L386
theorem imbalance_threePath_three L388
theorem imbalance_outStar_zero L390
theorem imbalance_outStar_one L392
theorem imbalance_outStar_two L394
theorem imbalance_outStar_three L396
theorem imbalance_twoEdge_zero L398
theorem imbalance_twoEdge_one L400
theorem imbalance_twoEdge_two L402
theorem imbalance_twoEdge_three L404
theorem imbalance_loopPoint_zero L406
theorem imbalance_loopPoint_one L408
theorem imbalanceSq_fork L410
theorem imbalanceSq_threePath L412
theorem imbalanceSq_outStar L414
theorem imbalanceSq_twoEdge L416
theorem imbalanceSq_loopPoint L418
theorem historyCost_jCost_eq L423
theorem historyCost_edge L431
theorem historyCost_path L435
theorem historyCost_point L439
theorem imbalanceSq_emptyComplex L443
theorem historyCost_empty L445
theorem blockSum_twoEdge L450
theorem historyCost_twoEdge L459
theorem blockSum_fork L463
theorem historyCost_fork L471
theorem blockSum_threePath L475
theorem historyCost_threePath L484
theorem blockSum_outStar L488
theorem historyCost_outStar L497
theorem historyCost_loopPoint L501
theorem diamond_J_seed L514
theorem diamond_J_threePath L525
theorem diamond_J_outStar L537
theorem diamond_J_disjoint L548
theorem jCost_not_a_function_of_counts L560
def pathLeft L580
def pathRight L593
theorem seed_edges_cover L605
theorem seed_edges_disjoint L610
theorem seed_interface L617
theorem subImbalance_pathLeft_one L621
theorem subImbalance_pathRight_one L624
theorem seed_diamond_defect L629
theorem seed_diamond_localized L636
theorem seed_inner_product L644
def threePathLeft L652
def threePathRight L670
theorem threePath_edges_cover L682
theorem threePath_edges_disjoint L688
theorem threePath_interface L699
theorem subImbalance_threePathLeft_two L705
theorem subImbalance_threePathRight_two L708
theorem threePath_diamond_defect L713
def outStarFork L720
def outStarSpur L738
theorem outStar_edges_cover L750

… and 37 more