Three algebraic norms force the mixed product algebraic
ProvedDiaz.quadratic_algebra_distanceSource. Carlo Perassi's manuscript C. Perassi, Rigidity of logarithms with algebraic modulus — Around a conjecture of Diaz, unpublished manuscript, 15 August 2026, statement 56 of 57, Theorem
thm:padic-distance (p-adic algebraic distance and plane rigidity, source line 2744) — the
forward implication of its first equivalence, stated over an arbitrary quadratic algebra rather
than over a quadratic extension of ℚ_p.
Statement. Let R be a commutative ring, σ a ring involution, A a subring, and suppose A
absorbs the roots of monic quadratics over it: if z² − p z + q = 0 with p, q ∈ A then z ∈ A.
If the three norms u σ u, v σ v and (u − v) σ (u − v) all lie in A, then so does the mixed
product u σ v.
The mechanism. Put z = u σ v. The trace–norm identity gives
z + σ z = N u + N v − N (u − v) ∈ A and z σ z = N u * N v ∈ A, and z is then a root of
X² − (z + σ z) X + z σ z, a monic quadratic over A — the vanishing is a bare ring identity.
The absorption hypothesis finishes it. Over ℂ with A = ℚ̄ the hypothesis holds because the
algebraic numbers are algebraically closed in ℂ; over ℂ_p it holds for the same reason, which
is the manuscript's point.
What this is not. The manuscript's full theorem concludes v / u ∈ ℚ×, and that last step
needs the p-adic Baker theorem (Brumer) to descend an algebraic linear relation to a rational one.
That input is not formalised here; this node is the part of the argument that is pure quadratic
algebra.
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 it is stated in the manuscript itself: its
introduction says that "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 A (products of logarithms) and both of
its outlook appendices (elliptic, p-adic) were removed as blocks; the intervening appendix, the
conjugation-degree framework, was kept and promoted to a body section. Nothing here was
withdrawn as wrong, and no statement in the dropped blocks was replaced by a corrected version.
It is worth recording because the argument is unconditional and short, and because a statement
that survives only in a superseded draft is the kind that gets lost.
Novelty. No novelty is claimed. Possibly known; not checked against the literature.
import Mathlib import Definitions.Def_Diaz_Closure import Definitions.Def_Diaz_Instantiation open ComplexConjugate open Diaz
theorem Diaz.quadratic_algebra_distance {R : Type*} [CommRing R] (σ : R →+* R) (hσ : ∀ x, σ (σ x) = x)
(A : Subring R)
(hquad : ∀ z p q : R, p ∈ A → q ∈ A → z * z - p * z + q = 0 → z ∈ A)
{u v : R} (hu : u * σ u ∈ A) (hv : v * σ v ∈ A)
(huv : (u - v) * σ (u - v) ∈ A) :
u * σ v ∈ A := by sorry