A role colouring puts every point on exactly $3$ lines

Proved

RolesForceSeven.three_lines

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

combinatoricsfano-planesteiner-triple-systems

Let $S$ be a Steiner triple system on $[n]$ with a role colouring $\rho$ . Then every point $x$ lies on exactly

3

lines. Completeness gives three lines through $x$ with three different roles, so at least $3$ ; minimality makes "line $\mapsto$ role of $x$ on it" one-to-one into $\{0,1,2\}$ , so at most $3$ .

Preamble

import Mathlib
import Definitions.Def_RolesForceSeven_sts

Formal statement

namespace RolesForceSeven
theorem three_lines (n : ℕ) (S : STS n) (role : Fin n → Finset (Fin n) → Fin 3)
    (h : RoleColouring S role) (x : Fin n) :
    (S.lines.filter (fun l => x ∈ l)).card = 3 := by sorry
end RolesForceSeven

Source

Shape Zero LLC, "Formal Proofs of the C1 Verification Package" (August 2026), §3.1, Definition 3.5 (the role postulates force r = 3): 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

Theorem three_lines. Let $n \ge 0$ be a natural number and write $[n] = \{0, 1, \dots, n-1\}$ (a set with exactly $n$ elements, empty when $n = 0$ ). Let $S$ be a Steiner triple system on $[n]$ , which here means a finite collection $\mathcal{L}$ of subsets of $[n]$ (the lines; it is a set of subsets, so no line is listed twice) such that

every line has exactly $3$ elements: $|l| = 3$ for all $l \in \mathcal{L}$ ;
every pair of distinct points lies on exactly one line: for all $x, y \in [n]$ with $x \ne y$ there is a unique $l \in \mathcal{L}$ with $x \in l$ and $y \in l$ .

Let $\mathrm{role}$ be an arbitrary function that takes a point $x \in [n]$ and an arbitrary subset $A \subseteq [n]$ and returns a value $\mathrm{role}(x, A) \in \{0, 1, 2\}$ . It is defined on all pairs (point, subset), including subsets that are not lines and points not in the subset; only the values $\mathrm{role}(x, l)$ with $l \in \mathcal{L}$ and $x \in l$ are constrained below. Assume $\mathrm{role}$ is a role colouring of $S$ , i.e. all three of the following hold:

Injective on each line: for every line $l \in \mathcal{L}$ and all $x, y \in l$ ,

\mathrm{role}(x, l) = \mathrm{role}(y, l) \implies x = y .

Every role is realised at every point: for every point $x \in [n]$ and every $\rho \in \{0, 1, 2\}$ there exists a line $l \in \mathcal{L}$ with $x \in l$ and $\mathrm{role}(x, l) = \rho$ .
Injective on the lines through a point: for every point $x \in [n]$ and all lines $l, l' \in \mathcal{L}$ with $x \in l$ and $x \in l'$ ,

\mathrm{role}(x, l) = \mathrm{role}(x, l') \implies l = l' .

Then, for every point $x \in [n]$ , the number of lines containing $x$ is exactly three:

\bigl|\{\, l \in \mathcal{L} : x \in l \,\}\bigr| = 3 .

Degenerate cases. When $n = 0$ there are no points, so the conclusion (which is about a point $x \in [n]$ ) is vacuous. When $n = 1$ or $n = 2$ , no $3$ -element subsets exist, so $\mathcal{L} = \varnothing$ ; for $n = 2$ the pair condition then cannot hold (no Steiner triple system exists), and for $n = 1$ condition 2 of the role colouring fails (the single point lies on no line), so in both cases the hypotheses are unsatisfiable and the statement is vacuous. For larger $n$ the hypotheses require both that $S$ is a Steiner triple system on $[n]$ and that a role colouring of it exists; nothing else about $n$ is assumed.

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

A role colouring puts every point on exactly 333 lines

A role colouring puts every point on exactly $3$ lines