$1$, $\nu$ and $p$ are $K$-independent when $p\nu$ is a non-zero element of $K$

Source. This is Carlo Perassi's mathematics, from his unpublished note on Diaz's modulus conjecture, section Polar coordinates and the discreteness of the period, statement Theorem (Non-real two-point fibres force $e^{\pi^2}$ transcendental), the independence step in its proof. Published on his mission with his permission. No novelty is claimed for it here; the argument is elementary, and it is possibly known — it has not been checked against the literature.

Statement. Let $K \subset \mathbb{C}$ be a subfield, $p$ transcendental over $K$, and $\nu \in \mathbb{C}$ with $\beta := p\nu \in K \setminus \{0\}$. Then $1$, $\nu$, $p$ are linearly independent over $K$.

Where it sits, and what it does not claim. In the manuscript this is the step that prepares Diaz's Corollaire 2 (P)(1) of 2007 for the triple $(\lambda_1,\lambda_2,\lambda_3) = (i\pi, \nu, i\pi)$, with $K = \overline{\mathbb{Q}}$ and $p = i\pi$ (transcendental by Lindemann). Applied there, Diaz's corollary gives $\{(i\pi)\nu, (i\pi)^2\} \not\subset \widetilde{\mathcal{L}}$; since $(i\pi)\nu \in \overline{\mathbb{Q}}$, one gets $\pi^2 \notin \widetilde{\mathcal{L}}$ and hence $e^{\pi^2}$ transcendental, under the hypothesis that some algebraic exponential fibre contains two candidates with $\alpha \notin \mathbb{R}$.

That conditional conclusion is not what this node asserts. Diaz's corollary is a deep input with no Mathlib formalisation at this revision, and the augmented logarithm space $\widetilde{\mathcal{L}}$ is not among the mission's definitions. What is recorded here is only the elementary independence step, which is self-contained and needs nothing beyond the transcendence of $p$ over $K$. A contributor who formalises Diaz's Corollaire 2 can compose it with this node to obtain the $e^{\pi^2}$ statement.

Proof. Multiply $A + B\nu + Cp = 0$ by $p$: since $p\nu = \beta$, this reads $Cp^2 + Ap + B\beta = 0$, a quadratic relation for $p$ with all three coefficients in $K$. As $p$ is transcendental over $K$, the polynomial $CX^2 + AX + B\beta \in K[X]$ must be zero, so $C = A = 0$ and $B\beta = 0$; $\beta \neq 0$ then forces $B = 0$.