def HexRootsMathlib.NKData.coeffs (p : Hex.ZPoly) (s : Hex.DyadicSquare) : Array Hex.GaussDyadic

Exact Taylor coefficients used by the executable witness.

Equations

• HexRootsMathlib.NKData.coeffs p s = (Hex.TaylorShift.compute p s.center).coeffs

@[simp]

theorem HexRootsMathlib.NKData.coeffs_eq_taylor (p : Hex.ZPoly) (s : Hex.DyadicSquare) : coeffs p s = Hex.taylor p s.center

The cached coefficient array is the exact Taylor expansion.

def HexRootsMathlib.NKData.c1 (p : Hex.ZPoly) (s : Hex.DyadicSquare) : Hex.GaussDyadic

The exact first Taylor coefficient.

Equations

• HexRootsMathlib.NKData.c1 p s = (HexRootsMathlib.NKData.coeffs p s).getD 1 (0, 0)

def HexRootsMathlib.NKData.normSq (p : Hex.ZPoly) (s : Hex.DyadicSquare) : Dyadic

Squared modulus of the first Taylor coefficient.

Equations

• HexRootsMathlib.NKData.normSq p s = (HexRootsMathlib.NKData.c1 p s).normSq

def HexRootsMathlib.NKData.invPrec (p : Hex.ZPoly) (s : Hex.DyadicSquare) : ℤ

Precision used for the executable reciprocal floor.

Equations

• HexRootsMathlib.NKData.invPrec p s = 8 + max 0 (Hex.Dyadic.ceilLog2 (HexRootsMathlib.NKData.normSq p s))

def HexRootsMathlib.NKData.inverse (p : Hex.ZPoly) (s : Hex.DyadicSquare) : Hex.GaussDyadic

Executable approximate inverse of the first Taylor coefficient.

Equations

• One or more equations did not get rendered due to their size.

def HexRootsMathlib.NKData.residual (p : Hex.ZPoly) (s : Hex.DyadicSquare) (k : ℕ) : Hex.GaussDyadic

Taylor coefficient after multiplication by the approximate inverse.

Equations

• HexRootsMathlib.NKData.residual p s k = (HexRootsMathlib.NKData.inverse p s).mul ((HexRootsMathlib.NKData.coeffs p s).getD k (0, 0))

def HexRootsMathlib.NKData.y (p : Hex.ZPoly) (s : Hex.DyadicSquare) : Dyadic

Exact sup norm of the constant Newton residual.

Equations

• HexRootsMathlib.NKData.y p s = (HexRootsMathlib.NKData.residual p s 0).lo

def HexRootsMathlib.NKData.z1 (p : Hex.ZPoly) (s : Hex.DyadicSquare) : Dyadic

Exact sup-operator norm of the first-order defect.

Equations

• HexRootsMathlib.NKData.z1 p s = Hex.Dyadic.abs (1 - (HexRootsMathlib.NKData.residual p s 1).1) + Hex.Dyadic.abs (HexRootsMathlib.NKData.residual p s 1).2

def HexRootsMathlib.NKData.z2Step (p : Hex.ZPoly) (s : Hex.DyadicSquare) (acc : Dyadic × Dyadic) (i : ℕ) : Dyadic × Dyadic

One step of the running-power fold used by the executable radial bound.

Equations

• HexRootsMathlib.NKData.z2Step p s acc i = if 2 ≤ i then (acc.1 + Dyadic.ofInt ↑i * (HexRootsMathlib.NKData.residual p s i).hi * acc.2, acc.2 * s.radiusHi) else acc

def HexRootsMathlib.NKData.z2Sum (p : Hex.ZPoly) (s : Hex.DyadicSquare) : Dyadic

Running-power fold used by the executable radial derivative bound.

Equations

• HexRootsMathlib.NKData.z2Sum p s = (List.foldl (HexRootsMathlib.NKData.z2Step p s) (0, 1) (List.range (HexRootsMathlib.NKData.coeffs p s).size)).1

