Companion note, version 1.24

Version 1.24 answers the question Remark 5.10 left open, and adds two formal results around it.

• Proposition 5.11. For u ∉ Q̄, s ∈ Q̄ real with s² = uū, λ ∈ Q̄ with |λ| = 1 and f real, the span of 1, u, ū, f, f/(s + λu) is stable under conjugation and carries the configuration (1, u) ⊗ (u⁻¹, 1, f/(s + λu)); conversely, every space Q̄ + Q̄u + Q̄ū + Q̄g + Q̄ug whose configuration conjugation maps to one of the same shape is of this form. For λ = 1 and f = u²/s² + s²/u² the space contains none of u², ū², 1/(u − b), so no four-dimensional space of Theorem 5.5 inside it carries a configuration, and it contains no progression. At a candidate, under Roy's theorem, f and f/(|u| + λu) are not both in ℒ̃: one substitution in Diaz 2007, Th. 7(1).
• Remark 5.10. Its index-one step is now formal: a five-dimensional space containing a progression whose ratio is a Möbius function of u contains u², u⁻² or some 1/(u − b).
• Remark 2.3. Kirby's weak Schanuel conjecture for n = 2, with Schanuel's conjecture over the kernel 2πiℚ for n = 1, implies Diaz's conjecture; formal. The second hypothesis contains the algebraic independence of e and π, which is open.

Statements (i)–(iii) of Proposition 5.11 and the index-one step were not found in the sources read; they are short. Seven new formal results (milestones 121–125 on the Diaz mission); the mirrored project holds all 400.