A distance-rigid locus has no collinear triple

Source. Carlo Perassi's manuscript C. Perassi, Rigidity of logarithms with algebraic modulus — Around a conjecture of Diaz, unpublished manuscript, 15 August 2026, statement 52 of 57, Theorem thm:elliptic-distance (Elliptic algebraic distance and plane rigidity) of Appendix C, An elliptic outlook (source line 2557) — its second half, the plane statement.

Statement, as formalised. Let k ⊆ ℂ be a subfield of algebraic numbers and D ⊆ ℂ a set such that

• every x ∈ D has algebraic norm x conj x;
• D is stable under multiplication by k^×;
• (distance dichotomy) distinct x, y ∈ D with (x−y) conj (x−y) algebraic satisfy y ∈ k^× x.

If u, v, w ∈ D with v ∉ k u, and w = a u + b v with a, b ∈ k, then a = 0 or b = 0. Equivalently: D ∩ span_k{u,v} = k^× u ⊔ k^× v, so the image of D in the projective space has no collinear triple.

What is a hypothesis and why. The manuscript's D is the elliptic Diaz locus, k the endomorphism field, and the distance dichotomy is the first half of the same theorem. That first half splits in two: an identity of quadratic algebras — the cosine rule, published on this mission as Diaz.trace_norm_quadratic_algebra and Diaz.quadratic_algebra_distance, which give u conj v algebraic and hence u/v algebraic — and then the elliptic Baker theorem of Masser and Bertrand–Masser, which converts an algebraic linear relation between elliptic logarithms into a k-linear one. Elliptic Baker is not in Mathlib and is not formalisable here, so it is carried as the explicit hypothesis hdist, together with the consequence of it that the manuscript uses a second time in the plane argument (the reduction of w to a k-combination of u and v, which appears here as the hypothesis that w has that shape). The citation boundary is therefore visible in the statement itself.

The one step that is not a citation is what is proved: if ab ≠ 0 then a u ∈ D, w ≠ a u, and (w − a u) conj (w − a u) = b conj b · v conj v is algebraic because b conj b is a product of algebraic numbers — in the manuscript, because |b|² = N(b) ∈ ℚ. The dichotomy applied to a u and w then puts w in k^× (a u), whence v ∈ k^× u, contradicting independence.

No new definition. ℒ_E and the elliptic Diaz locus do not appear; D is an arbitrary set with the three stated closure properties.

Dropped from the successor manuscript. This statement is not in C. Perassi, Rigidity of logarithms with algebraic modulus — Around a conjecture of Diaz, unpublished manuscript, 15 August 2026, the later version of the same note. The reason is scope, and the manuscript says so itself (line 119): consequences of the same machinery that concern all logarithms rather than the Diaz locus, "and the transfers to elliptic and p-adic settings, are developed separately and are not needed here." The whole of the manuscript's Appendix C (An elliptic outlook) and Appendix D (A p-adic outlook) were removed as blocks; the appendix between them, the conjugation-degree framework, was kept and promoted to a body section. Nothing was withdrawn as wrong: the manuscript still asserts that the rank inequality rank(M) > ½ r_str(M) "also governs the elliptic and p-adic appendices". The appendices were moved out, not retracted.

Novelty. No novelty is claimed, either for the mathematics or for the formalisation. The manuscript itself presents these appendices as transfers of a complex argument to another setting. Possibly known; not checked against the literature.