Documentation

Counterexamples.HeawoodUnitDistance

A simple planar unit-distance embedding of the Heawood graph #

The Heawood graph on 14 vertices is the point-line incidence graph of the Fano plane. Besides being 3-regular and symmetric it has a number of interesting properties: it is the unique (3,6)-cage, it can be embedded on the torus with dual K₇ and so on.

In 1972 Chvátal wrote of a "suspicion" that the Heawood graph was not unit-distance embeddable into the Euclidean plane (Problem 21 in [CKK72]). In 2009 Gerbracht disproved the suspicion by presenting an explicit embedding [Ger09], but the embeddings presented there are very hard to describe: the minimal polynomials of their vertex coordinates go up to degree 79. Other embeddings found since then, such as the one in [HI14], suffer from the same complexity issue.

This file formalises a much simpler embedding, independently found by Moritz Firsching in July 2016 and Jeremy Tan in August 2025. Its coordinates are polynomials in the unique real root of 2c^3 + 3c + 1.

source
def SimpleGraph.heawoodGraph :
SimpleGraph (Fin 14)

The Heawood graph, a notable simple graph on 14 vertices. The numbering corresponds to a typical Hamiltonian cycle-and-arcs drawing.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    instance SimpleGraph.instDecidableRelFinOfNatNatAdjHeawoodGraph :
    DecidableRel heawoodGraph.Adj
    Equations
    source
    theorem SimpleGraph.heawoodGraph_edgeFinset :
    heawoodGraph.edgeFinset = Finset.image (fun (i : Fin 14) => s(i, i + 1)) Finset.univ ∪ Finset.image (fun (i : Fin 14) => s(i, i + 5)) {x : Fin 14 | Even ↑x}
    source
    theorem SimpleGraph.card_heawoodGraph_edgeFinset :
    heawoodGraph.edgeFinset.card = 21
    source
    theorem SimpleGraph.heawoodGraph_neighborFinset (i : Fin 14) :
    heawoodGraph.neighborFinset i = {i + 1, i - 1, if Even ↑i then i + 5 else i - 5}
    source
    theorem SimpleGraph.isRegularOfDegree_heawoodGraph :
    heawoodGraph.IsRegularOfDegree 3

    The Heawood graph is 3-regular.

    A key number #

    source
    theorem SimpleGraph.Heawood.exists_root_in_Ioo :
    ∃ c ∈ Set.Ioo (-1 / 3) (-5 / 16), 2 * c ^ 3 + 3 * c + 1 = 0

    2c^3+3c+1 has a root in (-1/3, -5/16). This root, which turns out to be unique (we do not need uniqueness), underpins our unit-distance embedding's coordinates.

    source
    noncomputable def SimpleGraph.Heawood.root :
    ℝ

    The real root c = -0.312908... of 2c^3+3c+1.

    Equations
    Instances For
      source
      def SimpleGraph.Heawood.termC :
      Lean.ParserDescr

      The real root c = -0.312908... of 2c^3+3c+1.

      Equations
      Instances For
        source
        theorem SimpleGraph.Heawood.root_bounds :
        root ∈ Set.Ioo (-1 / 3) (-5 / 16)
        source
        theorem SimpleGraph.Heawood.root_equation :
        2 * root ^ 3 + 3 * root + 1 = 0

        The embedding proper #

        source
        def SimpleGraph.Heawood.termPlane :
        Lean.ParserDescr

        Notation for the Euclidean plane.

        Equations
        Instances For
          source
          theorem SimpleGraph.Heawood.dist_eq_one_iff {x₀ y₀ x₁ y₁ : ℝ} :
          dist !₂[x₀, y₀] !₂[x₁, y₁] = 1 ↔ (x₀ - x₁) ^ 2 + (y₀ - y₁) ^ 2 = 1
          source
          noncomputable def SimpleGraph.Heawood.udMap :
          Fin 14 → Plane

          The base function from graph vertices to Euclidean points in our embedding.

          Equations
          Instances For
            source
            theorem SimpleGraph.Heawood.reflect_toEuclideanLin {x y : ℝ} :
            (Matrix.toEuclideanLin !![1, 0; 0, -1]) !₂[x, y] = !₂[x, -y]
            source
            theorem SimpleGraph.Heawood.udMap_reflect (i : Fin 14) :
            udMap i.rev = (Matrix.toEuclideanLin !![1, 0; 0, -1]) (udMap i)
            source
            theorem SimpleGraph.Heawood.decompose_point (p : Plane) :
            p = !₂[(EuclideanSpace.proj 0) p, (EuclideanSpace.proj 1) p]
            source
            theorem SimpleGraph.Heawood.injOn_udMap_sextet :
            Set.InjOn udMap ↑{0, 7, 10, 5, 2, 9}

            udMap is injective on indices [0, 7, 10, 5, 2, 9] because their x-coordinates strictly increase in that order.

            source
            theorem SimpleGraph.Heawood.injective_udMap :
            Function.Injective udMap

            udMap is injective and thus can be used in a unit-distance embedding.

            source
            theorem SimpleGraph.Heawood.dist_udMap_rev {i j : Fin 14} (h : dist (udMap i) (udMap j) = 1) :
            dist (udMap i.rev) (udMap j.rev) = 1
            source
            theorem SimpleGraph.Heawood.dist_udMap_rev_iff {i j : Fin 14} :
            dist (udMap i) (udMap j) = 1 ↔ dist (udMap i.rev) (udMap j.rev) = 1
            source
            theorem SimpleGraph.Heawood.dist_udMap_eq_one_of_eq {i j i' j' : Fin 14} (he : s(i', j') = s(i, j)) (hd : dist (udMap i') (udMap j') = 1) :
            dist (udMap i) (udMap j) = 1
            source
            noncomputable def SimpleGraph.Heawood.unitDistEmbedding :
            heawoodGraph.UnitDistEmbedding Plane

            A unit-distance embedding of the Heawood graph in the Euclidean plane.

            Equations
            • One or more equations did not get rendered due to their size.
            Instances For