Opposite conjugate planes multiply into the span of 1, u and its conjugate

Let $K \subseteq \mathbb{C}$ be a subfield and $u \in \mathbb{C}$ with $\rho = u\bar u \in K$. For $A,B,C,D \in K$ the product

lies in $K + Ku + K\bar u$.

Where this sits. This is the elementary half of Theorem 3.3 (thm:two-planes, Two saturated conjugate planes) of the manuscript: the computation

establishing $U_- \subseteq \mathcal{M}_x$ for $x = A + Bu \in U_+$, where $U_\pm = \bar{\mathbb{Q}} \oplus \bar{\mathbb{Q}}u^{\pm}$ and $\widetilde{\mathcal{L}} = \bar{\mathbb{Q}} + \operatorname{span}_{\bar{\mathbb{Q}}}\mathcal{L}$. With $K = \bar{\mathbb{Q}}$ and $u$ a Diaz candidate, the right-hand side is exactly a member of $\widetilde{\mathcal{L}}$, since $u$ and $\bar u$ are logarithms.

The one thing that makes the identity work is $u \cdot \bar u \in K$: the product of the two "opposite" generators stays in the base. This is the whole content of the chirality in the manuscript's Corollary 3.4.

What is deliberately not claimed. The reverse inclusion $\mathcal{M}_x \subseteq U_-$ is Theorem 3.2, the multiplier bound $\dim_{\bar{\mathbb{Q}}}\mathcal{M}_x \le 2$, which is Roy's strong six exponentials theorem and is not available in Mathlib. Without it the saturation — the equality $\mathcal{M}_x = U_-$ — is not asserted, and neither is the "only if" half of the chiral multiplication law.

Elementary; possibly known, not checked against the literature.

Source. Carlo Perassi, Rigidity of logarithms with algebraic modulus — Around a conjecture of Diaz (private manuscript, 15 August 2026). The mathematics is his; this node only records one step of it in Lean, and claims no novelty of its own.