theorem HexPolyZTheory.norm_pow_sub_pow_le {x y : ℂ} {C : ℝ} (hx : ‖x‖ ≤ C) (hy : ‖y‖ ≤ C) (hC : 1 ≤ C) (i : ℕ) : ‖y ^ i - x ^ i‖ ≤ ↑i * C ^ (i - 1) * ‖y - x‖

The divided-difference entry bound: ‖yⁱ − xⁱ‖ ≤ i · Cⁱ⁻¹ · ‖y − x‖ when ‖x‖, ‖y‖ ≤ C and 1 ≤ C. Follows from the geometric factorisation yⁱ − xⁱ = (∑_{l<i} yˡ xⁱ⁻¹⁻ˡ)(y − x).

theorem HexPolyZTheory.sqrt_sum_pow_sq_le (a : ℂ) (N : ℕ) : √(∑ i : Fin N, ‖a ^ ↑i‖ ^ 2) ≤ √↑N * max 1 ‖a‖ ^ (N - 1)

The L² norm of an ordinary Vandermonde column: √(∑ᵢ ‖aⁱ‖²) ≤ √N · max(1,‖a‖)^{N-1}.

theorem HexPolyZTheory.sqrt_sum_sub_pow_sq_le {x y : ℂ} {C : ℝ} (hx : ‖x‖ ≤ C) (hy : ‖y‖ ≤ C) (hC : 1 ≤ C) (N : ℕ) : √(∑ i : Fin N, ‖y ^ ↑i - x ^ ↑i‖ ^ 2) ≤ C ^ (N - 2) * ‖y - x‖ * √(∑ i : Fin N, ↑↑i ^ 2)

The L² norm of the isolating (differenced) Vandermonde column: √(∑ᵢ ‖yⁱ − xⁱ‖²) ≤ C^{N-2} · ‖y − x‖ · √(∑ᵢ i²).

theorem HexPolyZTheory.sqrt_sum_sq_le (N : ℕ) : √(∑ i : Fin N, ↑↑i ^ 2) ≤ √↑N ^ 3

√(∑_{i<N} i²) ≤ (√N)³.

theorem HexPolyZTheory.norm_det_vandermonde_le {N : ℕ} (hN : 2 ≤ N) (c : ℂ) (α : Fin N → ℂ) {i₀ i₁ : Fin N} (hne : i₀ ≠ i₁) (hle : ‖α i₀‖ ≤ ‖α i₁‖) : ‖c‖ ^ (N - 1) * ‖(Matrix.vandermonde α).det‖ ≤ √↑N ^ (N - 1) * √(∑ i : Fin N, ↑↑i ^ 2) * (‖c‖ * ∏ j : Fin N, max 1 ‖α j‖) ^ (N - 1) * ‖α i₁ - α i₀‖

Mahler's isolating-column bound. For a leading coefficient c and points α : Fin N → ℂ with ‖α i₀‖ ≤ ‖α i₁‖, the scaled Vandermonde determinant is bounded by √N^{N-1} · √(∑ i²) · (‖c‖ · ∏ max(1,‖α j‖))^{N-1} · ‖α i₁ − α i₀‖.

theorem HexPolyZTheory.norm_prod_roots_eq_sq {N : ℕ} (α : Fin N → ℂ) (hα : Function.Injective α) : ‖(Multiset.map (fun (x : ℂ) => (Multiset.map (fun (y : ℂ) => x - y) ((Multiset.map α Finset.univ.val).erase x)).prod) (Multiset.map α Finset.univ.val)).prod‖ = ‖(Matrix.vandermonde α).det‖ ^ 2

The off-diagonal root-difference product equals ‖det V‖² in norm.

theorem HexPolyZTheory.norm_discr_eq {N : ℕ} (α : Fin N → ℂ) (hα : Function.Injective α) {f : Polynomial ℂ} (hf : 0 < f.degree) (hsplit : f.Splits) (hroots : f.roots = Multiset.map α Finset.univ.val) : ‖f.discr‖ = ‖f.leadingCoeff‖ ^ (2 * f.natDegree - 2) * ‖(Matrix.vandermonde α).det‖ ^ 2

The discriminant in root-enumeration form: ‖disc f‖ = ‖lc‖^{2n-2} · ‖det V‖².

theorem HexPolyZTheory.one_le_mahlerDist_of_separable (p : Polynomial ℤ) (hsep : (Polynomial.map (Int.castRingHom ℚ) p).Separable) {z₁ z₂ : ℂ} (hr₁ : (Polynomial.map (Int.castRingHom ℂ) p).IsRoot z₁) (hr₂ : (Polynomial.map (Int.castRingHom ℂ) p).IsRoot z₂) (hne : z₁ ≠ z₂) : 1 ≤ √↑p.natDegree ^ (p.natDegree + 2) * (Polynomial.map (Int.castRingHom ℂ) p).mahlerMeasure ^ (p.natDegree - 1) * ‖z₁ - z₂‖

The exponent-independent assembly of Mahler's root-separation argument. For two distinct roots of a separable integral polynomial, the product of their distance with the Hadamard degree factor and the appropriate power of the Mahler measure is at least one. Executable precision specializations need only bound the final two factors.

theorem HexPolyZTheory.one_le_mahlerDist (p : Polynomial ℤ) (hp : p ≠ 0) {z₁ z₂ : ℂ} (hr₁ : (Polynomial.map (Int.castRingHom ℂ) p).IsRoot z₁) (hr₂ : (Polynomial.map (Int.castRingHom ℂ) p).IsRoot z₂) (hne : z₁ ≠ z₂) : 1 ≤ √↑p.natDegree ^ (p.natDegree + 2) * (Polynomial.map (Int.castRingHom ℂ) p).mahlerMeasure ^ (p.natDegree - 1) * ‖z₁ - z₂‖

Mahler separation for arbitrary nonzero integral polynomials. Repeated factors do not affect the set of roots: applying the separable theorem to the integral radical gives the same two roots, no larger degree, and no larger Mahler measure.