theorem HexRootsMathlib.ZPoly.toPolyℂ_negRoots {p : Hex.ZPoly} (hprim : p.Primitive) : ∃ (u : ℂ), u ≠ 0 ∧ toPolyℂ p.negRoots = Polynomial.C u * (toPolyℂ p).comp (-Polynomial.X)

Reflection changes the complex polynomial only by composition with -X and a nonzero sign used to restore a positive leading coefficient.

theorem HexRootsMathlib.ZPoly.isRoot_negRoots {p : Hex.ZPoly} {z : ℂ} (hprim : p.Primitive) (hz : (toPolyℂ p).IsRoot z) : (toPolyℂ p.negRoots).IsRoot (-z)

A root reflects to a root of the normalized reflected polynomial.

theorem HexRootsMathlib.ZPoly.toPolyℂ_normalizePrimitiveSign (p : Hex.ZPoly) : ∃ (u : ℂ), u ≠ 0 ∧ toPolyℂ p.normalizePrimitiveSign = Polynomial.C u * toPolyℂ p

Leading-sign normalization changes the complex polynomial only by a nonzero scalar.

@[simp]

theorem HexRootsMathlib.DyadicSquare.center_neg (s : Hex.DyadicSquare) : center s.neg = -center s

@[simp]

theorem HexRootsMathlib.DyadicSquare.radius_neg (s : Hex.DyadicSquare) : radius s.neg = radius s

@[simp]

theorem HexRootsMathlib.DyadicSquare.openSquare_neg {s : Hex.DyadicSquare} {z : ℂ} : -z ∈ openSquare s.neg ↔ z ∈ openSquare s

@[simp]

theorem HexRootsMathlib.DyadicSquare.closedSquare_neg {s : Hex.DyadicSquare} {z : ℂ} : -z ∈ closedSquare s.neg ↔ z ∈ closedSquare s

@[simp]

theorem HexRootsMathlib.DyadicSquare.disc_neg {s : Hex.DyadicSquare} {z : ℂ} : -z ∈ disc s.neg ↔ z ∈ disc s

@[simp]

theorem HexRootsMathlib.DyadicSquare.closedDisc_neg {s : Hex.DyadicSquare} {z : ℂ} : -z ∈ closedDisc s.neg ↔ z ∈ closedDisc s

def HexRootsMathlib.DyadicRootIsolation.openRegion {p : Hex.ZPoly} (iso : Hex.DyadicRootIsolation p) : Set ℂ

The open counterpart of an atom's selected certified region.

Equations

• HexRootsMathlib.DyadicRootIsolation.openRegion iso = if iso.witness.isNK = true then HexRootsMathlib.DyadicSquare.openSquare iso.square else HexRootsMathlib.DyadicSquare.disc iso.square

theorem HexRootsMathlib.DyadicRootIsolation.openRegion_subset_region {p : Hex.ZPoly} (iso : Hex.DyadicRootIsolation p) : openRegion iso ⊆ region iso

The selected open atom region lies in its closed counterpart.

theorem HexRootsMathlib.DyadicRootIsolation.sound {p : Hex.ZPoly} (iso : Hex.DyadicRootIsolation p) : ∃ (z : ℂ), Polynomial.eval z (toPolyℂ p) = 0 ∧ z ∈ openRegion iso ∧ Polynomial.eval z (Polynomial.derivative (toPolyℂ p)) ≠ 0 ∧ ∀ (w : ℂ), Polynomial.eval w (toPolyℂ p) = 0 → w ∈ region iso → w = z

Every atom contains an interior simple root, unique in its selected closed certified region. If both witnesses hold, this follows from the NK witness because that is the executable region-selection rule.

noncomputable def HexRootsMathlib.Certified.rootsIn (q : Polynomial ℂ) (S : Set ℂ) : ℕ

Number of roots of q in an arbitrary set, counted with multiplicity.

Equations

• HexRootsMathlib.Certified.rootsIn q S = (Multiset.filter (fun (w : ℂ) => w ∈ S) q.roots).card

noncomputable def HexRootsMathlib.Certified.rootCount {p : Hex.ZPoly} (r : Hex.Certified p) : ℕ

The number of polynomial roots in a certificate's selected closed region, counted with multiplicity.

