Companion note, version 1.21

Version 1.21 puts the rank-one results of Section 5 into one mechanism, over any subfield K of ℂ.

• Theorem 5.12. Separation: numbers algebraically independent over F never enter a p×q configuration (p, q ≥ 2) in V₀ + Kw₁ + … + Kw_m with V₀ ⊆ F. Near a point of a circle, configurations in K + Ku + Kū have p + q ≤ 4, and the 2×2 ones are exactly x = μ·P(1, u), y = μ⁻¹·Q(1, ū) with P, Q ∈ GL₂(K). With generic numbers added they stay 2×2, their constant terms form an invertible matrix, and at a candidate every row and column has an entry outside the Q̄-span of the logarithms.
• Proposition 5.13. A Laurent hull span{uˢ : s ∈ S} carries a p×q configuration iff S contains a sumset A + B with |A| = p, |B| = q. For {0, ±1, ±k, ±l}, 4 ≤ k < l, a 2×3 configuration exists iff l ∈ {k+1, k+2, 2k−1, 2k, 2k+1, 3k}; the hull of {0, ±1} ∪ {±4ʲ} carries none.
• Remark 5.14. The pairs of powers excluded at a candidate are substitutions in Diaz 2007; linear Cauchy–Davenport is a case of Eliahou–Lecouvey, as stated by Bachoc–Serra–Zémor. Separation, the normal form and the Laurent criterion were not found in the sources read.
• Theorem 4.1 (no vanishing coefficient) now assumes only u ∉ K, as its Lean statement does.

Eighteen new formal results (milestones 111–115 on the Diaz mission); the mirrored project holds all 382.