def Hex.RefinedIsolation (p : ZPoly) : Type

An isolation refined at least to separation precision. At this precision the disc radius is below sep(p)/4, so two refined isolations isolate the same root exactly when their discs intersect.

Equations

• Hex.RefinedIsolation p = { iso : Hex.DyadicRootIsolation p // ↑(Hex.mahlerPrec p) ≤ iso.square.prec }

def Hex.RefinedIsolation.conj {p : ZPoly} (r : RefinedIsolation p) : RefinedIsolation p

Reflect an isolation, transporting its certificate without numerical checks.

Equations

• r.conj = ⟨{ square := r.val.square.conj, witness := r.val.witness.conj }, ⋯⟩

def Hex.Intersects {p : ZPoly} (i₁ i₂ : RefinedIsolation p) : Prop

The circumscribed discs intersect. A single exact dyadic comparison (squared centre distance against squared radius sum).

Equations

• Hex.Intersects i₁ i₂ = (i₁.val.square.discsMeet i₂.val.square = true)

@[instance_reducible]

instance Hex.instDecidableIntersects {p : ZPoly} {i₁ i₂ : RefinedIsolation p} : Decidable (Intersects i₁ i₂)

Equations

• Hex.instDecidableIntersects = Hex.instDecidableIntersects._aux_1

def Hex.SimpleRoot (p : ZPoly) : Type

The identity of a simple root, independent of which isolation witnessed it. (Quot of a bare relation; the companion proves Intersects is an equivalence on RefinedIsolation whose classes are the simple roots.)

Equations

• Hex.SimpleRoot p = Quot Hex.Intersects

def Hex.SimpleRoot.mk {p : ZPoly} (iso : RefinedIsolation p) : SimpleRoot p

The simple root witnessed by a refined isolation.

Equations

• Hex.SimpleRoot.mk iso = Quot.mk Hex.Intersects iso

def Hex.SimpleRoot.ofSquare (p : ZPoly) (s : DyadicSquare) (hw : atomWitness p s := by decide) (hp : ↑(mahlerPrec p) ≤ s.prec := by decide) : SimpleRoot p

The simple root of p isolated by the square s. Both side conditions are decidable checks on printable data, so a caller who has only a square -- a Repr output, a fixture, a literal -- rebuilds the certificate with decide and recovers the root. The companion's ofSquare_mk identifies the result with the root that any isolation on that square witnesses.

Equations

• Hex.SimpleRoot.ofSquare p s hw hp = Hex.SimpleRoot.mk ⟨{ square := s, witness := Hex.AtomCertificate.ofWitness hw }, hp⟩

def Hex.RefinedIsolation.sameRoot {p : ZPoly} (i₁ i₂ : RefinedIsolation p) : Bool

Boolean form of Intersects, used for equality tests on data containing roots (see hex-number-field).

Equations

• i₁.sameRoot i₂ = i₁.val.square.discsMeet i₂.val.square

theorem Hex.AtomCertificate.size_gt_one {p : ZPoly} {s : DyadicSquare} (certificate : AtomCertificate p s) : 1 < DensePoly.size p

Every structural atom certificate belongs to a polynomial with at least two stored coefficients. Exact reflection preserves that count.

theorem Hex.DyadicRootIsolation.size_gt_one {p : ZPoly} (i : DyadicRootIsolation p) : 1 < DensePoly.size p

A certified atom needs at least two stored coefficients.

theorem Hex.DyadicRootIsolation.posDegree {p : ZPoly} (i : DyadicRootIsolation p) : 0 < DensePoly.natDegree p

A certified atom can only exist for a positive-degree polynomial.

theorem Hex.SimpleRoot.posDegree {p : ZPoly} (x : SimpleRoot p) : 0 < DensePoly.natDegree p

Every represented simple root belongs to a positive-degree polynomial.

def Hex.DyadicRootIsolation.toRefined? {p : ZPoly} (iso : DyadicRootIsolation p) : Option (RefinedIsolation p)

Wrap an isolation as a RefinedIsolation when it meets the separation precision, deciding the subtype bound. ZPoly.isolateComplexRoots?'s output always qualifies (its target has a separationDepth ≥ mahlerPrec floor); this is the constructor consumers use to record that fact.

Equations

• iso.toRefined? = if h : ↑(Hex.mahlerPrec p) ≤ iso.square.prec then some ⟨iso, h⟩ else none