A logarithmic modulus forces independence, from the master dichotomy

Source. This is the Corollary A logarithmic modulus forces independence, statement 42 of C. Perassi, Rigidity of logarithms with algebraic modulus — Around a conjecture of Diaz, unpublished manuscript, 15 August 2026, the predecessor manuscript of Carlo Perassi's note on Diaz's modulus conjecture. The manuscript states that the corollary is not its own: it is Exercise 15.16(c) of M. Waldschmidt, Diophantine Approximation on Linear Algebraic Groups, whose hint attributes it to Diaz. It is ported here as an attributed legacy node. Neither the statement nor its attribution has been verified against the original; both were transcribed from C. Perassi, Rigidity of logarithms with algebraic modulus — Around a conjecture of Diaz, unpublished manuscript, 15 August 2026.

Statement. Let $\lambda$ be a non-zero logarithm of an element of a conjugation-stable subfield $K\subset\mathbb C$ (at $K=\overline{\mathbb Q}$: $\lambda\in\mathcal L\setminus\{0\}$), with $\lambda\notin\mathbb R$, and suppose $|\lambda|$ is again such a logarithm. Then

Provenance of the carried hypothesis. The dichotomy hMaster is the Theorem Master dichotomy for rationally proportional products of C. Perassi, Rigidity of logarithms with algebraic modulus — Around a conjecture of Diaz, unpublished manuscript, 15 August 2026, the predecessor manuscript of Carlo Perassi's note on Diaz's modulus conjecture. In that manuscript it is derived from Roy and Waldschmidt's Théorème 0.2 (M. Waldschmidt and D. Roy, 1997; the dichotomy form), and the manuscript records that its $m=1$ case is Exercise 1.8 / the worked example of §12.5 of M. Waldschmidt, Diophantine Approximation on Linear Algebraic Groups. That statement was transcribed from C. Perassi, Rigidity of logarithms with algebraic modulus — Around a conjecture of Diaz, unpublished manuscript, 15 August 2026 and has not been verified against its own source; the sources are not held on this mission. It is therefore carried as the explicit hypothesis hMaster rather than asserted: this node asserts only the implication.

What the node proves. Apply hMaster to $(\mu_1,\nu_1,\mu_2,\nu_2)=(\lambda,\overline\lambda,|\lambda|,|\lambda|)$ with $m=1$; all four entries are non-zero logarithms, and $|\lambda|^2=\lambda\overline\lambda$. The first alternative gives $|\lambda|\in\mathbb Q^\times\lambda$ and the second $|\lambda|\in\mathbb Q^\times\overline\lambda$; taking imaginary parts, either makes $\lambda$ real, which is excluded. Only the transcendence-degree alternative survives. That elimination — the unconditional core of the corollary — is the content actually verified here.

Scope of the conclusion. The manuscript states the conclusion as "$\lambda$ and $\overline\lambda$ are algebraically independent over $\mathbb Q$; equivalently $\operatorname{trdeg}_{\mathbb Q}\mathbb Q(\lambda,|\lambda|)=2$". What is recorded here is the lower bound $\ge 2$ that the dichotomy yields directly. The passage from it to algebraic independence of the pair, and to the exact value $2$, uses the standard extraction of a transcendence basis from a generating set together with $\overline\lambda=|\lambda|^2/\lambda$; that step is not formalised in this node.

Formalization note. $K$ is an arbitrary subfield of $\mathbb C$ with hKconj asserting stability under complex conjugation — the property of $\mathcal L$ the manuscript uses to know $\overline\lambda\in\mathcal L$. "$\lambda\notin\mathbb R$" is lam.im ≠ 0, and $|\lambda|$ is ((‖lam‖ : ℝ) : ℂ). #print axioms on the submitted proof: [propext, Classical.choice, Quot.sound].