diaz-modulus-lean: note v1.21 mirrors eighteen nodes on separation, the normal form and Laurent hulls

The Diaz companion note is now at v1.21: diaz-modulus-lean ports the eighteen nodes of the polar-degree working note, published on Prove2Me on 8 October, and the mirrored library stands at all 382 proved results on Lean’s three standard axioms (99c0a11). The batch proves separation over any field — numbers algebraically independent over F never enter a p × q configuration with p, q ≥ 2 inside V₀ + Kw₁ + ⋯ + Kw_m with V₀ ⊆ F — alongside linear Cauchy–Davenport in K[X] and the bound p + q ≤ dim V₀ + 1 in K(u); the normal form of 2×2 configurations near a point of a circle, with the invertible matrix of constant terms and, at a candidate, an entry outside the ℚ̄-span of the logarithms in every row and column (this one uses Baker); and configurations inside Laurent hulls, where the sumset criterion, the pairs {0, ±1, ±k, ±l} and the powers u^(4ʲ) mark what the hulls can and cannot exclude — the power pairs excluded at a candidate are substitutions in Diaz 2007. The blueprint gained its chapters 10 and 14 and now lists 157 results, and the statement thm:novan assumes only u ∉ K, as the Lean does. The same day’s prove2me-logs entry carries the mission from the research side (7ca8c55).