Theorems and proofs¶

Proof. For \(n \le 2\) the only type is the empty one. For \(3 \le n \le 12\) the exhaustive search of Algorithm 1 decided every admissible type without time-outs; completeness of the search is argued there. The counts of YES answers are the stated values (runs/comb_{n}.json). The SAT encoding (Algorithm 2) returns the same verdict on every type for \(n \le 12\). \(\square\)

Proof. Lower bounds. The certificates in data/certificates/n{n}.json, one per type, are all accepted by the exact verifier; Theorem D1 below explains why acceptance proves realizability.

Upper bounds. Every combinatorially possible type without a certificate is excluded in one of three ways:

• by Theorem A2, A3 or A1, applied to its \(t_k\);
• because it has no orientable linear space (Algorithm 3, engine mode 4, runs/orient_{n}.json; the SAT implementation agrees where it finished);
• for \(n = 12\), because it is \(\{4^9\}\) (Proposition C3), \(\{3^{20}\}\) (Proposition C3a), \(\{4^5, 3^9\}\) (Proposition C3b), or \(\{6, 4, 3^{12}\}\) or \(\{6, 3^{14}\}\) (Theorems C4 and C5).

The classification files data/results/classification_n{n}.json list the reason for every type; for \(n \le 12\) none is open. \(\square\)

Proof. (1) A point on a pencil line other than \(P\) lies on exactly one pencil line, so its multiplicity is one more than the number of lines of \(\mathcal A'\) through it. It is therefore either an absorbed point of \(\mathcal A'\) or an ordinary point, and the type has the stated form.

(2) Choose \(P\) off the lines of \(\mathcal A'\) and off every line joining two of its intersection points. Join \(P\) to the points to be absorbed (at most \(\binom k2 \le m\) of them) and add generic lines through \(P\) until there are \(m\). Besides the absorbed points only ordinary points are created, and no point has more than \(m\) lines because \(\mu'(p) + 1 \le k + 1 \le m\).

The formula for \(f_0\) is a direct count of the points along the pencil lines; full details are in notes/bands.md. \(\square\)

Proof. We work in the dual picture: ten points, one line \(L\) through five of them, ten lines through three of them, and \(t_2 = 45 - 10 - 30 = 5\) lines through two of them, sixteen lines in all. Call the points on \(L\) \(Q_1, \dots, Q_5\) and the other points \(X_1, \dots, X_5\). A line other than \(L\) meets \(L\) in at most one point, so each 3-point line consists either of one \(Q_i\) and two \(X\)'s, or of three \(X\)'s.

Step 1: every 3-point line passes through some \(Q_i\). Fix \(Q_i\). The lines joining \(Q_i\) to the five \(X\)'s split the \(X\)'s into classes, one class per line; a class of size \(s\) gives an \((s+1)\)-point line, so \(s \le 2\). If \(g_i\) is the number of these lines, then \(5 - g_i\) of them are 3-point lines. Let \(\tau\) be the number of 3-point lines through some \(Q_i\), so that \(\sum_i g_i = 25 - \tau\), and let \(\lambda\) be the number of lines that contain no \(Q_i\). Counting all sixteen lines,

Since there are only ten 3-point lines, \(\tau \le 10\), and since \(\lambda \ge 0\), we get \(\tau = 10\) and \(\lambda = 0\). So every 3-point line passes through some \(Q_i\), every line through two \(X\)'s also passes through some \(Q_i\), and no three \(X\)'s are collinear. Each \(Q_i\) lies on exactly two 3-point lines, and these are two disjoint pairs \(X_jX_k\), \(X_lX_m\).

Step 2: the combinatorics is unique. Each \(Q_i\) corresponds to a pair of disjoint edges of the complete graph on \(X_1, \dots, X_5\), and the five pairs partition its ten edges. There are exactly six such partitions, and all are equivalent under relabelling the \(X\)'s (scripts/pentagon.py enumerates them). Up to relabelling,

In words: each side of the pentagon \(X_1X_2X_4X_5X_3\) meets the opposite diagonal in one of the \(Q_i\).

