OAI/Geometry/PlaneColoring/AngularBoundary.lean

GitHub source file

55 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.EuclideanFiveColor.FourWordValid line 8

    Source documentation

    0 is the outsider and 1,2 the two diagonal states.

    def FourWordValid (w : Fin 6 → Fin 3) : Prop :=
…
  2. instance OAI.EuclideanFiveColor.(instance at line 10) line 10
  3. def OAI.EuclideanFiveColor.FourWordMixed line 11
  4. instance OAI.EuclideanFiveColor.(instance at line 13) line 13
  5. def OAI.EuclideanFiveColor.FourWordCross line 14
  6. instance OAI.EuclideanFiveColor.(instance at line 16) line 16
  7. lemma OAI.EuclideanFiveColor.forall_six_word line 17
  8. lemma OAI.EuclideanFiveColor.four_word_has_outsider line 28
  9. lemma OAI.EuclideanFiveColor.four_word_mixed_periodic line 31
  10. lemma OAI.EuclideanFiveColor.four_word_mixed_isolated line 35
  11. lemma OAI.EuclideanFiveColor.four_word_parity line 39
  12. lemma OAI.EuclideanFiveColor.four_word_shift_parity line 43
  13. lemma OAI.EuclideanFiveColor.four_word_opposite_parity line 47
  14. lemma OAI.EuclideanFiveColor.dense_isolated_value_constant line 62

    Source documentation

    Uniform local isolation of a value on a dense subset of a connected metric space propagates globally. This is the manuscript dense-set chain argument.

    lemma dense_isolated_value_constant {E F : Type*} [MetricSpace E] [PreconnectedSpace E]
    {G : Set E} (hG : Dense G) (f : E → F) {b : F} {ε : ℝ} (hε : 0<ε)
    (hne : ∃x∈G,f x=b)
    (hl : ∀x∈G,f x=b → ∀y∈G,dist x y<ε → f y=b) : ∀y∈G,f y=b := by
…
  15. lemma OAI.EuclideanFiveColor.sixty_six line 92
  16. lemma OAI.EuclideanFiveColor.sixty_three line 98
  17. def OAI.EuclideanFiveColor.sixAngle line 103
  18. lemma OAI.EuclideanFiveColor.sixAngle_step line 104
  19. lemma OAI.EuclideanFiveColor.sixAngle_half line 107
  20. lemma OAI.EuclideanFiveColor.direction_add_pi line 111
  21. lemma OAI.EuclideanFiveColor.four_words_no_mixed line 123

    Source documentation

    The mixed-parity exceptional words are excluded by actual local isolation and sixty-degree covariance on a dense set.

    lemma four_words_no_mixed (G : Set Angles) (hG : Dense G) (w : Angles → Fin 6 → Fin 3)
    (hv : ∀t∈G,FourWordValid (w t))
    (hshiftG : ∀t∈G,t+(sixty : Angles)∈G)
    (hshift : ∀t∈G,∀j,w (t+(sixty : Angles)) j=w t (j+1))
    {ε : ℝ} (hε : 0<ε)
    (hcross : ∀t∈G,∀u∈G,dist t u<ε → FourWordCross (w t) (w u)) :
    ∀t∈G,¬FourWordMixed (w t) := by
…

    Mentions: OAI.EuclideanFiveColor.Angles, OAI.EuclideanFiveColor.FourWordValid, OAI.EuclideanFiveColor.sixty, OAI.EuclideanFiveColor.FourWordCross, OAI.EuclideanFiveColor.FourWordMixed

  22. def OAI.EuclideanFiveColor.Straddle line 147

    Source documentation

    The source's strict min/max straddling region, in equivalent witness form.

    def Straddle (K : Set ℂ) : Set ℂ := {z | ∃p∈K,∃q∈K,dist z p<1 ∧ 1<dist z q}
  23. lemma OAI.EuclideanFiveColor.straddle_isOpen line 148
  24. lemma OAI.EuclideanFiveColor.straddle_connected_unit line 156
  25. lemma OAI.EuclideanFiveColor.approaching_direction_inside line 160
  26. lemma OAI.EuclideanFiveColor.approaching_direction_outside line 173
  27. lemma OAI.EuclideanFiveColor.outer_straddle_strip line 186
  28. lemma OAI.EuclideanFiveColor.inner_straddle_strip line 200
  29. lemma OAI.EuclideanFiveColor.finite_positive_lower_bound line 221
  30. structure OAI.EuclideanFiveColor.ApproachingContinuum line 235

    Source documentation

    The approach data furnished by the manuscript interface proposition, with no assumption of angular strip conclusions.

    structure ApproachingContinuum (x : ℂ) (K : Set ℂ) (v : ℂ) where
