noncomputable def HexRootsTheory.DyadicRootIsolation.root {p : Hex.ZPoly} (iso : Hex.DyadicRootIsolation p) : ℂ

The unique complex root selected by an atom certificate.

Equations

• HexRootsTheory.DyadicRootIsolation.root iso = ⋯.choose

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

The selected value is an interior simple root, unique in the atom's selected closed region.

theorem HexRootsTheory.DyadicRootIsolation.isRoot {p : Hex.ZPoly} (iso : Hex.DyadicRootIsolation p) : (toPolyℂ p).IsRoot (root iso)

The selected value is a root.

theorem HexRootsTheory.DyadicRootIsolation.root_mem_closedDisc {p : Hex.ZPoly} (iso : Hex.DyadicRootIsolation p) : root iso ∈ DyadicSquare.closedDisc iso.square

The selected root lies in the atom's stored circumscribed disc.

theorem HexRootsTheory.DyadicRootIsolation.root_refined {p : Hex.ZPoly} (iso : Hex.DyadicRootIsolation p) (h : ↑(Hex.mahlerPrec p) ≤ iso.square.prec) : root iso = RefinedIsolation.root ⟨iso, h⟩

The raw and separation-refined semantic-root interpretations agree.

theorem HexRootsTheory.array_mapM_isSome {α : Type u_1} {β : Type u_2} {f : α → Option β} {xs : Array α} (h : ∀ x ∈ xs.toList, (f x).isSome = true) : (Array.mapM f xs).isSome = true

An option-valued array map succeeds when its function succeeds on every input entry. Public because HexNumberFieldTheory uses it to discharge success of the embedding and refinement mapM pipelines.

theorem HexRootsTheory.isolateComplexRoots?_run (p : Hex.ZPoly) (h : Hex.HasOnlySimpleRoots p) (atomPrec : ℤ) (strategy : Hex.AtomStrategy) (hdegree : 0 < Hex.DensePoly.natDegree p) {atoms : Array (Hex.DyadicRootIsolation p)} (hrun : p.isolateComplexRoots? h atomPrec strategy = some atoms) : ∃ (rs : Array (Hex.Certified p)), Hex.isolateAll? p (max atomPrec ↑(Hex.separationDepth p)) #[Hex.Component.cauchy p hdegree] strategy = some rs ∧ rs.size = atoms.size ∧ ∀ (i : ℕ) (hi : i < rs.size) (hj : i < atoms.size), rs[i] = Hex.Certified.atom atoms[i]

In the positive-degree branch, successful isolation is a successful Cauchy-started general driver run whose results correspond indexwise to the returned atoms.

theorem HexRootsTheory.isolateComplexRoots?_root_mem_of_pos (p : Hex.ZPoly) (h : Hex.HasOnlySimpleRoots p) (atomPrec : ℤ) (strategy : Hex.AtomStrategy) (hdegree : 0 < Hex.DensePoly.natDegree p) {atoms : Array (Hex.DyadicRootIsolation p)} (hrun : p.isolateComplexRoots? h atomPrec strategy = some atoms) {z : ℂ} (hzroot : (toPolyℂ p).IsRoot z) : ∃ iso ∈ atoms.toList, DyadicRootIsolation.root iso = z

Every root belongs to one of the atoms returned by successful positive-degree isolation.

theorem HexRootsTheory.isolateComplexRoots?_nonpositive (p : Hex.ZPoly) (h : Hex.HasOnlySimpleRoots p) (atomPrec : ℤ) (strategy : Hex.AtomStrategy) (hdegree : ¬0 < Hex.DensePoly.natDegree p) {atoms : Array (Hex.DyadicRootIsolation p)} (hrun : p.isolateComplexRoots? h atomPrec strategy = some atoms) : Hex.DensePoly.size p ≠ 0 ∧ atoms = #[]

A successful non-positive-degree call is the nonzero constant branch and returns no atoms, independently of strategy.

