OAI/Geometry/PlaneColoring/Interfaces.lean

GitHub source file

47 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.EuclideanFiveColor.interfaceFourEdge line 10

   Source documentation

   The four cyclic edges, with outsider label 4. This definition is local to this interface argument and agrees extensionally with fourEdge.

   def interfaceFourEdge (i : Fin 4) : Finset (Fin 5) :=
   …

2. def OAI.EuclideanFiveColor.interfaceFourAllowed line 12
3. def OAI.EuclideanFiveColor.InterfaceFourCompatible line 14
4. def OAI.EuclideanFiveColor.InterfaceFourSplit line 17
5. def OAI.EuclideanFiveColor.interfaceFourDiagonal line 18
6. lemma OAI.EuclideanFiveColor.interface_four_not_edge line 19
7. lemma OAI.EuclideanFiveColor.interface_four_split line 23
8. lemma OAI.EuclideanFiveColor.interface_four_split_neg line 28
9. lemma OAI.EuclideanFiveColor.interface_four_diagonal_neg line 31
10. lemma OAI.EuclideanFiveColor.interface_four_diagonal_ne_zero line 34
11. lemma OAI.EuclideanFiveColor.interface_four_split_no_opposite line 37
12. def OAI.EuclideanFiveColor.fourInterfaceSign line 48
13. lemma OAI.EuclideanFiveColor.interfaceFourEdge_eq line 50
14. lemma OAI.EuclideanFiveColor.fourInterfaceSign_opposite line 51
15. lemma OAI.EuclideanFiveColor.four_interface_compatible line 61
16. lemma OAI.EuclideanFiveColor.four_interface_admissible line 86
17. lemma OAI.EuclideanFiveColor.four_state_group_of_admissible line 91
18. lemma OAI.EuclideanFiveColor.four_state_represents_of_group line 95
19. lemma OAI.EuclideanFiveColor.four_state_changes_of_group line 104
20. lemma OAI.EuclideanFiveColor.four_state_diagonal_positive_of_group line 111
21. lemma OAI.EuclideanFiveColor.four_interface_state_rule line 143
22. lemma OAI.EuclideanFiveColor.angle_state_preimage_positive line 158
23. lemma OAI.EuclideanFiveColor.angle_support_lift line 166

    Source documentation

    Every point of an angular essential support has a real essential-support lift. The compact fundamental domain is used only to establish the support inclusion.

    lemma angle_support_lift {A : Set Angles} (hA : MeasurableSet A) {t : Angles}
        (ht : t∈(angularMeasure.restrict A).support) :
        ∃b : ℝ,(b : Angles)=t ∧ b∈(volume.restrict (((↑) : ℝ → Angles) ⁻¹' A)).support := by
    …

    Mentions: OAI.EuclideanFiveColor.Angles

24. lemma OAI.EuclideanFiveColor.direction_inner_real line 198
25. lemma OAI.EuclideanFiveColor.three_direction_moment line 204
26. lemma OAI.EuclideanFiveColor.direction_sixty_unit line 231
27. lemma OAI.EuclideanFiveColor.compact_no_unit_margin line 241
28. def OAI.EuclideanFiveColor.interfaceStateSet line 256
29. def OAI.EuclideanFiveColor.interfaceStateSupport line 257
30. lemma OAI.EuclideanFiveColor.interfaceStateSet_measurable line 259
31. lemma OAI.EuclideanFiveColor.interfaceStateSupport_ae line 261
32. lemma OAI.EuclideanFiveColor.interfaceStateSupport_no_unit line 266
33. lemma OAI.EuclideanFiveColor.interfaceStateSupport_margin line 281
34. lemma OAI.EuclideanFiveColor.four_diagonal_product_neg line 303
35. lemma OAI.EuclideanFiveColor.four_diagonal_product_pos line 313
36. lemma OAI.EuclideanFiveColor.four_diagonal_orbit_half line 324
37. lemma OAI.EuclideanFiveColor.four_diagonal_uniform_of_parity line 329
38. lemma OAI.EuclideanFiveColor.four_uniform_diagonal_one line 341
39. lemma OAI.EuclideanFiveColor.four_uniform_diagonal_two line 351
40. lemma OAI.EuclideanFiveColor.four_opposite_uniform_diagonals_false line 364

    Source documentation

    The three-direction quadratic moment replaces the source's projective arc length argument. No assumption about antipodal ray pairs or the collinear case is required: two opposite uniform diagonal triples are already contradictory.

    lemma four_opposite_uniform_diagonals_false {v : Fin 4 → ℂ} {t u : Angles}
        (hnt : ∀j i,⟪direction (t+sixAngle j),v i⟫≠0)
        (hnu : ∀j i,⟪direction (u+sixAngle j),v i⟫≠0)
        {a b : Fin 3} (ha : a≠0) (hb : b≠0) (hab : a≠b)
        (hdt : ∀j : Fin 6,interfaceFourDiagonal (fourInterfaceSign v (t+sixAngle j))=a)
        (hdu : ∀j : Fin 6,interfaceFourDiagonal (fourInterfaceSign v (u+sixAngle j))=b) : False := by
    …

    Mentions: OAI.EuclideanFiveColor.Angles, OAI.EuclideanFiveColor.direction, OAI.EuclideanFiveColor.sixAngle, OAI.EuclideanFiveColor.interfaceFourDiagonal, OAI.EuclideanFiveColor.fourInterfaceSign

41. lemma OAI.EuclideanFiveColor.sixAngle_prev line 382
42. def OAI.EuclideanFiveColor.fourInterfaceWord line 386
43. lemma OAI.EuclideanFiveColor.fourInterfaceWord_shift line 388
44. lemma OAI.EuclideanFiveColor.four_interface_word_data line 395

    Source documentation

    Construction of the dense conull shift-invariant set and its actual six-position words, from the previously established genuine state system.

    lemma four_interface_word_data (hw : WeakColoring 5 c) {x : ℂ} {v : Fin 4 → ℂ}
        (hv : ∀i,‖v i‖=1)
        (hcompat : ∀ᵐt∂angularMeasure,InterfaceFourCompatible (fourInterfaceSign v t) (palette c hc x t)) :
        ∃G : Set Angles,Dense G ∧ (∀t∈G,t+(sixty : Angles)∈G) ∧
          (∀t∈G,∀j i,⟪direction (t+sixAngle j),v i⟫≠0) ∧
          (∀t∈G,∀j,fourInterfaceWord hc x t j≠0 → fourInterfaceWord hc x t j=
            interfaceFourDiagonal (fourInterfaceSign v (t+sixAngle j))) ∧
          (∀t∈G,FourWordValid (fourInterfaceWord hc x t)) ∧
          ∃ε : ℝ,0<ε ∧ ∀t∈G,∀u∈G,dist t u<ε →
            FourWordCross (fourInterfaceWord hc x t) (fourInterfaceWord hc x u) := by
    …

    Mentions: OAI.EuclideanFiveColor.WeakColoring, OAI.EuclideanFiveColor.angularMeasure, OAI.EuclideanFiveColor.InterfaceFourCompatible, OAI.EuclideanFiveColor.fourInterfaceSign, OAI.EuclideanFiveColor.palette, OAI.EuclideanFiveColor.Angles, OAI.EuclideanFiveColor.sixty, OAI.EuclideanFiveColor.direction, OAI.EuclideanFiveColor.sixAngle, OAI.EuclideanFiveColor.fourInterfaceWord, OAI.EuclideanFiveColor.interfaceFourDiagonal, OAI.EuclideanFiveColor.FourWordValid, OAI.EuclideanFiveColor.FourWordCross

45. lemma OAI.EuclideanFiveColor.four_word_opposite_geometry_false line 454
46. lemma OAI.EuclideanFiveColor.no_four_word_geometry line 473
47. lemma OAI.EuclideanFiveColor.no_four_interfaces line 516

    Source documentation

    The actual length-four interface cycle is impossible. All hypotheses are exactly approach directions and common straddling exclusion of both endpoints.

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

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