Companion note, version 1.18

Version 1.18 records what the batch of 5 October 2026 machine-checks.

• Theorem 5.5. Let u ∉ Q̄ with uū algebraic, and z ∉ H₀ = Q̄ + Q̄u + Q̄ū. Then H₀ + Q̄z carries a rank-one 2×3 configuration (two Q̄-independent x_i, three Q̄-independent y_j, all six products x_i y_j in the space) exactly when z ∈ H₀ + Q̄w for w = u², w = ū² or w = 1/(u − a) with a algebraic and non-zero.
  • With Roy's strong six exponentials theorem, these are Diaz's exclusions at a candidate (2007, Corollaire 5(1) and 5(4)).
  • Every configuration in such a space is a geometric progression b, bh, bh², bh³, the shape of Fischler's Lemma 6.1 (2001) and Diaz's Théorème 7(2) (2007).
  • The classification was not found in the sources read. A hypothesis z ∈ ℒ̃ brings z̄ with it, and the five-dimensional spaces H₀ + Q̄z + Q̄z̄ are not covered.
• Appendix A. One new row, with the five Lean identifiers of the theorem and its steps. The mirrored project holds all 359 proved results of the development.