OAI/Geometry/PlaneColoring/Sectors.lean

GitHub source file

29 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.EuclideanFiveColor.triangleEdge line 10
2. lemma OAI.EuclideanFiveColor.triangle_majority_cover line 11
3. lemma OAI.EuclideanFiveColor.triangle_outsider line 13
4. lemma OAI.EuclideanFiveColor.ApproachingContinuum.side_strip line 16
5. lemma OAI.EuclideanFiveColor.triangle_outsider_strip line 32

   Source documentation

   Three interface edges supply an actual outsider-only open strip in every nonexceptional direction, with the radial side chosen by the majority sign.

   lemma triangle_outsider_strip {c : ℂ → Fin 5} (hc : Measurable c)
       {x : ℂ} {K : Fin 3 → Set ℂ} {v : Fin 3 → ℂ}
       (hK : ∀i,ApproachingContinuum x (K i) (v i))
       (hH : ∀i,∀j∈triangleEdge i,Disjoint (spatialSupport c j) (Straddle (K i)))
       {e : ℂ} (he : ‖e‖=1) (hn : ∀i,⟪e,v i⟫≠0) :
       ∃b : Bool,∃δ>0,∃W : Set ℂ,IsOpen W ∧
         (∀ᵐz : ℂ∂volume,z∈W → c z=3 ∨ c z=4) ∧
         ∀e' : ℂ,‖e'‖=1 → dist e' e<δ → ∀r : ℝ,
           0<r → |r-1|<δ → (if b then 1<r else r<1) → x+(r:ℂ)*e'∈W := by
   …

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

6. lemma OAI.EuclideanFiveColor.triangle_palette_local line 61

   Source documentation

   Actual local triangle palette rigidity, without terminal angular sectors or boundary information as hypotheses.

   lemma triangle_palette_local {c : ℂ → Fin 5} (hc : Measurable c) (hw : WeakColoring 5 c)
       {x : ℂ} {K : Fin 3 → Set ℂ} {v : Fin 3 → ℂ}
       (hK : ∀i,ApproachingContinuum x (K i) (v i))
       (hH : ∀i,∀j∈triangleEdge i,Disjoint (spatialSupport c j) (Straddle (K i)))
       {t : Angles} (hn : ∀i,⟪direction t,v i⟫≠0)
       (hnR : ∀i,⟪direction t*(Circle.exp (Real.pi/3) : ℂ),v i⟫≠0) :
       ∃i : Fin 5,(i=3 ∨ i=4) ∧ ∃A : Set Angles,IsOpen A ∧ t∈A ∧
         ∀ᵐu∂angularMeasure,u∈A → i∈palette c hc x u := by
   …

   Mentions: OAI.EuclideanFiveColor.WeakColoring, OAI.EuclideanFiveColor.ApproachingContinuum, OAI.EuclideanFiveColor.triangleEdge, OAI.EuclideanFiveColor.spatialSupport, OAI.EuclideanFiveColor.Straddle, OAI.EuclideanFiveColor.Angles, OAI.EuclideanFiveColor.direction, OAI.EuclideanFiveColor.angularMeasure, OAI.EuclideanFiveColor.palette

7. lemma OAI.EuclideanFiveColor.triangle_binary_from_continua line 85
8. def OAI.EuclideanFiveColor.triangleState line 119
9. lemma OAI.EuclideanFiveColor.triangleState_measurable line 122
10. lemma OAI.EuclideanFiveColor.triangleState_flip line 124
11. lemma OAI.EuclideanFiveColor.triangleState_local line 133
12. lemma OAI.EuclideanFiveColor.direction_injective line 150
13. lemma OAI.EuclideanFiveColor.direction_plus_sixty line 152
14. lemma OAI.EuclideanFiveColor.triple_orthogonal_cover line 157
15. lemma OAI.EuclideanFiveColor.triangle_boundary_one_orbit line 193

    Source documentation

    The actual three-interface data force the source's unique six-position boundary orbit. This theorem does not assume local rigidity or orbit finiteness.

    lemma triangle_boundary_one_orbit {c : ℂ → Fin 5} (hc : Measurable c) (hw : WeakColoring 5 c)
        {x : ℂ} {K : Fin 3 → Set ℂ} {v : Fin 3 → ℂ} (hv : ∀i,‖v i‖=1)
        (hK : ∀i,ApproachingContinuum x (K i) (v i))
        (hH : ∀i,∀j∈triangleEdge i,Disjoint (spatialSupport c j) (Straddle (K i))) :
        ∃t,angleBoundary (triangleState c hc x)={u | ∃j : Fin 6,u=t+sixAngle j} := by
    …

    Mentions: OAI.EuclideanFiveColor.WeakColoring, OAI.EuclideanFiveColor.ApproachingContinuum, OAI.EuclideanFiveColor.triangleEdge, OAI.EuclideanFiveColor.spatialSupport, OAI.EuclideanFiveColor.Straddle, OAI.EuclideanFiveColor.angleBoundary, OAI.EuclideanFiveColor.triangleState, OAI.EuclideanFiveColor.sixAngle

16. lemma OAI.EuclideanFiveColor.angleEssential_connected line 209
17. lemma OAI.EuclideanFiveColor.one_orbit_first_arc line 226
18. lemma OAI.EuclideanFiveColor.angleEssential_real_periodic line 257
19. lemma OAI.EuclideanFiveColor.one_orbit_sectors line 274
20. lemma OAI.EuclideanFiveColor.moser_density_impossible line 326
21. lemma OAI.EuclideanFiveColor.lineDensityZero_compl_of_mem_nhds line 347
22. def OAI.EuclideanFiveColor.positiveSector line 358
23. def OAI.EuclideanFiveColor.negativeSector line 359
24. lemma OAI.EuclideanFiveColor.positiveSector_open line 360
25. lemma OAI.EuclideanFiveColor.negativeSector_open line 362
26. lemma OAI.EuclideanFiveColor.polynomial_region_density line 365
27. lemma OAI.EuclideanFiveColor.no_alternating_sectors line 392

    Source documentation

    The exact six-sector outcome of triangle rigidity is impossible, for every center and phase.

    lemma no_alternating_sectors {c : ℂ → Fin 5} (hc : Measurable c) (hw : WeakColoring 5 c)
        {x : ℂ} {a b : Fin 5} (hab : a≠b) (φ : ℝ)
        (hpos : RealState hc x (positiveSector φ) {a})
        (hneg : RealState hc x (negativeSector φ) {b}) : False := by
    …

    Mentions: OAI.EuclideanFiveColor.WeakColoring, OAI.EuclideanFiveColor.RealState, OAI.EuclideanFiveColor.positiveSector, OAI.EuclideanFiveColor.negativeSector

28. lemma OAI.EuclideanFiveColor.triangleState_palette line 411
29. lemma OAI.EuclideanFiveColor.no_triangle_interfaces line 428

    Source documentation

    Complete actual triangle-interface endgame, including boundary rigidity, sector extraction and the exact seven-point unit-distance certificate.

    lemma no_triangle_interfaces {c : ℂ → Fin 5} (hc : Measurable c) (hw : WeakColoring 5 c)
        {x : ℂ} {K : Fin 3 → Set ℂ} {v : Fin 3 → ℂ} (hv : ∀i,‖v i‖=1)
        (hK : ∀i,ApproachingContinuum x (K i) (v i))
        (hH : ∀i,∀j∈triangleEdge i,Disjoint (spatialSupport c j) (Straddle (K i))) : False := by
    …

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