Equations

• HexRootsMathlib.Certified.rootCount r = HexRootsMathlib.Certified.rootsIn (HexRootsMathlib.toPolyℂ p) (HexRootsMathlib.Certified.region r)

def HexRootsMathlib.Certified.Sound {p : Hex.ZPoly} (r : Hex.Certified p) : Prop

Uniform semantic contract for both certificate constructors. Every certificate has its stored multiplicity count in the selected closed region; atoms additionally have an interior simple root unique there, while clusters exclude roots from their disc boundary.

Equations

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

theorem HexRootsMathlib.Certified.sound {p : Hex.ZPoly} (r : Hex.Certified p) : Sound r

Every certificate is semantically sound by construction.

theorem HexRootsMathlib.root_mem_nestedPellet {p : Hex.ZPoly} {inner outer : Hex.DyadicSquare} {k : ℕ} (hk : 0 < k) (hinner : Hex.witness p inner k) (houter : Hex.witness p outer k) (hsubset : DyadicSquare.closedDisc inner ⊆ DyadicSquare.closedDisc outer) {z : ℂ} (hzroot : Polynomial.eval z (toPolyℂ p) = 0) (hzouter : z ∈ DyadicSquare.closedDisc outer) : z ∈ DyadicSquare.closedDisc inner

Equal positive Pellet counts on nested closed discs force every root in the outer disc into the inner disc. Strict Pellet inequalities exclude both boundaries, so the open-disc counts also count roots in the closed discs.

theorem HexRootsMathlib.pelletAtom_mem_region {p : Hex.ZPoly} {s : Hex.DyadicSquare} (h : Hex.witness p s 1) {z : ℂ} (hzdisc : z ∈ DyadicSquare.closedDisc s) : z ∈ Certified.region (Hex.Certified.atom { square := s, witness := Hex.AtomCertificate.pellet h })

A root in a k = 1 Pellet disc belongs to the atom's selected semantic region even when the same square also happens to carry an NK witness (in which case DyadicRootIsolation.region selects the closed square).

theorem HexRootsMathlib.certifyPelletAtShift_preserves {p : Hex.ZPoly} {c : Hex.Component} {shift : Hex.TaylorShift p (Hex.encSquare c.squares).center} {k : ℕ} {r : Hex.Certified p} (hcert : Hex.Component.certifyPelletAtShift? p c shift k = some r) {z : ℂ} (hzroot : Polynomial.eval z (toPolyℂ p) = 0) (hz : z ∈ Component.region c) : z ∈ Certified.region r

Each cached-shift Pellet attempt preserves every polynomial root covered by the input component.

theorem HexRootsMathlib.certifyPelletExactAt_preserves {p : Hex.ZPoly} {c : Hex.Component} {shift : Hex.TaylorShift p (Hex.encSquare c.squares).center} {k : ℕ} {r : Hex.Certified p} (hcert : Hex.Component.certifyPelletExactAt? p c shift k = some r) {z : ℂ} (hzroot : Polynomial.eval z (toPolyℂ p) = 0) (hz : z ∈ Component.region c) : z ∈ Certified.region r

One exact cached-shift Pellet attempt preserves every covered root.

theorem HexRootsMathlib.certifyPelletSoft_preserves {p : Hex.ZPoly} {c : Hex.Component} {shift : Hex.TaylorShift p (Hex.encSquare c.squares).center} {ks : List ℕ} {r : Hex.Certified p} (hcert : Hex.Component.certifyPelletSoft? p c shift ks = some r) {z : ℂ} (hz : z ∈ Component.region c) : z ∈ Certified.region r

A direct soft all-count result preserves every root in the input component.

theorem HexRootsMathlib.certifyPelletAt_preserves {p : Hex.ZPoly} {c : Hex.Component} {k : ℕ} {r : Hex.Certified p} (hcert : Hex.Component.certifyPelletAt? p c k = some r) {z : ℂ} (hzroot : Polynomial.eval z (toPolyℂ p) = 0) (hz : z ∈ Component.region c) : z ∈ Certified.region r

The public one-count wrapper has the cached attempt's preservation property.

