noncomputable def HexRootsMathlib.RefinedIsolation.root {p : Hex.ZPoly} (i : Hex.RefinedIsolation p) : ℂ

The unique root in a refined isolation's selected certified region.

Equations

• HexRootsMathlib.RefinedIsolation.root i = ⋯.choose

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

The selected root is a simple polynomial root, interior to the selected region and unique in its closed counterpart.

theorem HexRootsMathlib.RefinedIsolation.isRoot {p : Hex.ZPoly} (i : Hex.RefinedIsolation p) : (toPolyℂ p).IsRoot (root i)

The selected value is a root.

theorem HexRootsMathlib.RefinedIsolation.poly_ne_zero {p : Hex.ZPoly} (i : Hex.RefinedIsolation p) : p ≠ 0

A polynomial carrying a refined isolation is nonzero.

theorem HexRootsMathlib.RefinedIsolation.root_mem_region {p : Hex.ZPoly} (i : Hex.RefinedIsolation p) : root i ∈ DyadicRootIsolation.region ↑i

The semantic root lies in its atom's selected closed region.

theorem HexRootsMathlib.RefinedIsolation.root_mem_closedDisc {p : Hex.ZPoly} (i : Hex.RefinedIsolation p) : root i ∈ DyadicSquare.closedDisc (↑i).square

Both atom witness forms place the semantic root in the stored square's circumscribed disc.

theorem HexRootsMathlib.RefinedIsolation.eq_root_of_mem_closedDisc {p : Hex.ZPoly} (i : Hex.RefinedIsolation p) {z : ℂ} (hzroot : (toPolyℂ p).IsRoot z) (hzmem : z ∈ DyadicSquare.closedDisc (↑i).square) : z = root i

A polynomial root in the closed circumscribed disc of a refined isolation is the isolation's selected root.

theorem HexRootsMathlib.RefinedIsolation.intersects_iff_root_eq {p : Hex.ZPoly} (i₁ i₂ : Hex.RefinedIsolation p) : Hex.Intersects i₁ i₂ ↔ root i₁ = root i₂

At separation precision, executable disc intersection is exactly semantic root equality. Only nonzeroness of the ambient polynomial is needed; each refined isolation supplies it locally.

theorem HexRootsMathlib.RefinedIsolation.intersects_equivalence {p : Hex.ZPoly} : Equivalence Hex.Intersects

Intersects is an equivalence relation on refined isolations.

noncomputable def HexRootsMathlib.SimpleRoot.rootOf {p : Hex.ZPoly} : Hex.SimpleRoot p → ℂ

Interpret a quotient root as its complex value.

Equations

• HexRootsMathlib.SimpleRoot.rootOf = Quot.lift HexRootsMathlib.RefinedIsolation.root ⋯

@[simp]

theorem HexRootsMathlib.SimpleRoot.rootOf_mk {p : Hex.ZPoly} (i : Hex.RefinedIsolation p) : rootOf (Hex.SimpleRoot.mk i) = RefinedIsolation.root i

theorem HexRootsMathlib.SimpleRoot.ofSquare_mk {p : Hex.ZPoly} (i : Hex.RefinedIsolation p) (hw : Hex.atomWitness p (↑i).square) (hp : ↑(Hex.mahlerPrec p) ≤ (↑i).square.prec) : Hex.SimpleRoot.ofSquare p (↑i).square hw hp = Hex.SimpleRoot.mk i

Rebuilding from an isolation's own square names that isolation's root. Hex.Intersects compares stored squares, so the rebuilt certificate need not match the original: any two isolations on one square are related, and Quot.sound identifies them. This is what makes the Repr output of hex-number-field a faithful round trip.

theorem HexRootsMathlib.RefinedIsolation.sameRoot_eq_true_iff {p : Hex.ZPoly} (i₁ i₂ : Hex.RefinedIsolation p) : i₁.sameRoot i₂ = true ↔ Hex.Intersects i₁ i₂

The executable Boolean test is the proposition Intersects.

theorem HexRootsMathlib.RefinedIsolation.sameRoot_iff_mk_eq {p : Hex.ZPoly} (i₁ i₂ : Hex.RefinedIsolation p) : i₁.sameRoot i₂ = true ↔ Hex.SimpleRoot.mk i₁ = Hex.SimpleRoot.mk i₂

The executable test decides equality in the quotient of refined isolations.

@[reducible, inline]

noncomputable abbrev Hex.RefinedIsolation.root {p : ZPoly} (i : RefinedIsolation p) : ℂ

Field-notation alias for the companion's semantic root.

Equations

• i.root = HexRootsMathlib.RefinedIsolation.root i

@[reducible, inline]

noncomputable abbrev Hex.rootOf {p : ZPoly} : SimpleRoot p → ℂ

Mathlib interpretation of a quotient simple root.

Equations

• Hex.rootOf = HexRootsMathlib.SimpleRoot.rootOf