…
  31. lemma OAI.EuclideanFiveColor.ApproachingContinuum.outer_strip line 244
  32. lemma OAI.EuclideanFiveColor.ApproachingContinuum.inner_strip line 251
  33. lemma OAI.EuclideanFiveColor.continuum_outer_restriction line 259
  34. lemma OAI.EuclideanFiveColor.continuum_inner_restriction line 279
  35. def OAI.EuclideanFiveColor.spatialSupport line 308

    Source documentation

    The manuscript's essential spatial color support.

    def spatialSupport (i : Fin k) : Set ℂ := (volume.restrict {z | c z=i}).support
  36. lemma OAI.EuclideanFiveColor.mem_spatialSupport_ae line 309
  37. lemma OAI.EuclideanFiveColor.support_exclusion_ae line 313
  38. lemma OAI.EuclideanFiveColor.finite_support_exclusion_ae line 317
  39. def OAI.EuclideanFiveColor.angleEssential line 334
  40. lemma OAI.EuclideanFiveColor.angleEssential_open line 336
  41. lemma OAI.EuclideanFiveColor.angleEssential_ae line 340
  42. lemma OAI.EuclideanFiveColor.angleEssential_disjoint line 342
  43. def OAI.EuclideanFiveColor.angleBoundary line 349
  44. lemma OAI.EuclideanFiveColor.angleBoundary_closed line 350
  45. lemma OAI.EuclideanFiveColor.angleEssential_shift line 352
  46. lemma OAI.EuclideanFiveColor.angleBoundary_shift line 370
  47. lemma OAI.EuclideanFiveColor.angleBoundary_nonempty line 381
  48. lemma OAI.EuclideanFiveColor.sixAngle_add line 408
  49. lemma OAI.EuclideanFiveColor.sixty_order line 418
  50. lemma OAI.EuclideanFiveColor.sixAngle_injective line 423
  51. def OAI.EuclideanFiveColor.sixAngleHom line 430
  52. lemma OAI.EuclideanFiveColor.sixAngle_sub line 434
  53. lemma OAI.EuclideanFiveColor.angleBoundary_six line 435
  54. lemma OAI.EuclideanFiveColor.six_antipodal_vertex_cover line 444
  55. lemma OAI.EuclideanFiveColor.angleBoundary_one_orbit line 448

    Source documentation

    Core finite obstruction behind the one-orbit boundary theorem.

    lemma angleBoundary_one_orbit {s : Angles → Bool}
    (hf : ∀ᵐt∂angularMeasure,s (t+(sixty : Angles))= !(s t)) (B : Finset Angles)
    (hB : B.card≤6) (hanti : ∀t,t+(Real.pi : Angles)∈B ↔ t∈B)
    (hl : ∀t,t∉B → t+(sixty : Angles)∉B → ∃b,t∈angleEssential s b) :
    ∃t,angleBoundary s={u | ∃j : Fin 6,u=t+sixAngle j} := by
…

    Mentions: OAI.EuclideanFiveColor.Angles, OAI.EuclideanFiveColor.angularMeasure, OAI.EuclideanFiveColor.sixty, OAI.EuclideanFiveColor.angleEssential, OAI.EuclideanFiveColor.angleBoundary, OAI.EuclideanFiveColor.sixAngle