def HexRootsMathlib.NKData.z2 (p : Hex.ZPoly) (s : Hex.DyadicSquare) : Dyadic

Executable radial derivative-Lipschitz bound.

Equations

• HexRootsMathlib.NKData.z2 p s = 2 * HexRootsMathlib.NKData.z2Sum p s

def HexRootsMathlib.NKData.radius (s : Hex.DyadicSquare) : Dyadic

Sup radius of the certified square.

Equations

• HexRootsMathlib.NKData.radius s = Dyadic.ofIntWithPrec 1 s.prec

def HexRootsMathlib.NKData.halfRadiusSq (s : Hex.DyadicSquare) : Dyadic

Exact representation of half the squared sup radius.

Equations

• HexRootsMathlib.NKData.halfRadiusSq s = Dyadic.ofIntWithPrec 1 (2 * s.prec + 1)

theorem HexRootsMathlib.NKData.witness_iff (p : Hex.ZPoly) (s : Hex.DyadicSquare) : Hex.nkWitness p s ↔ 2 ≤ (coeffs p s).size ∧ 0 < normSq p s ∧ y p s + z1 p s * radius s + z2 p s * halfRadiusSq s < radius s ∧ z1 p s + z2 p s * radius s < 1

Decode the Boolean witness into its three strict exact inequalities.

theorem HexRootsMathlib.NKData.toReal_fold_z2 (p : Hex.ZPoly) (s : Hex.DyadicSquare) (n : ℕ) : (Dyadic.toReal (List.foldl (z2Step p s) (0, 1) (List.range n)).1 = ∑ i ∈ Finset.range n, if 2 ≤ i then ↑i * Dyadic.toReal (residual p s i).hi * Dyadic.toReal s.radiusHi ^ (i - 2) else 0) ∧ Dyadic.toReal (List.foldl (z2Step p s) (0, 1) (List.range n)).2 = Dyadic.toReal s.radiusHi ^ (n - 2)

Casting the fold accumulator gives its mathematical partial sum and the next real power of the radial bound.

theorem HexRootsMathlib.NKData.toReal_z2Sum (p : Hex.ZPoly) (s : Hex.DyadicSquare) : Dyadic.toReal (z2Sum p s) = ∑ i ∈ Finset.range (coeffs p s).size, if 2 ≤ i then ↑i * Dyadic.toReal (residual p s i).hi * Dyadic.toReal s.radiusHi ^ (i - 2) else 0

Real closed form of the executable running-power sum.

@[simp]

theorem HexRootsMathlib.NKData.coeffs_size (p : Hex.ZPoly) (s : Hex.DyadicSquare) : (coeffs p s).size = Hex.DensePoly.size p

theorem HexRootsMathlib.NKData.coeff_zero (p : Hex.ZPoly) (s : Hex.DyadicSquare) : GaussDyadic.toComplex ((coeffs p s).getD 0 (0, 0)) = Polynomial.eval (DyadicSquare.center s) (toPolyℂ p)

The zeroth executable Taylor coefficient is evaluation at the centre.

theorem HexRootsMathlib.NKData.coeff_one (p : Hex.ZPoly) (s : Hex.DyadicSquare) : GaussDyadic.toComplex (c1 p s) = Polynomial.eval (DyadicSquare.center s) (Polynomial.derivative (toPolyℂ p))

The first executable Taylor coefficient is derivative evaluation at the centre.

theorem HexRootsMathlib.NKData.toComplex_residual (p : Hex.ZPoly) (s : Hex.DyadicSquare) (k : ℕ) : GaussDyadic.toComplex (residual p s k) = GaussDyadic.toComplex (inverse p s) * ((toPolyℂ p).comp (Polynomial.X + Polynomial.C (DyadicSquare.center s))).coeff k

Casting a residual gives multiplication of the approximate inverse by the corresponding exact Taylor coefficient.

@[simp]

theorem HexRootsMathlib.NKData.toReal_radius (s : Hex.DyadicSquare) : Dyadic.toReal (radius s) = DyadicSquare.halfWidth s

