IndisputableMonolith.Gravity.SevenGaps.Gap2SizeBlindnessReach

declarations in this module (94)

• def loopCount L154
• theorem loopCount_eq_sum L157
• theorem loop_iff_of_relabel L165
• theorem loopCount_congr L174
• theorem loopCount_invariant L191
• theorem inlV_inj L201
• theorem inrV_inj L204
• theorem dunion_edgeVerts_inl L207
• theorem dunion_edgeVerts_inr L213
• theorem loopCount_dunion L220
• theorem loopCount_emptyComplex L245
• def properEdgeCount L265
• theorem properEdgeCount_eq_sum L268
• theorem properEdgeCount_congr L274
• theorem properEdgeCount_invariant L291
• theorem inlV_eq_iff L296
• theorem inrV_eq_iff L300
• theorem properEdgeCount_dunion L305
• theorem properEdgeCount_eq_zero_of_nV_le_one L327
• theorem properEdgeCount_emptyComplex L338
• structure AdditiveStat L349
• def loopStat L358
• def properStat L365
• def statWeight L380
• theorem gibbsWeight_positive L384
• theorem statWeight_invariant L394
• theorem statWeight_pos L399
• theorem statWeight_emptyComplex L403
• theorem classMass_statWeight L411
• theorem statWeight_glues L452
• theorem statWeight_glues_at_dust_edge L467
• theorem also L483
• theorem statWeight_not_gluesGenerally L486
• def twoLoops L505
• def twoBridges L516
• theorem loopCount_twoLoops L526
• theorem loopCount_twoBridges L528
• theorem properEdgeCount_twoLoops L530
• theorem properEdgeCount_twoBridges L532
• theorem twoLoops_sizes L534
• theorem twoBridges_sizes L537
• theorem witnesses_same_sizes_different_loops L542
• def SizeBlind L555
• theorem sizeWeight_sizeBlind L559
• theorem sq_ne_one_of_pos_ne_one L566
• theorem loopEscape_not_sizeBlind L574
• theorem properEscape_not_sizeBlind L590
• def NormalizedAtTheAtoms L610
• theorem gibbsWeight_eq_one_at_atoms L613
• theorem properEscape_normalizedAtTheAtoms L623
• theorem loopEscape_fails_the_atoms L635
• theorem statWeight_sizeBlind_at_one L652
• theorem loopEscape_sizeBlind_at_one L662
• theorem properEscape_sizeBlind_at_one L666
• def SatisfiesTheOtherHypotheses L684
• theorem properEscape_satisfiesTheOtherHypotheses L695
• theorem classMass_statWeight_at_one L706
• theorem properEscape_classMass_ne_mu L715
• theorem size_blindness_not_forced_by_the_other_hypotheses L756
• def RespectsKinds L780
• theorem postingAlphabet_equiv_iff_total L789
• theorem sizes_le_of_respectsKinds L806
• theorem exists_respectsKinds_iff_sizes L838
• def AlphabetBlindSorted L855
• theorem alphabetBlindSorted_iff_sizeBlind L860
• theorem loopEscape_not_alphabetBlindSorted L870
• def blob L884
• def canonicalSizeFun L897
• theorem sizeBlind_eq_sizeWeight L900
• theorem sizeBlind_iff_exists_sizeFun L919
• theorem premise_one_iff_alphabetBlind L936
• def Invariant L963
• def ResolvesNoMoreThanSizes L967
• def BlindTo L972
• theorem coarse_invariant_blindness_implies_sizeBlind L979
• theorem fine_invariant_blindness_does_not_imply_sizeBlind L994
• theorem invariant_coarse_or_fine L1031
• theorem blindness_forces_premise_one_iff_coarse L1074
• theorem indistinguishability_premises_never_weaken_premise_one L1088
• def sizeStatInvariant L1115

… and 14 more