The role postulates force exactly seven points

Theorem roles_force_seven. Let $n$ be a natural number with $n > 0$, and write $[n] = \{0, 1, \dots, n-1\}$ for the point set.

The structure $S$. In the code, $S$ is a "Steiner triple system on $[n]$". It is given by a finite family $\mathcal{L}$ of subsets of $[n]$, called lines, such that:

• every line $\ell \in \mathcal{L}$ has exactly $3$ elements;
• for every two distinct points $x \neq y$ in $[n]$ there is exactly one line $\ell \in \mathcal{L}$ with $x \in \ell$ and $y \in \ell$.

Nothing else is required. There is no divisibility or admissibility condition on $n$, and no stated requirement that every point lies on a line. (For $n \ge 2$ that follows from the pair condition. For $n = 1$ there are no pairs, and since $[1]$ has no $3$-element subsets, $\mathcal{L} = \emptyset$. For $n = 2$ no such structure exists.)

The role function. The theorem also takes an arbitrary function

written $\mathrm{role}(x, \ell)$. It is defined on every pair of a point and a subset of $[n]$, but the hypothesis below only uses its values at pairs $(x, \ell)$ with $\ell \in \mathcal{L}$ and $x \in \ell$. The hypothesis $h$ says that $\mathrm{role}$ is a "role colouring" of $S$, meaning all three of the following conditions hold:

1. Distinct roles within a line: for every line $\ell \in \mathcal{L}$ and all $x, y \in \ell$,

Since lines have $3$ points, the three points of each line receive the three roles $0, 1, 2$ in some order. 2. Every role occurs at every point: for every point $x \in [n]$ and every role $\rho \in \{0, 1, 2\}$, there is a line $\ell \in \mathcal{L}$ with $x \in \ell$ and $\mathrm{role}(x, \ell) = \rho$. 3. Each role at most once per point: for every point $x \in [n]$ and all lines $\ell, \ell' \in \mathcal{L}$ with $x \in \ell$ and $x \in \ell'$,

Together, conditions 2 and 3 say that for each point $x$, the map $\ell \mapsto \mathrm{role}(x, \ell)$ is a bijection from the lines through $x$ onto $\{0, 1, 2\}$. So every point lies on exactly three lines.

Conclusion. For every such $n > 0$, every such $S$ and every such $\mathrm{role}$ satisfying conditions 1–3,

The conclusion is only about $n$. It says nothing more about $S$ or $\mathrm{role}$, and it does not claim that a structure satisfying the hypotheses exists for $n = 7$.

Degenerate cases. The case $n = 0$ is excluded by the hypothesis $n > 0$. For $n = 1$ the hypotheses cannot all hold: $\mathcal{L} = \emptyset$, so condition 2 fails. For $n = 2$ no $S$ exists at all. In both of these cases the statement is vacuously true.