OAI/Geometry/PlaneColoring/Exclusion.lean

GitHub source file

28 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.EuclideanFiveColor.fiveDiag line 8
  2. def OAI.EuclideanFiveColor.fiveAdj line 9
  3. instance OAI.EuclideanFiveColor.(instance at line 10) line 10
  4. def OAI.EuclideanFiveColor.fiveEdge line 11
  5. def OAI.EuclideanFiveColor.FiveAdmissible line 12
  6. def OAI.EuclideanFiveColor.fiveCanonical line 14
  7. lemma OAI.EuclideanFiveColor.five_admissible_diag line 17
  8. lemma OAI.EuclideanFiveColor.five_diag_disjoint line 20
  9. lemma OAI.EuclideanFiveColor.five_diag_nonempty line 21
  10. lemma OAI.EuclideanFiveColor.five_diag_unique line 22
  11. lemma OAI.EuclideanFiveColor.five_adj_four line 23
  12. lemma OAI.EuclideanFiveColor.five_no_common_adj line 24
  13. lemma OAI.EuclideanFiveColor.five_forced_label line 26
  14. def OAI.EuclideanFiveColor.sideAllowed line 36

    Source documentation

    Labels allowed on the side selected by b; a label survives precisely when both of its incident edges have the opposite sign.

    def sideAllowed (s : Fin 5 → Bool) (b : Bool) : Finset (Fin 5) :=
…
  15. def OAI.EuclideanFiveColor.SideCompatible line 39

    Source documentation

    Both actual one-sided strip restrictions on a palette.

    def SideCompatible (s : Fin 5 → Bool) (p : Finset (Fin 5)) : Prop :=
…
  16. instance OAI.EuclideanFiveColor.(instance at line 41) line 41
  17. lemma OAI.EuclideanFiveColor.side_compatible_diagonal line 43
  18. lemma OAI.EuclideanFiveColor.side_compatible_options line 45
  19. lemma OAI.EuclideanFiveColor.side_allowed_not line 48
  20. lemma OAI.EuclideanFiveColor.side_compatible_not line 53
  21. lemma OAI.EuclideanFiveColor.five_triple_forced line 57
  22. lemma OAI.EuclideanFiveColor.five_six_constant_steps_impossible line 60
  23. lemma OAI.EuclideanFiveColor.five_word_impossible line 64
  24. lemma OAI.EuclideanFiveColor.five_strip_orbit_impossible line 71
  25. def OAI.EuclideanFiveColor.angularSign line 94
  26. lemma OAI.EuclideanFiveColor.angularSign_opposite line 95
  27. lemma OAI.EuclideanFiveColor.five_sides_compatible line 104
  28. lemma OAI.EuclideanFiveColor.no_five_exclusion_continua line 144

    Source documentation

    Actual five-cycle angular obstruction under exactly the directional and common-support-exclusion data extracted in source Proposition interface-cycle. This does not assert that such data have been extracted.

    lemma no_five_exclusion_continua (hw : WeakColoring 5 c) {x : ℂ}
    {K : Fin 5 → Set ℂ} {v : Fin 5 → ℂ} (hv : ∀i,‖v i‖=1)
    (hK : ∀i,ApproachingContinuum x (K i) (v i))
    (hH : ∀i,Disjoint (spatialSupport c i) (Straddle (K i)) ∧
      Disjoint (spatialSupport c (i+1)) (Straddle (K i))) : False := by
…

    Mentions: OAI.EuclideanFiveColor.WeakColoring, OAI.EuclideanFiveColor.ApproachingContinuum, OAI.EuclideanFiveColor.spatialSupport, OAI.EuclideanFiveColor.Straddle