theorem HexRootsTheory.isolateComplexRoots?_prec (p : Hex.ZPoly) (h : Hex.HasOnlySimpleRoots p) (atomPrec : ℤ) (strategy : Hex.AtomStrategy) {atoms : Array (Hex.DyadicRootIsolation p)} (hrun : p.isolateComplexRoots? h atomPrec strategy = some atoms) (iso : Hex.DyadicRootIsolation p) : iso ∈ atoms.toList → max atomPrec ↑(Hex.separationDepth p) ≤ iso.square.prec

Every returned atom meets the full driver target, not only the requested atom precision.

theorem HexRootsTheory.isolateComplexRoots?_refined (p : Hex.ZPoly) (h : Hex.HasOnlySimpleRoots p) (atomPrec : ℤ) (strategy : Hex.AtomStrategy) {atoms : Array (Hex.DyadicRootIsolation p)} (hrun : p.isolateComplexRoots? h atomPrec strategy = some atoms) (iso : Hex.DyadicRootIsolation p) : iso ∈ atoms.toList → ↑(Hex.mahlerPrec p) ≤ iso.square.prec

Every successful isolation result can be wrapped as a RefinedIsolation: the driver's separation target dominates mahlerPrec.

theorem HexRootsTheory.isolateComplexRoots?_roots_ne (p : Hex.ZPoly) (h : Hex.HasOnlySimpleRoots p) (atomPrec : ℤ) (strategy : Hex.AtomStrategy) {atoms : Array (Hex.DyadicRootIsolation p)} (hrun : p.isolateComplexRoots? h atomPrec strategy = some atoms) {i j : ℕ} (hi : i < atoms.size) (hj : j < atoms.size) (hij : i ≠ j) : DyadicRootIsolation.root atoms[i] ≠ DyadicRootIsolation.root atoms[j]

Distinct output indices select distinct semantic roots.

theorem HexRootsTheory.isolateComplexRoots?_disjoint (p : Hex.ZPoly) (h : Hex.HasOnlySimpleRoots p) (atomPrec : ℤ) (strategy : Hex.AtomStrategy) {atoms : Array (Hex.DyadicRootIsolation p)} (hrun : p.isolateComplexRoots? h atomPrec strategy = some atoms) {i j : ℕ} (hi : i < atoms.size) (hj : j < atoms.size) (hij : i ≠ j) : Disjoint (DyadicSquare.closedDisc atoms[i].square) (DyadicSquare.closedDisc atoms[j].square)

Distinct output atoms have disjoint closed circumscribed discs, for every strategy accepted by the general isolation driver.

theorem HexRootsTheory.isolateComplexRoots?_count (p : Hex.ZPoly) (h : Hex.HasOnlySimpleRoots p) (atomPrec : ℤ) (strategy : Hex.AtomStrategy) {atoms : Array (Hex.DyadicRootIsolation p)} (hrun : p.isolateComplexRoots? h atomPrec strategy = some atoms) : atoms.size = (toPolyℂ p).natDegree

The number of returned atoms is the polynomial's complex natural degree. Together with isolateComplexRoots?_roots_ne, this records that the exact enumeration has no duplicate representatives.

theorem HexRootsTheory.isolateComplexRoots?_sound (p : Hex.ZPoly) (h : Hex.HasOnlySimpleRoots p) (atomPrec : ℤ) (strategy : Hex.AtomStrategy) {atoms : Array (Hex.DyadicRootIsolation p)} (hrun : p.isolateComplexRoots? h atomPrec strategy = some atoms) : (List.map DyadicRootIsolation.root atoms.toList).toFinset = (toPolyℂ p).roots.toFinset ∧ ∀ iso ∈ atoms.toList, atomPrec ≤ iso.square.prec

Successful isolation enumerates exactly the distinct complex roots and meets the requested precision, for every strategy and every executable edge case.

@[reducible, inline]

noncomputable abbrev Hex.DyadicRootIsolation.root {p : ZPoly} (iso : DyadicRootIsolation p) : ℂ

Field-notation alias for an atom's semantic root.

Equations

• iso.root = HexRootsTheory.DyadicRootIsolation.root iso