theorem HexRootsMathlib.certify_nk_cases {p : Hex.ZPoly} {c : Hex.Component} {r : Hex.Certified p} (hcert : Hex.Component.certify? p Hex.AtomStrategy.nk c = some r) : have base := (Hex.encSquare c.squares).doubled; have cand := (Hex.newtonSquare p base 1).doubled; (∃ (_ : Hex.nkWitness p base) (_ : cand.squareInside base = true) (hcand : Hex.nkWitness p cand), r = Hex.Certified.atom { square := cand, witness := Hex.AtomCertificate.nk hcand }) ∨ ∃ (hbase : Hex.nkWitness p base), r = Hex.Certified.atom { square := base, witness := Hex.AtomCertificate.nk hbase }

An NK-only certification result is either the coverage-guarded speculative candidate or the doubled enclosing base square.

@[simp]

theorem HexRootsMathlib.nkAtom_region {p : Hex.ZPoly} {s : Hex.DyadicSquare} (h : Hex.nkWitness p s) : Certified.region (Hex.Certified.atom { square := s, witness := Hex.AtomCertificate.nk h }) = DyadicSquare.closedSquare s

The semantic region of an explicitly NK-certified atom is its closed square.

theorem HexRootsMathlib.nkRoot_mem_nested {p : Hex.ZPoly} {inner outer : Hex.DyadicSquare} (hinner : Hex.nkWitness p inner) (houter : Hex.nkWitness p outer) (hsubset : DyadicSquare.closedSquare inner ⊆ DyadicSquare.closedSquare outer) {z : ℂ} (hzroot : Polynomial.eval z (toPolyℂ p) = 0) (hzouter : z ∈ DyadicSquare.closedSquare outer) : z ∈ DyadicSquare.closedSquare inner

A root in an outer unique-root square belongs to a nested inner square that also has a unique root.

theorem HexRootsMathlib.certify_nk_unique {p : Hex.ZPoly} {c : Hex.Component} {r : Hex.Certified p} (hcert : Hex.Component.certify? p Hex.AtomStrategy.nk c = some r) : ∃ (iso : Hex.DyadicRootIsolation p), r = Hex.Certified.atom iso ∧ Hex.nkWitness p iso.square ∧ iso.witness.isNK = true ∧ ∃! z : ℂ, Polynomial.eval z (toPolyℂ p) = 0 ∧ z ∈ DyadicSquare.closedSquare iso.square

Every NK-only certification result is an atom carrying an executable NK witness and hence exactly one root in its stored closed square.

theorem HexRootsMathlib.certify_nk_sound {p : Hex.ZPoly} {c : Hex.Component} {r : Hex.Certified p} (hcert : Hex.Component.certify? p Hex.AtomStrategy.nk c = some r) : ∃ (iso : Hex.DyadicRootIsolation p), r = Hex.Certified.atom iso ∧ ∃ (z : ℂ), Polynomial.eval z (toPolyℂ p) = 0 ∧ z ∈ DyadicSquare.openSquare iso.square ∧ Polynomial.eval z (Polynomial.derivative (toPolyℂ p)) ≠ 0 ∧ ∀ (w : ℂ), Polynomial.eval w (toPolyℂ p) = 0 → w ∈ DyadicSquare.closedSquare iso.square → w = z

Every NK-only certification result contains a unique interior simple root in its stored square.

theorem HexRootsMathlib.certifier_preserves_nk (p : Hex.ZPoly) : Certifier.Preserves p Hex.AtomStrategy.nk

NK-only component certification preserves every input-component root, including through the speculative recentring branch.

theorem HexRootsMathlib.isolateLoop_nk_covers {p : Hex.ZPoly} {target : ℤ} {fuel : ℕ} {work : Array Hex.Component} {rs : Array (Hex.Certified p)} (hloop : Hex.isolateLoop p target Hex.AtomStrategy.nk fuel work = some rs) {z : ℂ} (hzroot : (toPolyℂ p).IsRoot z) (hz : z ∈ Worklist.region work) : z ∈ Results.region rs

Successful NK-only loop execution preserves all polynomial roots covered by its starting worklist.