Odd distance graph

2 fully proved1 ready to prove

The odd distance graph

DefinitionOdd distance graph#✓fully proved

The odd distance graph is the simple graph on the Euclidean plane \(\mathbb{R}^2\) in which two points \(x\) and \(y\) are adjacent when their Euclidean distance is an odd integer.

noncomputable def OddDistanceGraph : SimpleGraph (EuclideanSpace ℝ (Fin 2)) where
  Adj x y := ∃ k : ℕ, Odd k ∧ dist x y = (k : ℝ)
  symm := ⟨by
    intro x y h
    obtain ⟨k, hk, hkk⟩ := h
    exact ⟨k, hk, by rw [dist_comm]; exact hkk⟩⟩
  loopless := ⟨by
    intro x h
    obtain ⟨k, hk, hkk⟩ := h
    rw [dist_self] at hkk
    have hk0 : k = 0 := by exact_mod_cast hkk.symm
    rw [hk0] at hk
    exact Nat.not_odd_zero hk⟩

Used by 1

Used byInfinite chromatic number of the odd distance graph

DefinitionInfinite chromatic number of the odd distance graph#✓fully proved

The proposition that the odd distance graph on \(\mathbb{R}^2\) has infinite chromatic number, that is, has no proper colouring with finitely many colours.

def OddDistanceChromaticInfinite : Prop := OddDistanceGraph.chromaticNumber = ⊤

noncomputable def OddDistanceGraph : SimpleGraph (EuclideanSpace ℝ (Fin 2)) where
  Adj x y := ∃ k : ℕ, Odd k ∧ dist x y = (k : ℝ)
  symm := ⟨by
    intro x y h
    obtain ⟨k, hk, hkk⟩ := h
    exact ⟨k, hk, by rw [dist_comm]; exact hkk⟩⟩
  loopless := ⟨by
    intro x h
    obtain ⟨k, hk, hkk⟩ := h
    rw [dist_self] at hkk
    have hk0 : k = 0 := by exact_mod_cast hkk.symm
    rw [hk0] at hk
  ⋯

WantedExt/GraphTheory/OddDistanceGraphInfiniteChromaticWanted.lean:36

Uses 1 · Used by 1

Statement usesOdd distance graph

Used byDavies' odd distance theorem

Davies' odd distance theorem

TheoremDavies' odd distance theorem#●ready to prove

The odd distance graph on the Euclidean plane \(\mathbb{R}^2\), in which two points are adjacent when their distance is an odd integer, has infinite chromatic number: it has no proper colouring with finitely many colours.

Davies proves (Theorem 1) that every finite colouring of the plane has a monochromatic pair of points at odd integer distance.

public theorem_wanted OddDistanceChromaticInfinite_holds : ODGIC.OddDistanceChromaticInfinite

Sources

James Davies, Odd distances in colourings of the plane, Geometric and Functional Analysis 34 (2024) 19-31, arXiv:2209.15598, https://arxiv.org/abs/2209.15598.

Uses 1

Statement usesInfinite chromatic number of the odd distance graph

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.