IndisputableMonolith.Gravity.SevenGaps.Gap2OrientedFaceSpan · Recognition explainer

used by (2)

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

IndisputableMonolith.Gravity.SevenGaps.Gap2LetterCostDichotomy module_import
IndisputableMonolith.Gravity.SevenGaps.Gap2OrientedFaceSpanHostileProbe module_import

depends on (1)

Lean names referenced from this declaration's body.

IndisputableMonolith.Gravity.SevenGaps.Gap2JEhrhartSpan module_import

declarations in this module (80)

abbrev OFace L139
def rotFace L143
def revFace L147
theorem revFace_involutive L149
theorem revFace_eq_iff L151
theorem revFace_inj L156
def ind L160
theorem ind_congr L166
def orientSign L179
theorem orientSign_rev L186
def facetTriple L202
def facetSign L210
def faceImbalance L215
theorem faceImbalance_reverse L220
def facetImbalanceSq L236
def imbalanceSqTotal L240
def jFaceCost L254
theorem jFaceCost_inl L259
theorem jFaceCost_edge L262
theorem jFaceCost_tet L265
theorem historyCost_jFaceCost L271
theorem historyCost_jFaceCost_eq L281
theorem jFaceCost_vanishes_on_balanced_tet L295
def mapTriple L312
theorem mapTriple_rotFace L315
theorem mapTriple_revFace L318
theorem mapTriple_inj L321
theorem orientSign_map L326
theorem facetTriple_relabel L331
theorem faceImbalance_relabel L337
theorem facetImbalanceSq_relabel L346
theorem jFaceCost_equivariant L356
def oneTet L374
def twoTets L387
theorem facetImbalanceSq_oneTet L398
theorem imbalanceSqTotal_oneTet L400
theorem imbalanceSqTotal_twoTets L404
theorem twoTets_shared_facet_balanced_others_not L410
theorem faceImbalance_reverse_nonvacuous L418
theorem orientSign_degenerate_witness L425
theorem blockSum_oneTet L430
theorem blockSum_twoTets L436
theorem jFaceCost_not_fixedKindTotals L457
def mFor4 L495
def mForRaw4 L501
def mCurl4 L507
theorem cert4_sees_mFor4 L509
theorem cert4_sees_mForRaw4 L512
theorem cert4_sees_mCurl4 L515
theorem census4_with_const_span_iff L530
theorem no_pure_surface_term_in_census_span L559
theorem mFor4_not_in_census_span_with_const L571
theorem mFor4_not_in_census_span L579
theorem mForRaw4_not_in_census_span_with_const L586
theorem mCurl4_not_in_census_span_with_const L595
def oV4e L611
def oE4e L612
def oT4 L613
def oFor4e L616
def ocert4e L618
def oV4o L620
def oE4o L621
def oFor4o L624
def ocert4o L626
theorem ocert4e_annihilates_census L628
theorem ocert4e_sees_oFor4e L634
theorem ocert4o_annihilates_census L638
theorem ocert4o_sees_oFor4o L644
theorem oFor4e_not_in_census_span_with_const L649
theorem oFor4o_not_in_census_span_with_const L661
def mFor3 L679
theorem cert3_sees_mFor3 L681
theorem mFor3_not_in_census_span L684
structure OrientedFaceSpanVerdict L702
theorem orientedFaceSpanVerdict L745
structure OrientedFaceIndex L769
def orientedFaceIndex L793
theorem index_no_triple L803
theorem index_flag_unmoved L805
theorem index_not_the_a15_obstruction L807