noncomputable def HexRootsMathlib.NKData.centerSup (s : Hex.DyadicSquare) : NewtonKantorovich.ComplexSup

The sup-norm centre corresponding to the executable square centre.

Equations

• HexRootsMathlib.NKData.centerSup s = NewtonKantorovich.ComplexSup.equiv (HexRootsMathlib.DyadicSquare.center s)

def HexRootsMathlib.NKData.inverseComplex (p : Hex.ZPoly) (s : Hex.DyadicSquare) : ℂ

Complex scalar used as the executable approximate inverse.

Equations

• HexRootsMathlib.NKData.inverseComplex p s = HexRootsMathlib.GaussDyadic.toComplex (HexRootsMathlib.NKData.inverse p s)

noncomputable def HexRootsMathlib.NKData.approxInverse (p : Hex.ZPoly) (s : Hex.DyadicSquare) : NewtonKantorovich.ComplexSup →L[ℝ] NewtonKantorovich.ComplexSup

Approximate inverse as a real-linear operator in sup coordinates.

Equations

• HexRootsMathlib.NKData.approxInverse p s = NewtonKantorovich.ComplexSup.mul (HexRootsMathlib.NKData.inverseComplex p s)

theorem HexRootsMathlib.NKData.eval_center (p : Hex.ZPoly) (s : Hex.DyadicSquare) : NewtonKantorovich.ComplexSup.eval (toPolyℂ p) (centerSup s) = NewtonKantorovich.ComplexSup.equiv (GaussDyadic.toComplex ((coeffs p s).getD 0 (0, 0)))

Evaluation at the centre is the zeroth executable Taylor coefficient.

theorem HexRootsMathlib.NKData.apply_residual (p : Hex.ZPoly) (s : Hex.DyadicSquare) (k : ℕ) : (NewtonKantorovich.ComplexSup.mul (inverseComplex p s)) (NewtonKantorovich.ComplexSup.equiv (GaussDyadic.toComplex ((coeffs p s).getD k (0, 0)))) = NewtonKantorovich.ComplexSup.equiv (GaussDyadic.toComplex (residual p s k))

Multiplying an executable Taylor coefficient by the approximate inverse gives the executable residual.

theorem HexRootsMathlib.NKData.norm_residual (p : Hex.ZPoly) (s : Hex.DyadicSquare) : ‖(approxInverse p s) (NewtonKantorovich.ComplexSup.eval (toPolyℂ p) (centerSup s))‖ = Dyadic.toReal (y p s)

The first Newton quantity is exact: no Euclidean norm conversion enters.

theorem HexRootsMathlib.NKData.comp_deriv_center (p : Hex.ZPoly) (s : Hex.DyadicSquare) : approxInverse p s ∘SL NewtonKantorovich.ComplexSup.evalDeriv (toPolyℂ p) (centerSup s) = NewtonKantorovich.ComplexSup.mul (GaussDyadic.toComplex (residual p s 1))

The approximate inverse composed with the frozen centre derivative is multiplication by the first executable residual.

theorem HexRootsMathlib.NKData.norm_defect (p : Hex.ZPoly) (s : Hex.DyadicSquare) : ‖1 - approxInverse p s ∘SL NewtonKantorovich.ComplexSup.evalDeriv (toPolyℂ p) (centerSup s)‖ = Dyadic.toReal (z1 p s)

The first-order defect bound is the exact sup operator norm.

theorem HexRootsMathlib.NKData.natDegree_lt_size (p : Hex.ZPoly) (hp : 0 < Hex.DensePoly.size p) : (toPolyℂ p).natDegree < Hex.DensePoly.size p

A nonempty executable polynomial has complex degree below its stored coefficient count.

noncomputable def HexRootsMathlib.NKData.shifted (p : Hex.ZPoly) (s : Hex.DyadicSquare) : Polynomial ℂ

The exact Taylor shift at the square centre.

Equations

• HexRootsMathlib.NKData.shifted p s = (Polynomial.taylor (HexRootsMathlib.DyadicSquare.center s)) (HexRootsMathlib.toPolyℂ p)

