Corollary A: the Fano plane has a role colouring

Proved

RolesForceSeven.fano_has_role_colouring

by ShapeZero · Sep 24, 2026 · Mathlib 0df444a (Lean v4.33.1)

combinatoricsfano-planesteiner-triple-systems

The Fano plane on $\{0, \dots, 6\}$ , with lines $\{i, i+1, i+3\}$ modulo $7$ , admits a role colouring. One colouring: on the line starting at $i$ , give $i$ role $0$ , $i+1$ role $1$ and $i+3$ role $2$ . Equivalently, $\rho(x, \ell) = 0$ if $\ell = L_x$ , $1$ if $\ell = L_{x-1}$ , and $2$ otherwise.

This shows the hypotheses of the goal are satisfiable, so the goal is not vacuously true. (The Fano plane has $48$ role colourings in total; only existence is asserted.)

Preamble

import Mathlib
import Definitions.Def_RolesForceSeven_fano

Formal statement

namespace RolesForceSeven
theorem fano_has_role_colouring : ∃ role, RoleColouring fano role := by sorry
end RolesForceSeven

Source

Shape Zero LLC, "Formal Proofs of the C1 Verification Package" (August 2026), §3.1, Theorem 3.6 (existence of a role colouring of the Fano plane): https://github.com/ShapeZeroSZ/shape-zero/blob/main/01_source/proofs/ShapeZero_C1_Formal_Proofs.pdf ; corrected in "Errata — C1 Formal Proofs (Sections 3 and 6)", Section 3: https://github.com/ShapeZeroSZ/shape-zero/blob/main/01_source/proofs/ERRATUM_Theorem_6.1.md ; public references: Wikipedia, "Steiner system" (Steiner triple systems, replication number): https://en.wikipedia.org/wiki/Steiner_system ; Wikipedia, "Fano plane": https://en.wikipedia.org/wiki/Fano_plane ; Wikipedia, "Octonion" (Fano plane mnemonic for the multiplication of imaginary units): https://en.wikipedia.org/wiki/Octonion

Read-back

What the Lean code literally says, in plain math · claude-opus-5-5

Setting. Points are the seven elements of $\mathbb{Z}/7 = \{0,1,\dots,6\}$ (addition wraps modulo 7). For each $i \in \mathbb{Z}/7$ the set $L_i = \{i,\ i+1,\ i+3\}$ is defined, and the structure $\mathcal{F}$ (called "fano") has as its lines exactly the image $\{L_i : i \in \mathbb{Z}/7\}$ , namely the seven 3-element sets

\{0,1,3\},\ \{1,2,4\},\ \{2,3,5\},\ \{3,4,6\},\ \{0,4,5\},\ \{1,5,6\},\ \{0,2,6\}.

As part of its definition, $\mathcal{F}$ carries the facts that every line has exactly 3 points and that any two distinct points lie together on exactly one line (these facts are part of the structure, not of the theorem's claim). Each point lies on exactly three of these lines.

Role colouring. A "role function" is an arbitrary function $r$ assigning to every point $x \in \mathbb{Z}/7$ and every subset $S \subseteq \mathbb{Z}/7$ a value $r(x,S) \in \{0,1,2\}$ ; it is defined on all pairs (point, subset), including subsets that are not lines and points not on the subset, but only its values $r(x,\ell)$ with $\ell$ a line and $x \in \ell$ are constrained below. Such an $r$ is a role colouring of $\mathcal{F}$ when all three of the following hold:

Distinct roles within a line: for every line $\ell$ and all points $x, y \in \ell$ , if $r(x,\ell) = r(y,\ell)$ then $x = y$ . (Since each line has 3 points and there are 3 values, the three points of a line receive the three values $0,1,2$ once each.)
Every role is taken at every point: for every point $x$ and every $\rho \in \{0,1,2\}$ there exists a line $\ell$ with $x \in \ell$ and $r(x,\ell) = \rho$ .
Distinct roles at a point: for every point $x$ and all lines $\ell, \ell'$ with $x \in \ell$ and $x \in \ell'$ , if $r(x,\ell) = r(x,\ell')$ then $\ell = \ell'$ . (Together with 2 and the fact that each point is on exactly three lines, the three lines through $x$ receive the three values $0,1,2$ once each.)

The statement. There exists a function $r : \mathbb{Z}/7 \times \mathcal{P}(\mathbb{Z}/7) \to \{0,1,2\}$ that is a role colouring of $\mathcal{F}$ in the above sense. This is a pure existence claim about this specific seven-line configuration: nothing is asserted about uniqueness, about the number of such colourings, about other Steiner triple systems, or about any other orderings or relabellings of the points.

Human review

Endorsed by Shuze Chen · Sep 24, 2026
Confirmed by the moderator at approval.
Endorsed by ShapeZero · Sep 24, 2026
Confirmed by the mission captain (proposal self-audit).

View graph