theorem HexRootsTheory.NKData.exactCoeffNorm_eq (p : Hex.ZPoly) (s : Hex.DyadicSquare) (k : ℕ) : exactCoeffNorm (toPolyℂ p) k (centerSup s) = ‖NewtonKantorovich.ComplexSup.mul ((((toPolyℂ p).comp (Polynomial.X + Polynomial.C (DyadicSquare.center s))).coeff 1)⁻¹ * ((toPolyℂ p).comp (Polynomial.X + Polynomial.C (DyadicSquare.center s))).coeff k)‖

The exact-centre coefficient norm is the sup-operator norm of the ratio of the corresponding Taylor coefficient to the linear coefficient.

theorem HexRootsTheory.NKData.translated_eq_factor {p : Polynomial ℂ} {c z : ℂ} {roots : Multiset ℂ} (hp : p ≠ 0) (hroots : p.roots = z ::ₘ roots) (hremote : ∀ w ∈ roots, w ≠ c) : ∃ (K : ℂ), K ≠ 0 ∧ p.comp (Polynomial.X + Polynomial.C c) = Polynomial.C K * ((Polynomial.X - Polynomial.C (z - c)) * remotePoly (Multiset.map Inv.inv (Multiset.map (fun (w : ℂ) => w - c) roots)))

A translated polynomial with one designated root is a nonzero scalar times its near-root linear factor and the normalized remote-root product.

theorem HexRootsTheory.NKData.weighted_coeff_le {g : Polynomial ℂ} {a : ℂ} {n : ℕ} {rho E : ℝ} (hrho : 0 < rho) (hdeg : g.natDegree < n) (htail : ∑ j ∈ (Finset.range n).erase 0, ‖g.coeff j‖ * (4 * rho) ^ j ≤ E) (ha : ‖a‖ ≤ rho / 2) : (∑ k ∈ Finset.range (n + 1), if 2 ≤ k then ↑k * ‖((Polynomial.X - Polynomial.C a) * g).coeff k‖ * rho ^ (k - 2) else 0) ≤ 9 / (16 * rho) * E

The weighted higher-coefficient mass of a near-root linear factor times a normalized remote product is controlled by the remote product's ordinary coefficient tail at four times the working radius.

theorem HexRootsTheory.NKData.exactCoeffNorm_factor {p : Hex.ZPoly} {s : Hex.DyadicSquare} {K : ℂ} {h : Polynomial ℂ} (hK : K ≠ 0) (hfactor : (toPolyℂ p).comp (Polynomial.X + Polynomial.C (DyadicSquare.center s)) = Polynomial.C K * h) (hlinear : h.coeff 1 ≠ 0) (k : ℕ) : exactCoeffNorm (toPolyℂ p) k (centerSup s) ≤ √2 * (‖h.coeff k‖ / ‖h.coeff 1‖)

A nonzero scalar factor cancels from every exact inverse-normalized Taylor coefficient.

theorem HexRootsTheory.NKData.supNorm_inverse_mul_le {a e : ℂ} {r rho : ℝ} (hr : 0 < r) (hrho : 0 < rho) (hrho' : rho ≤ 3 * r / 2) (haSup : supNorm a ≤ r / 2) (ha : ‖a‖ ≤ rho / 2) (he : ‖e‖ ≤ 1 / 256) : supNorm ((1 - e)⁻¹ * -a) ≤ 9 / 14 * r

A small multiplicative perturbation of the exact near-root correction keeps its sup norm well inside the executable residual margin.

theorem HexRootsTheory.NKData.witness_of_remote_roots {p : Hex.ZPoly} {s : Hex.DyadicSquare} {z : ℂ} {roots : Multiset ℂ} {d : ℝ} (hp : toPolyℂ p ≠ 0) (hsize : 1 < Hex.DensePoly.size p) (hroots : (toPolyℂ p).roots = z ::ₘ roots) (hd : 0 < d) (hremote : ∀ w ∈ roots, d ≤ ‖w - DyadicSquare.center s‖) (hcenter : supNorm (z - DyadicSquare.center s) ≤ DyadicSquare.halfWidth s / 2) (htailSmall : (1 + 4 * Dyadic.toReal s.radiusHi / d) ^ roots.card - 1 ≤ 1 / 32) : Hex.nkWitness p s

A simple root with a small normalized remote-root tail makes the actual dyadic Newton--Kantorovich witness succeed. The centre hypothesis is in the sup norm, matching the doubled enclosing-square geometry.