theorem HexRootsMathlib.NKData.one_add_pow_le {x : ℝ} (hx : 0 ≤ x) (n : ℕ) (hsmall : ↑n * x ≤ 1 / 2) : (1 + x) ^ n ≤ 1 + 2 * ↑n * x

A convenient elementary upper bound for a small binomial tail.

theorem HexRootsMathlib.NKData.one_add_pow_sub_one_le {x : ℝ} {n : ℕ} (hx : 0 ≤ x) (hsmall : ↑n * x ≤ 1 / 96) : (1 + x) ^ n - 1 ≤ 1 / 32

The numerical tail threshold used by witness_of_remote_roots.

theorem HexRootsMathlib.NKData.radiusHi_mul_degree_le {p : Hex.ZPoly} {s : Hex.DyadicSquare} (hprec : ↑(Hex.separationDepth p) ≤ s.prec) : Dyadic.toReal s.radiusHi * ↑(Nat.max 2 (Hex.DensePoly.natDegree p)) ≤ 2 ^ (-↑(Hex.mahlerPrec p)) * (1449 / 1024) / 256

At separationDepth, the executable upper radius times the degree is at most one 256th of the Mahler-radius scale.

theorem HexRootsMathlib.NKData.witness_of_simple {p : Hex.ZPoly} {s : Hex.DyadicSquare} {z : ℂ} (hsize : 1 < Hex.DensePoly.size p) (hp : p ≠ 0) (hz : (toPolyℂ p).IsRoot z) (hsimple : Polynomial.eval z (Polynomial.derivative (toPolyℂ p)) ≠ 0) (hprec : ↑(Hex.separationDepth p) ≤ s.prec) (hcenter : supNorm (z - DyadicSquare.center s) ≤ DyadicSquare.halfWidth s / 2) : Hex.nkWitness p s

A simple root lying in the central half of a square at the executable separation depth satisfies the actual Newton--Kantorovich witness. Other roots of the polynomial may have multiplicity.

theorem HexRootsMathlib.NKData.witness_at_separationDepth {p : Hex.ZPoly} {s : Hex.DyadicSquare} {z : ℂ} (hsize : 1 < Hex.DensePoly.size p) (hsep : (HexPolyZMathlib.toPolyℚ p).Separable) (hz : (toPolyℂ p).IsRoot z) (hprec : ↑(Hex.separationDepth p) ≤ s.prec) (hcenter : supNorm (z - DyadicSquare.center s) ≤ DyadicSquare.halfWidth s / 2) : Hex.nkWitness p s

Global separability is a convenient sufficient condition for the local simple-root premise.

theorem HexRootsMathlib.NKData.certify_nk_exists_of_witness {p : Hex.ZPoly} {c : Hex.Component} (hbase : Hex.nkWitness p (Hex.encSquare c.squares).doubled) : ∃ (r : Hex.Certified p), Hex.Component.certify? p Hex.AtomStrategy.nk c = some r

Once the doubled enclosing square has an NK witness, the executable NK-only certifier returns either its guarded speculative candidate or the base atom.

theorem HexRootsMathlib.NKData.certify_mixed_exists_of_witness {p : Hex.ZPoly} {c : Hex.Component} (hbase : Hex.nkWitness p (Hex.encSquare c.squares).doubled) : ∃ (r : Hex.Certified p), Hex.Component.certify? p Hex.AtomStrategy.nkThenPellet c = some r

The mixed certifier has the same successful NK prefix as the NK-only certifier. Pellet is not reached when the doubled enclosing square already has an NK witness.

theorem HexRootsMathlib.NKData.component_certify_nk {p : Hex.ZPoly} {c : Hex.Component} {z : ℂ} (hsize : 1 < Hex.DensePoly.size p) (hsep : (HexPolyZMathlib.toPolyℚ p).Separable) (hz : (toPolyℂ p).IsRoot z) (hzc : z ∈ Component.region c) (hprec : ↑(Hex.separationDepth p) ≤ (Hex.encSquare c.squares).doubled.prec) : ∃ (r : Hex.Certified p), Hex.Component.certify? p Hex.AtomStrategy.nk c = some r

A component root in the central half of its doubled enclosing square forces the actual .nk certification path at separationDepth. The depth hypothesis is deliberately on that enclosing square: deriving it from the component's leaf precision requires the separate gluing-width invariant.

theorem HexRootsMathlib.NKData.component_certify_nk_covers {p : Hex.ZPoly} {c : Hex.Component} {z : ℂ} (hsize : 1 < Hex.DensePoly.size p) (hsep : (HexPolyZMathlib.toPolyℚ p).Separable) (hz : (toPolyℂ p).IsRoot z) (hzc : z ∈ Component.region c) (hprec : ↑(Hex.separationDepth p) ≤ (Hex.encSquare c.squares).doubled.prec) : ∃ (r : Hex.Certified p), Hex.Component.certify? p Hex.AtomStrategy.nk c = some r ∧ z ∈ Certified.region r

The successful fixed-depth NK certificate continues to cover the designated component root, including through speculative recentring.

theorem HexRootsMathlib.NKData.component_certify_mixed_covers {p : Hex.ZPoly} {c : Hex.Component} {z : ℂ} (hsize : 1 < Hex.DensePoly.size p) (hsep : (HexPolyZMathlib.toPolyℚ p).Separable) (hz : (toPolyℂ p).IsRoot z) (hzc : z ∈ Component.region c) (hprec : ↑(Hex.separationDepth p) ≤ (Hex.encSquare c.squares).doubled.prec) : ∃ (r : Hex.Certified p), Hex.Component.certify? p Hex.AtomStrategy.nkThenPellet c = some r ∧ z ∈ Certified.region r

The mixed NK-then-Pellet certifier succeeds at the same fixed depth and continues to cover the designated component root.