The regulator of the cyclic cubic field of discriminant $49$ is $\approx 0.5255$

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.

$\operatorname{Reg}(K)$ is Mathlib's NumberField.Units.regulator K: the absolute value of the determinant of the $r\times r$ matrix $\big(N_w\log\lvert\varepsilon_i\rvert_w\big)$ where $\varepsilon_1,\dots,\varepsilon_r$ ($r=r_1+r_2-1$) is a fixed (Mathlib-chosen) system of fundamental units, i.e. units whose classes form a basis of $\mathcal O_K^\times$ modulo torsion, and $w$ ranges over the infinite places other than one fixed place; for $r=0$ it is the determinant of the empty matrix, $1$. Statement. Let $K$ be a number field with $[K:\mathbb Q]=3$ and suppose there is $\alpha\in K$ with $\alpha^3+\alpha^2-2\alpha-1=0$. Then $0.5254<\operatorname{Reg}(K)$ and $\operatorname{Reg}(K)<0.5256$ (strict inequalities between real numbers).