theorem HexRootsMathlib.NKData.shifted_coeff (p : Hex.ZPoly) (s : Hex.DyadicSquare) (k : ℕ) : (shifted p s).coeff k = GaussDyadic.toComplex ((coeffs p s).getD k (0, 0))

Coefficients of the recentred polynomial are the executable Taylor coefficients.

theorem HexRootsMathlib.NKData.shifted_deriv (p : Hex.ZPoly) (s : Hex.DyadicSquare) (δ : ℂ) : Polynomial.eval δ (Polynomial.derivative (shifted p s)) = Polynomial.eval (DyadicSquare.center s + δ) (Polynomial.derivative (toPolyℂ p))

The recentred derivative evaluates the original derivative at the translated point.

theorem HexRootsMathlib.NKData.deriv_sub_center (p : Hex.ZPoly) (s : Hex.DyadicSquare) (hsize : 2 ≤ (coeffs p s).size) (δ : ℂ) : Polynomial.eval (DyadicSquare.center s + δ) (Polynomial.derivative (toPolyℂ p)) - Polynomial.eval (DyadicSquare.center s) (Polynomial.derivative (toPolyℂ p)) = ∑ k ∈ Finset.range (coeffs p s).size, if 2 ≤ k then ↑k * GaussDyadic.toComplex ((coeffs p s).getD k (0, 0)) * δ ^ (k - 1) else 0

Radial Taylor identity for the derivative difference. The index is k, not the mean-value overestimate k * (k - 1).

theorem HexRootsMathlib.NKData.inverse_deriv_sub (p : Hex.ZPoly) (s : Hex.DyadicSquare) (hsize : 2 ≤ (coeffs p s).size) (δ : ℂ) : inverseComplex p s * (Polynomial.eval (DyadicSquare.center s + δ) (Polynomial.derivative (toPolyℂ p)) - Polynomial.eval (DyadicSquare.center s) (Polynomial.derivative (toPolyℂ p))) = ∑ k ∈ Finset.range (coeffs p s).size, if 2 ≤ k then ↑k * GaussDyadic.toComplex (residual p s k) * δ ^ (k - 1) else 0

The derivative difference after applying the executable approximate inverse, still as an exact finite Taylor sum.

theorem HexRootsMathlib.NKData.norm_term_le (d : Hex.GaussDyadic) (δ : ℂ) (k : ℕ) (hk : 2 ≤ k) {ρ t : ℝ} (hρ : ‖δ‖ ≤ ρ) (ht : ‖δ‖ ≤ √2 * t) : ‖NewtonKantorovich.ComplexSup.mul (↑k * GaussDyadic.toComplex d * δ ^ (k - 1))‖ ≤ 2 * (↑k * Dyadic.toReal d.hi * ρ ^ (k - 2)) * t

One radial Taylor term has the executable bound. There is one √2 from the scalar operator norm and one from complex modulus versus sup norm; they combine to the factor 2.

noncomputable def HexRootsMathlib.NKData.delta (s : Hex.DyadicSquare) (x : NewtonKantorovich.ComplexSup) : ℂ

Complex displacement from the executable square centre.

Equations

• HexRootsMathlib.NKData.delta s x = NewtonKantorovich.ComplexSup.equiv.symm x - HexRootsMathlib.DyadicSquare.center s

@[simp]

theorem HexRootsMathlib.NKData.equiv_delta (s : Hex.DyadicSquare) (x : NewtonKantorovich.ComplexSup) : NewtonKantorovich.ComplexSup.equiv (delta s x) = x - centerSup s

theorem HexRootsMathlib.NKData.norm_delta_le (s : Hex.DyadicSquare) (x : NewtonKantorovich.ComplexSup) : ‖delta s x‖ ≤ √2 * ‖x - centerSup s‖

The complex displacement is at most √2 times the sup-norm displacement from the centre.

