Steiner triple systems on $n$ points and role colourings

Definition

RolesForceSeven_sts

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

combinatoricsfano-planesteiner-triple-systems

Fix $n \in \mathbb{N}$ and take the points $[n] = \{0, 1, \dots, n-1\}$ . A Steiner triple system on $[n]$ is a finite family $\mathcal{L}$ of subsets of $[n]$ , called lines, such that

every line has exactly $3$ points, and
every two distinct points $x \neq y$ lie together on exactly one line.

A role colouring of such a system is a function $\rho$ assigning to each point $x$ and each line $\ell$ a role $\rho(x, \ell) \in \{0, 1, 2\}$ , such that

the three points of each line receive three different roles;
completeness: for every point $x$ and every role $r$ there is a line $\ell \ni x$ with $\rho(x, \ell) = r$ ;
minimality: two different lines through the same point $x$ give $x$ different roles.

Formalization Note Points are Fin n and lines are Finset (Fin n). The role function has type Fin n → Finset (Fin n) → Fin 3; only its values $\rho(x, \ell)$ with $\ell$ a line and $x \in \ell$ are constrained. No condition is placed on $n$ , so the empty system ( $n = 0$ , no lines) is allowed.

Definition code

import Mathlib

namespace RolesForceSeven

/-- A Steiner triple system on the points `Fin n`: every line has three points,
and every pair of distinct points lies on exactly one line. -/
structure STS (n : ℕ) where
  lines : Finset (Finset (Fin n))
  card_three : ∀ l ∈ lines, l.card = 3
  pair_unique : ∀ x y : Fin n, x ≠ y → ∃! l, l ∈ lines ∧ x ∈ l ∧ y ∈ l

/-- A role colouring (C1 Definition 3.5). `role x l` is the role of point `x` on
line `l`; only its values for `x ∈ l ∈ lines` matter. -/
def RoleColouring {n : ℕ} (S : STS n) (role : Fin n → Finset (Fin n) → Fin 3) :
    Prop :=
  -- the three points of a line get different roles
  (∀ l ∈ S.lines, ∀ x ∈ l, ∀ y ∈ l, role x l = role y l → x = y) ∧
  -- completeness: every point takes every role at least once
  (∀ x : Fin n, ∀ ρ : Fin 3, ∃ l ∈ S.lines, x ∈ l ∧ role x l = ρ) ∧
  -- minimality: every point takes every role at most once
  (∀ x : Fin n, ∀ l ∈ S.lines, ∀ l' ∈ S.lines, x ∈ l → x ∈ l' →
      role x l = role x l' → l = l')

end RolesForceSeven

Source

Shape Zero LLC, "Formal Proofs of the C1 Verification Package" (August 2026), §3, Definition 3.1 (Steiner triple system) and Definition 3.5 (role colouring): 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

Structure STS n (a "Steiner triple system" on $n$ points). For a natural number $n$ (any $n \ge 0$ , with no congruence or size condition imposed), let $[n] = \{0, 1, \dots, n-1\}$ be the point set. An object $S$ of type $\mathrm{STS}(n)$ consists of:

a finite family $\mathcal{L} = S.\mathrm{lines}$ of subsets of $[n]$ , called lines;
a proof that every line has exactly three elements: $\forall\, \ell \in \mathcal{L},\ |\ell| = 3$ ;
a proof that every two distinct points lie together in exactly one line:

\forall\, x, y \in [n],\quad x \neq y \implies \exists!\, \ell \subseteq [n] \text{ such that } \ell \in \mathcal{L},\ x \in \ell,\ y \in \ell.

Here $\exists!$ ranges over all subsets $\ell$ of $[n]$ , but because membership $\ell \in \mathcal{L}$ is part of the condition, it says exactly: there is one and only one line of $\mathcal{L}$ containing both $x$ and $y$ .

Nothing else is required: $\mathcal{L}$ may be empty, and no condition on $n$ is stated. Degenerate cases: for $n = 0$ and $n = 1$ there are no pairs of distinct points, so the pair condition is vacuous and the empty family $\mathcal{L} = \varnothing$ gives a valid $\mathrm{STS}(n)$ (for $n = 0$ it is the only one; for $n = 1$ it is also the only one, since a line would need 3 points). For $n = 2$ no $\mathrm{STS}(2)$ exists (the two points would need a common 3-element line inside a 2-element set). The two proof fields carry no data, so an $\mathrm{STS}(n)$ is determined by its family of lines.

Definition RoleColouring S role. Let $n \in \mathbb{N}$ , let $S$ be an $\mathrm{STS}(n)$ with line family $\mathcal{L}$ , and let

r : [n] \times \mathcal{P}([n]) \to \{0, 1, 2\}, \qquad (x, \ell) \mapsto r(x, \ell),

be an arbitrary function assigning a "role" in $\{0,1,2\}$ to every point $x$ and every subset $\ell \subseteq [n]$ — not only to lines, and not only to pairs with $x \in \ell$ . The values of $r$ at pairs $(x,\ell)$ where $\ell \notin \mathcal{L}$ or $x \notin \ell$ are never mentioned below and are completely unconstrained. The proposition " $r$ is a role colouring of $S$ " is the conjunction of the following three conditions:

Distinct roles within a line. For every line $\ell \in \mathcal{L}$ and all $x, y \in \ell$ : if $r(x,\ell) = r(y,\ell)$ then $x = y$ . That is, $x \mapsto r(x,\ell)$ is injective on $\ell$ ; since $|\ell| = 3 = |\{0,1,2\}|$ , the three points of each line receive the three roles $0, 1, 2$ bijectively.
Every point plays every role. For every point $x \in [n]$ and every role $\rho \in \{0,1,2\}$ there exists a line $\ell \in \mathcal{L}$ with $x \in \ell$ and $r(x,\ell) = \rho$ .
Distinct roles at a point. For every point $x \in [n]$ and all lines $\ell, \ell' \in \mathcal{L}$ with $x \in \ell$ and $x \in \ell'$ : if $r(x,\ell) = r(x,\ell')$ then $\ell = \ell'$ . That is, for fixed $x$ , the map $\ell \mapsto r(x,\ell)$ is injective on the lines through $x$ .

Conditions 2 and 3 together say that, for each point $x$ , the map $\ell \mapsto r(x,\ell)$ is a bijection from the set of lines through $x$ onto $\{0,1,2\}$ ; in particular every point lies on exactly three lines. Degenerate cases: for $n = 0$ all three conditions are vacuous, so every $r$ (there is only one function on an empty domain) is a role colouring of the (empty) $\mathrm{STS}(0)$ . For $n = 1$ the only $\mathrm{STS}(1)$ has no lines, so condition 2 fails for the single point and no role colouring exists. More generally, for $n \ge 1$ , in an $\mathrm{STS}(n)$ each point lies on exactly $(n-1)/2$ lines (by the pair condition and $|\ell| = 3$ ), so the requirement "exactly three lines through each point" can only be met when $n = 7$ ; for every other $n \ge 1$ the predicate is unsatisfiable.

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

Steiner triple systems on nnn points and role colourings

Steiner triple systems on $n$ points and role colourings