Planar graphs and minors

Graphs drawn in the plane and on the square lattice, crossing numbers, Euler's formula, discrete Jordan curve and turning-number theorems, and the theory of graph minors.

• Discrete Gauss–Bonnet formula for polyominoes
• Euler's formula and cycle rank
• Graph minors
• Self-duality of the square lattice
• Straight-line planar drawings
• Two-regular minors
• Universal point sets for planar graphs
• Boundary contours in the square lattice
• Whitney's cut–cycle duality on the square lattice
• Discrete Jordan curve theorem for the square lattice
• Hopf's Umlaufsatz for lattice polygons

TheoremCrossing points of the regular drawing of the complete bipartite graph#✓fully proved

Let \(n\) be a natural number. In the regular drawing of \(K_{n,n}\) in \(\mathbb{Q}^2\), the left vertices are the points \((0, i)\) and the right vertices are the points \((1, j)\) for \(0 \le i, j < n\), and each edge is the straight segment from \((0, i)\) to \((1, j)\). For \(i < i'\) and \(j' < j\), the edges from \((0, i)\) to \((1, j)\) and from \((0, i')\) to \((1, j')\) cross at the point \((x, i + x(j - i))\), where \(x = (i' - i)/((i' - i) + (j - j'))\). The number of distinct points obtained in this way, over all \(i, i', j, j' < n\) with \(i < i'\) and \(j' < j\), equals \(S_1 - S_2\), where \(S_1\) is the sum of \((n - a)(n - b)\) over all ordered pairs \((a, b)\) of coprime integers with \(1 \le a, b \le n - 1\), and \(S_2\) is the sum of \((n - 2a)(n - 2b)\) over all ordered pairs \((a, b)\) of coprime integers with \(1 \le 2a \le n - 1\) and \(1 \le 2b \le n - 1\).

The difference is taken in \(\mathbb{N}\); since \(S_2 \le S_1\), it is the ordinary difference.

MetaMathlibExt.legendre_regular_crossing · 29 lines

theorem legendre_regular_crossing :
    ∀ (n : ℕ),
      Finset.card
        (Finset.image
          (fun p => match p with
            | ((i, j), (i', j')) =>
              (((i' : Rat) - (i : Rat)) /
                (((i' : Rat) - (i : Rat)) + ((j : Rat) - (j' : Rat))),
                (i : Rat) +
                  (((i' : Rat) - (i : Rat)) /
                    (((i' : Rat) - (i : Rat)) +
                      ((j : Rat) - (j' : Rat))) *
                    ((j : Rat) - (i : Rat)))))
          (Finset.filter
            (fun p => match p with
              | ((i, j), (i', j')) => i < i' ∧ j' < j)
            (Finset.product
              (Finset.product (Finset.range n) (Finset.range n))
              (Finset.product (Finset.range n) (Finset.range n))))) =
        ((∑ a ∈ Finset.filter (fun a => 1 ≤ a) (Finset.range n),
            ∑ b ∈ Finset.filter (fun b => 1 ≤ b ∧ Nat.Coprime a b)
              (Finset.range n),
            (n - a) * (n - b)) -
          (∑ a ∈ Finset.filter (fun a => 1 ≤ 2 * a ∧ 2 * a < n)
              (Finset.range n),
            ∑ b ∈ Finset.filter
              (fun b => 1 ≤ 2 * b ∧ 2 * b < n ∧ Nat.Coprime a b)
              (Finset.range n),
            (n - 2 * a) * (n - 2 * b)))

Sources

• Stéphane Legendre, "The Number of Crossings in a Regular Drawing of the Complete Bipartite Graph", Journal of Integer Sequences 12 (2009), Article 09.5.5, Proposition count_all, line 263, https://cs.uwaterloo.ca/journals/JIS/VOL12/Legendre/legendre2.tex.

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.