theorem HexRootsMathlib.NKData.norm_delta_le_radiusHi (s : Hex.DyadicSquare) (x : NewtonKantorovich.ComplexSup) (hx : ‖x - centerSup s‖ ≤ DyadicSquare.halfWidth s) : ‖delta s x‖ ≤ Dyadic.toReal s.radiusHi

Inside the half-width sup ball, the complex displacement stays below the executable upper radius bound.

theorem HexRootsMathlib.NKData.comp_deriv_sub_eq_sum (p : Hex.ZPoly) (s : Hex.DyadicSquare) (hsize : 2 ≤ (coeffs p s).size) (x : NewtonKantorovich.ComplexSup) : approxInverse p s ∘SL (NewtonKantorovich.ComplexSup.evalDeriv (toPolyℂ p) x - NewtonKantorovich.ComplexSup.evalDeriv (toPolyℂ p) (centerSup s)) = ∑ k ∈ Finset.range (coeffs p s).size, if 2 ≤ k then NewtonKantorovich.ComplexSup.mul (↑k * GaussDyadic.toComplex (residual p s k) * delta s x ^ (k - 1)) else 0

Applying the approximate inverse to the derivative difference gives the finite sum whose terms are bounded by z2.

theorem HexRootsMathlib.NKData.deriv_lipschitz (p : Hex.ZPoly) (s : Hex.DyadicSquare) (hsize : 2 ≤ (coeffs p s).size) (x : NewtonKantorovich.ComplexSup) (hx : ‖x - centerSup s‖ ≤ DyadicSquare.halfWidth s) : ‖approxInverse p s ∘SL (NewtonKantorovich.ComplexSup.evalDeriv (toPolyℂ p) x - NewtonKantorovich.ComplexSup.evalDeriv (toPolyℂ p) (centerSup s))‖ ≤ Dyadic.toReal (z2 p s) * ‖x - centerSup s‖

The executable z2 is a radial Lipschitz bound for the transported polynomial derivative on the certified sup ball.

@[simp]

theorem HexRootsMathlib.NKData.toReal_halfRadiusSq (s : Hex.DyadicSquare) : Dyadic.toReal (halfRadiusSq s) = DyadicSquare.halfWidth s ^ 2 / 2

theorem HexRootsMathlib.NKData.toReal_z2_nonneg (p : Hex.ZPoly) (s : Hex.DyadicSquare) : 0 ≤ Dyadic.toReal (z2 p s)

The executable Lipschitz bound z2 is nonnegative.

def HexRootsMathlib.NKData.yNN (p : Hex.ZPoly) (s : Hex.DyadicSquare) : NNReal

Nonnegative Newton quantities in the format consumed by the generic theorem.

Equations

• HexRootsMathlib.NKData.yNN p s = ⟨HexRootsMathlib.Dyadic.toReal (HexRootsMathlib.NKData.y p s), ⋯⟩

def HexRootsMathlib.NKData.z1NN (p : Hex.ZPoly) (s : Hex.DyadicSquare) : NNReal

The executable derivative-defect bound z1 as a nonnegative real.

Equations

• HexRootsMathlib.NKData.z1NN p s = ⟨HexRootsMathlib.Dyadic.toReal (HexRootsMathlib.NKData.z1 p s), ⋯⟩

def HexRootsMathlib.NKData.z2NN (p : Hex.ZPoly) (s : Hex.DyadicSquare) : NNReal

The executable Lipschitz bound z2 as a nonnegative real.

Equations

• HexRootsMathlib.NKData.z2NN p s = ⟨HexRootsMathlib.Dyadic.toReal (HexRootsMathlib.NKData.z2 p s), ⋯⟩

def HexRootsMathlib.NKData.radiusNN (s : Hex.DyadicSquare) : NNReal

The square's half-width as a nonnegative real.

Equations

• HexRootsMathlib.NKData.radiusNN s = ⟨HexRootsMathlib.DyadicSquare.halfWidth s, ⋯⟩

