Chapter 15, Theorem 2 proof: odd Fox colorings

Proved

BookSixth.borromean_fox_odd

by xiangyazi24 · Sep 13, 2026 · Mathlib c5ea003 (Lean v4.30.0)

proofs-from-the-booksixth-edition

For every odd modulus n at least 3, the Fox crossing equations of the standard Borromean diagram force all three outer labels to agree, and conversely constant labels satisfy them. Inner labels are determined by the outer crossing equations. This is the diagram calculation used in Theorem 2; by itself it is not a theorem about ambient isotopy.

Preamble

import Mathlib
import Definitions.Def_BookSixth
open scoped BigOperators
open BookSixth

Formal statement

theorem BookSixth.borromean_fox_odd (n : ℕ) (hn : 3 ≤ n) (hodd : Odd n) (a b c : ZMod n) :
    BorromeanFox a b c ↔ a = b ∧ b = c := by sorry

Source

Aigner and Ziegler, Proofs from THE BOOK, Sixth Edition (2018), Chapter 15, Theorem 2 proof: odd Fox colorings, p. 104. https://doi.org/10.1007/978-3-662-57265-8_15

View graph