Replication count: every point lies on $r$ lines with $2r + 1 = n$

Setting. For a natural number $n$, write $[n] = \{0, 1, \dots, n-1\}$ for the set of $n$ points. An object $S$ of type "STS on $n$ points" consists of exactly the following data and axioms:

• a finite set $\mathcal{L}$ of subsets of $[n]$ (the lines);
• (size three) every line $\ell \in \mathcal{L}$ has exactly $3$ elements, $|\ell| = 3$;
• (unique line through a pair) for all points $x, y \in [n]$ with $x \neq y$, there is exactly one subset $\ell \subseteq [n]$ with $\ell \in \mathcal{L}$, $x \in \ell$ and $y \in \ell$.

No other conditions are imposed: there is no assumption on $n$ (such as $n \equiv 1$ or $3 \pmod 6$, or $n \geq 1$), and nothing beyond the two axioms above restricts $\mathcal{L}$.

Statement. For every natural number $n$, every such structure $S = (\mathcal{L}, \dots)$ on $[n]$, and every point $x \in [n]$, let

be the number of lines that contain $x$. The theorem asserts the equality of natural numbers

It is an unconditional equality: there is no subtraction or division in it, so no truncation or junk values arise.

Degenerate cases.

• $n = 0$. There are no points $x \in [0]$, so the statement says nothing.
• $n = 1$. The pair axiom holds vacuously. No $3$-element subset of a $1$-element set exists, so $\mathcal{L} = \varnothing$ and $r_0 = 0$. The assertion becomes $1 = 1$.
• $n = 2$. The pair axiom applied to the two distinct points requires a line of size $3$ inside a $2$-element set, which is impossible. So no structure $S$ exists for $n = 2$, and the statement is vacuous there.
• General $n$. The statement applies to every $n$ for which some structure $S$ exists, and it says nothing for any $n$ where none exists.

Unused imported definition. The imported file also defines a "role colouring" predicate (a map assigning each point–line pair one of three roles, subject to distinctness, surjectivity and injectivity conditions). That predicate does not appear in this theorem and places no condition on it.