theorem HexRootsMathlib.certifyPelletExactList_preserves {p : Hex.ZPoly} {c : Hex.Component} {shift : Hex.TaylorShift p (Hex.encSquare c.squares).center} (ks : List ℕ) {r : Hex.Certified p} (hcert : Hex.Component.certifyPelletExactList? p c shift ks = some r) {z : ℂ} (hzroot : Polynomial.eval z (toPolyℂ p) = 0) (hz : z ∈ Component.region c) : z ∈ Certified.region r

Searching an exact list with one cached shift preserves every polynomial root covered by the input component.

theorem HexRootsMathlib.certifyPelletListShift_preserves {p : Hex.ZPoly} {c : Hex.Component} {shift : Hex.TaylorShift p (Hex.encSquare c.squares).center} (ks : List ℕ) {r : Hex.Certified p} (hcert : Hex.Component.certifyPelletListShift? p c shift ks = some r) {z : ℂ} (hzroot : Polynomial.eval z (toPolyℂ p) = 0) (hz : z ∈ Component.region c) : z ∈ Certified.region r

The soft-first, exact-fallback cached list search preserves every covered root.

theorem HexRootsMathlib.certifyPelletList_preserves {p : Hex.ZPoly} {c : Hex.Component} (ks : List ℕ) {r : Hex.Certified p} (hcert : Hex.Component.certifyPelletList? p c ks = some r) {z : ℂ} (hzroot : Polynomial.eval z (toPolyℂ p) = 0) (hz : z ∈ Component.region c) : z ∈ Certified.region r

The public candidate-count search inherits the cached implementation's preservation property.

theorem HexRootsMathlib.certifyPelletShift_preserves {p : Hex.ZPoly} {c : Hex.Component} {shift : Hex.TaylorShift p (Hex.encSquare c.squares).center} {r : Hex.Certified p} (hcert : Hex.Component.certifyPelletShift? p c shift = some r) {z : ℂ} (hzroot : Polynomial.eval z (toPolyℂ p) = 0) (hz : z ∈ Component.region c) : z ∈ Certified.region r

Pellet candidate search with a caller-supplied shift preserves every root covered by the input component.

theorem HexRootsMathlib.certifyPellet_preserves {p : Hex.ZPoly} {c : Hex.Component} {r : Hex.Certified p} (hcert : Hex.Component.certifyPellet? p c = some r) {z : ℂ} (hzroot : Polynomial.eval z (toPolyℂ p) = 0) (hz : z ∈ Component.region c) : z ∈ Certified.region r

The public Pellet search inherits the caller-supplied shift implementation's preservation property.

theorem HexRootsMathlib.certifier_preserves_pellet (p : Hex.ZPoly) : Certifier.Preserves p Hex.AtomStrategy.pellet

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

theorem HexRootsMathlib.certify_nkThenPellet_cases {p : Hex.ZPoly} {c : Hex.Component} {r : Hex.Certified p} (hcert : Hex.Component.certify? p Hex.AtomStrategy.nkThenPellet 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 }) ∨ ∃ (shift : Hex.TaylorShift p (Hex.encSquare { squares := #[(Hex.encSquare c.squares).doubled.doubled], candidateK := c.candidateK }.squares).center), Hex.Component.certifyPelletShift? p { squares := #[(Hex.encSquare c.squares).doubled.doubled], candidateK := c.candidateK } shift = some r

A combined-strategy result is an NK result from the common leading branch, or the result of falling through to the Pellet search.

theorem HexRootsMathlib.certifier_preserves_nkThenPellet (p : Hex.ZPoly) : Certifier.Preserves p Hex.AtomStrategy.nkThenPellet

The default combined strategy preserves every input-component root in both its NK prefix and its Pellet fallback.

theorem HexRootsMathlib.certifier_preserves (p : Hex.ZPoly) (strategy : Hex.AtomStrategy) : Certifier.Preserves p strategy

Every component certification strategy preserves each covered root.

theorem HexRootsMathlib.certify_sound {p : Hex.ZPoly} {strategy : Hex.AtomStrategy} {c : Hex.Component} {r : Hex.Certified p} (_hcert : Hex.Component.certify? p strategy c = some r) : Certified.Sound r

Every successful executable component certification satisfies the uniform certificate contract. The equality hypothesis identifies the executable result; semantic soundness itself is structural because each Certified constructor already stores its checked witness.