The regulator is independent of the generators and of the deleted column, and positive

Non-blind read-back — not independent testimony. This read-back was written by the same agent (Aristotle, by Harmonic) that drafted this Lean statement, at the explicit request of the account owner. Its author knew the intended meaning while writing it, so it must not be mistaken for a blind audit by an independent reviewer. Please compare it against the Lean code itself.

Throughout, $K$ is a number field (a field of characteristic zero that is finite-dimensional over $\mathbb Q$), $\mathcal O_K$ is its ring of integers and $\mathcal O_K^\times$ the unit group. $r_1$ denotes the number of real infinite places of $K$ and $r_2$ the number of complex infinite places (each complex place corresponds to a pair of complex-conjugate embeddings $K\to\mathbb C$). For an infinite place $w$ of $K$, $\lvert x\rvert_w$ denotes the absolute value $\lvert\sigma(x)\rvert$ for an embedding $\sigma$ inducing $w$, and $N_w$ is $1$ if $w$ is real and $2$ if $w$ is complex. $\log$ is the real logarithm (Mathlib's convention gives $\log 0 = 0$, but units have $\lvert u\rvert_w>0$). Let $r=r_1+r_2-1$ (truncated subtraction). Statement. Let $K$ be a number field (with a chosen decidable equality on its infinite places, needed to form determinants; the value does not depend on it). Let $u,v:\{0,\dots,r-1\}\to\mathcal O_K^\times$ be families of units such that every unit $x$ can be written as $x=\zeta\prod_i u_i^{n_i}$ for some unit $\zeta$ of finite order and some integers $n_i$, and likewise for $v$ (only existence of such a representation is assumed, not uniqueness). Let $w_1,w_2$ be infinite places, and let $e_1$ (resp. $e_2$) be any bijection from the set of infinite places different from $w_1$ (resp. $w_2$) onto $\{0,\dots,r-1\}$. Define the square matrix $M_1$ with rows and columns indexed by the places $\neq w_1$ by $(M_1)_{i,j}=N_j\log\lvert u_{e_1(i)}\rvert_j$, and $M_2$ analogously with $w_2,e_2,v$. Then