theorem HexRootsMathlib.NKData.witness_inequalities {p : Hex.ZPoly} {s : Hex.DyadicSquare} (h : Hex.nkWitness p s) : yNN p s + z1NN p s * radiusNN s + z2NN p s * radiusNN s ^ 2 / 2 < radiusNN s ∧ z1NN p s + z2NN p s * radiusNN s < 1

The strict radius and contraction inequalities encoded by the executable witness.

theorem HexRootsMathlib.NKData.existsUnique_root_sup {p : Hex.ZPoly} {s : Hex.DyadicSquare} (h : Hex.nkWitness p s) : ∃! x : NewtonKantorovich.ComplexSup, Polynomial.eval (NewtonKantorovich.ComplexSup.equiv.symm x) (toPolyℂ p) = 0 ∧ ‖x - centerSup s‖₊ ≤ radiusNN s

The generic Newton--Kantorovich theorem applied to the exact executable quantities, before transporting the result back from sup coordinates.

theorem HexRootsMathlib.NKData.mem_closedSquare_iff (s : Hex.DyadicSquare) (z : ℂ) : z ∈ DyadicSquare.closedSquare s ↔ ‖NewtonKantorovich.ComplexSup.equiv z - centerSup s‖ ≤ DyadicSquare.halfWidth s

Closed-square membership is the sup-norm closed-ball inequality in the two-coordinate model.

theorem HexRootsMathlib.NKData.mem_openSquare_iff (s : Hex.DyadicSquare) (z : ℂ) : z ∈ DyadicSquare.openSquare s ↔ ‖NewtonKantorovich.ComplexSup.equiv z - centerSup s‖ < DyadicSquare.halfWidth s

Open-square membership is the strict sup-norm ball inequality in the two-coordinate model.

theorem HexRootsMathlib.NKData.existsUnique_root {p : Hex.ZPoly} {s : Hex.DyadicSquare} (h : Hex.nkWitness p s) : ∃! z : ℂ, Polynomial.eval z (toPolyℂ p) = 0 ∧ z ∈ DyadicSquare.closedSquare s

An executable Newton witness certifies exactly one root in the closed dyadic square.

theorem HexRootsMathlib.NKData.defect_lt_one {p : Hex.ZPoly} {s : Hex.DyadicSquare} (h : Hex.nkWitness p s) (z : ℂ) (hz : z ∈ DyadicSquare.closedSquare s) : ‖1 - approxInverse p s ∘SL NewtonKantorovich.ComplexSup.evalDeriv (toPolyℂ p) (NewtonKantorovich.ComplexSup.equiv z)‖ < 1

Throughout the certified square, the approximate-inverse derivative defect has norm strictly below one.

theorem HexRootsMathlib.NKData.derivative_ne_zero {p : Hex.ZPoly} {s : Hex.DyadicSquare} (h : Hex.nkWitness p s) {z : ℂ} (hz : z ∈ DyadicSquare.closedSquare s) : Polynomial.eval z (Polynomial.derivative (toPolyℂ p)) ≠ 0

Every root in a Newton-certified square is simple.

theorem HexRootsMathlib.NKData.root_mem_openSquare {p : Hex.ZPoly} {s : Hex.DyadicSquare} (h : Hex.nkWitness p s) {z : ℂ} (hzroot : Polynomial.eval z (toPolyℂ p) = 0) (hz : z ∈ DyadicSquare.closedSquare s) : z ∈ DyadicSquare.openSquare s

The strict radius check places every root in the certified closed square strictly inside that square.

theorem HexRootsMathlib.NKData.sound {p : Hex.ZPoly} {s : Hex.DyadicSquare} (h : Hex.nkWitness p s) : ∃ (z : ℂ), Polynomial.eval z (toPolyℂ p) = 0 ∧ z ∈ DyadicSquare.openSquare s ∧ Polynomial.eval z (Polynomial.derivative (toPolyℂ p)) ≠ 0 ∧ ∀ (w : ℂ), Polynomial.eval w (toPolyℂ p) = 0 → w ∈ DyadicSquare.closedSquare s → w = z

Combined semantic contract of an executable Newton witness.