Step 3: the algebra. Take \(X_1, X_2, X_3, X_4\) as the projective frame and \(X_5 = (x : y : 1)\). The \(Q_i\) are polynomial in \(x\) and \(y\), and the condition that all five lie on one line is the vanishing of the ten determinants \(\det(Q_a, Q_b, Q_c)\). A Gröbner basis computation (scripts/pentagon.py, output in notes/pentagon_output.txt) shows that this system has exactly two solutions,

both real and non-degenerate (no three \(X\)'s collinear, the five \(Q_i\) distinct). They are the two Galois-conjugate projective images of the regular pentagon with its axes; in the dual picture the axes are the lines \(Q_iX_i\).

Conclusion. Every arrangement of type \(\{5, 3^{10}\}\) is projectively equivalent to one of these two. A projective transformation defined over \(\mathbb Q\) would keep \(X_5\) rational, so no realization is defined over \(\mathbb Q\). \(\square\)

Proof. Linear spaces. The Fano plane, the Möbius–Kantor configuration \(8_3\), and the affine plane \(AG(2,3)\) (the Hesse configuration \(9_4 12_3\)); the search of Algorithm 1 finds them.

Non-realizability. For \(\{3^7\}\), \(t_2 = 0\) contradicts Theorem A2; for \(\{3^{12}\}\) likewise \(t_2 = 36 - 36 = 0\).

For \(\{3^8\}\) we have \(t_2 = 4\), so the inequalities do not help. The exhaustive search shows that every linear space of this type is the Möbius–Kantor configuration, and that it admits no orientation (Algorithm 3; classically, Hilbert–Cohn-Vossen §16 or Gropp 1997⁹). \(\square\)

Proof. Consider twelve elements carrying nine blocks of size 4, any two blocks sharing at most one element. An element on four blocks would be joined to \(4 \cdot 3 = 12 > 11\) other elements, so every element lies on at most three blocks. The blocks contain \(9 \cdot 4 = 36 = 12 \cdot 3\) incidences, so every element lies on exactly three blocks.

Now swap the roles: take the nine blocks as points and the twelve elements as lines, each line consisting of the three blocks through that element. Two blocks share at most one element, so two of the nine points lie on at most one common line; and the twelve lines cover \(12 \cdot \binom 32 = 36 = \binom 92\) pairs, so every pair lies on exactly one line. This is a Steiner triple system on nine points, which is unique up to isomorphism: the affine plane \(AG(2,3)\), the Hesse configuration.

Realizability is preserved by duality, and \(AG(2,3)\) is not realizable over \(\mathbb R\): every pair of its points lies on a 3-point line, so it has no ordinary line, contradicting the Sylvester–Gallai theorem (Theorem A2). Over \(\mathbb C\) the configuration exists (the nine inflection points of a cubic and their twelve lines), so the obstruction is genuinely real. \(\square\)

Proof. Work in the dual picture: twelve points and twenty 3-point lines, which cover \(60\) of the \(66\) pairs. A point lies on \((11 - d)/2\) of the 3-point lines, where \(d\) is the number of uncovered pairs at that point, so \(d\) is odd. The twelve values of \(d\) sum to \(2 \cdot 6 = 12\), so every \(d\) equals \(1\): the uncovered pairs form a perfect matching.

Add a thirteenth point and join it to the two ends of each uncovered pair. The result is a Steiner triple system of order 13, and conversely deleting a point from a Steiner triple system of order 13 gives a linear space of type \(\{3^{20}\}\). There are exactly two Steiner triple systems of order 13 up to isomorphism.¹⁰ Their 26 point deletions fall into 5 isomorphism classes, and the SAT encoding of Algorithm 3 shows that none of the 26 admits a chirotope (scripts/orchard12.py, runs/orchard12.json). \(\square\)

Proof. Two pencils share at most one line, so the five 4-pencils are described, up to relabelling, by the lines that lie in at least two of them: a family of subsets of the five pencils, any two sharing at most one pencil. The five pencils have 20 incidences with only 12 lines, and exactly 8 such configurations fit. For each of the 8 the 4-pencils are fixed and the SAT encoding of Algorithm 3 is asked for a chirotope on a linear space of type \(\{4^5, 3^9\}\) containing them; all 8 instances are unsatisfiable, with three different solvers (CaDiCaL, Glucose, MapleChrono). As a control, the same 8 instances for the realizable type \(\{4^5, 3^8\}\) are all satisfiable (scripts/orient_split.py, runs/orient_split_12.json). \(\square\)

Proof. Uniqueness. The engine's exhaustive enumeration (mode 5) lists 283 680 linear spaces of the type (labelled, modulo its symmetry breaking), of which 30 240 are orientable; the exact isomorphism test shows that all orientable ones are relabellings of the space above (runs/enum_classes_12_6_4_3x12.json).

Forced collinearity. Take \(0, 1, 6, 7\) as projective frame, the points of the 6-block on the line \(z = 0\) and the other points in the affine chart. The 16 collinearity determinants generate an ideal \(I\) in 12 unknowns, and the Gröbner basis of \(I + (t \cdot d_{7,10,11} - 1)\) is \(\{1\}\) (data/proofs/n12_6-4-3x12.json). Hence \(d_{7,10,11}\) vanishes on \(V(I)\).

Pseudolines. Realizability by pseudolines is the Folkman–Lawrence theorem applied to the chirotope found by the engine. \(\square\)

Proof by hand. Send the 6-point line \(\{0, \dots, 5\}\) to infinity. The six points \(6, \dots, 11\) become affine points \(A, B, C, D, E, F\), and "collinear with a point of the line at infinity" becomes "parallel". The 4-block says that \(A, B, D\) are collinear, and the triples say

Put \(A = 0\), \(B = b\,u\), \(D = d\,u\) and \(C = v\), where \(u, v\) are independent (because \(A, B, C\) are not collinear) and \(b, d\) are distinct and non-zero. From \(AC \parallel BE \parallel DF\) we get \(E = b\,u + e\,v\) and \(F = d\,u + f\,v\). Then:

• \(BC \parallel DE\) gives \(d = b(e+1)\);
• \(AE \parallel BF\) gives \(bf = e(d - b) = b e^2\), so \(f = e^2\);
• \(AF \parallel CE\) gives \(d(e-1) = fb\), that is \(b(e+1)(e-1) = be^2\), that is \(-1 = 0\).

So the configuration does not exist over any field; the parallelisms \(CD \parallel EF\) and \(CF \parallel AB\) were not even needed. This is slightly stronger than the statement of the theorem: under the non-degeneracy conditions used here (\(A, B, C\) not collinear, \(A, B, D\) distinct) the collinearities have no solution at all, while the Gröbner certificate only says that every solution, degenerate or not, has \(7, 10, 11\) collinear. \(\square\)

Proof. Enumeration. engine/ls.c, mode 5.

Isomorphism classes. scripts/canon_dedupe.py computes an exact canonical form. The 6-block \(B\) is unique, so an isomorphism maps \(B\) to itself and the six other points \(X\) to themselves. Each point \(q \in B\) is recorded by the set of pairs of \(X\) that lie in a block through \(q\) (its pair-mask), and the blocks inside \(X\) by one more pair-mask. Taking the \(q\)-masks as a sorted list removes the labels of \(B\); the minimum of (sorted \(q\)-masks, \(X\)-mask) over the 720 permutations of \(X\) is then a complete invariant. An independent VF2 graph-isomorphism check agrees on the first class.

Certificates. data/proofs/n12_6-3x14.json; each is verified by a reduced Gröbner basis \(\{1\}\) in sympy. \(\square\)

Proof. Exact arithmetic. The program represents elements of \(\mathbb Z[\sqrt d]\) as integer pairs and uses only ring operations, so every computed quantity is the exact value of the corresponding expression in the real number \(\sqrt d\). An element \(p_0 + p_1\sqrt d\) with integers \(p_0, p_1\) is zero iff \(p_0 = p_1 = 0\), because \(d\) is checked to be \(0\) or a positive non-square integer, so \(\sqrt d\) is irrational (or absent). Hence every zero test is exact.

Distinct lines. The program checks that each line is a non-zero vector and that no two are proportional (cross product non-zero), so the \(n\) lines are distinct.

The type. For each pair \(i < j\) it computes the intersection point \(P = L_i \times L_j\) and the set \(S_{ij} = \{k : L_k \cdot P = 0\}\) of all lines through \(P\); the distinct sets \(S_{ij}\) are exactly the intersection points of the arrangement with their pencils, so the multiset of their sizes is the pencil type. Acceptance means this multiset, restricted to sizes \(\ge 3\), equals \(T\). \(\square\)

Proof. From Theorem A2 and \(t_2 = \binom n2 - \sum_{k\ge3}\binom k2 t_k\): \(\sum_{k\ge3}(\binom k2 + k - 3)t_k \le \binom n2 - 3\). The loss is \(\sum_{k\ge3}(\binom k2 - 1)t_k\) and \((\binom k2 - 1)/(\binom k2 + k - 3) = (k+1)/(k+3)\) increases with \(k\), so the loss is at most \(\frac{m+1}{m+3}(\binom n2 - 3)\). \(\square\)

Proof. Let \(m \le n - 3\) be the largest multiplicity and \(b = n - m \ge 3\). There are three ranges of \(n\).

Case \(n \ge 36\). If \(b \le (2n-9)/3\), Lemma E1 gives \(f_0 \ge 1 + mb - \binom b2 \ge 2n - 2\): the difference is \(n(b-2) - \frac{3b^2 - b - 6}2\), which is \(\ge 0\) when \(n \ge \frac32 b + \frac92\). Otherwise \(m < (n+9)/3\), and Lemma E2 gives \(f_0 > \frac{3n(n-1)}{n+18} \ge 2n-2\), because \(n^2 - 37n + 36 \ge 0\).

Case \(17 \le n \le 120\). The script scripts/f0_bounds.py checks that \(\max(1 + G(n,b), \lceil\text{Lemma E2}\rceil) \ge 2n-2\) for every \(m \le n-3\). This range overlaps the previous one.

Case \(13 \le n \le 16\). The same check succeeds except for \((n, m) = (13, 5), (14, 5), (14, 6), (15, 6), (16, 6)\). For these five pairs a linear programme over \((t_2, \dots, t_m)\) with the pair identity, Theorem A2, Theorem A4 (with coefficients \(k - 4\)) and \(t_m \ge 1\) has optimum \(\ge 2n - 2\). The script prints exact dual multipliers and re-verifies them coefficientwise in rational arithmetic.

For example, for \((13, 5)\) the multipliers \(\alpha = \frac5{24}\) (pairs), \(\beta = \frac7{24}\) (Melchior) and \(\gamma = \frac12\) (Hirzebruch) satisfy

hence \(f_0 \ge \frac5{24}\cdot 78 + \frac7{24}\cdot 3 + \frac12 \cdot 13 = 23.625\), that is \(f_0 \ge 24\). \(\square\)

Proof. For each \(n\) the certificates give the attained values listed on the points page. The missing values are excluded as follows.

• \(2, \dots, n-1\): by Theorem A1.
• \(n+1, \dots, 2n-5\): by Theorem A6 for \(n \ge 10\), and by the classification for \(n \le 9\).
• \(\binom n2 - 1\) and \(\binom n2 - 3\): by Theorem 1 of the points page.
• The sporadic values \(8\) (\(n = 7\)), \(9, 10\) (\(n = 8\)), \(10, 11, 12\) (\(n = 9\)) and \(21\) (\(n = 12\)): every admissible type with that \(f_0\) is non-realizable (classification files).
• \(23\) for \(n = 13\): by Theorem E3. Independently, all 81 admissible types with \(f_0 = 23\) fail the combinatorial sieve or Theorem A2 (runs/comb_13_f23.json, runs/sat_13_f23.json).

\(\square\)