Five.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

lemma OAI.EuclideanFiveColor.graphRealization_positive_three line 10

theorem OAI.EuclideanFiveColor.graph_map_small_mesh_impossible line 22

Source documentation

The actual positive-coordinate component cover contradicts the planar cover obstruction whenever every connected positive region has diameter at most two.

theorem graph_map_small_mesh_impossible
    (F : C(Metric.closedBall (0:ℂ) 5,GraphSpace (⊤ : SimpleGraph (Fin 5))))
    (hmesh : ∀(i : Fin 5) (K : Set ℂ),IsPreconnected K → K⊆Metric.closedBall (0:ℂ) 5 →
      (∀z : Metric.closedBall (0:ℂ) 5,z.val∈K → 0<(F z).val i) →
      ∀x∈K,∀y∈K,dist x y≤2) : False := by
…

Mentions: OAI.EuclideanFiveColor.GraphSpace

lemma OAI.EuclideanFiveColor.graph_map_large_positive line 94

Source documentation

Every continuous graph-valued map of the disk has a positive-coordinate connected region of diameter greater than two.

lemma graph_map_large_positive
    (F : C(Metric.closedBall (0:ℂ) 5,GraphSpace (⊤ : SimpleGraph (Fin 5)))) :
    ∃i : Fin 5,∃K : Set ℂ,IsPreconnected K ∧ K⊆Metric.closedBall (0:ℂ) 5 ∧
      (∀z : Metric.closedBall (0:ℂ) 5,z.val∈K → 0<(F z).val i) ∧
      ∃x∈K,∃y∈K,2<dist x y := by
…

Mentions: OAI.EuclideanFiveColor.GraphSpace

theorem OAI.EuclideanFiveColor.no_measurable_weak_five_coloring line 105
Source documentation
No Borel weak five-coloring exists. The global approximants here are constructed from the actual coloring, its transition graph, and its common interface limits, rather than supplied as an extra coloring hypothesis.
```
theorem no_measurable_weak_five_coloring {c : ℂ → Fin 5}
    (hc : Measurable c) (hw : WeakColoring 5 c) : False := by
…
```
Mentions: OAI.EuclideanFiveColor.WeakColoring
theorem OAI.EuclideanFiveColor.no_proper_five_coloring line 124
Source documentation
No unrestricted five-coloring separates all unit-distance pairs in the Euclidean plane.
Distinct definitions of this name: ComparatorChallenges/EuclideanFiveColor.lean:10 (different declaration text). Qualify references as OAI.EuclideanFiveColor.no_proper_five_coloring@path.
```
theorem no_proper_five_coloring : ¬ ∃ c : ℂ → Fin 5, ProperColoring 5 c := by
…
```