theorem Hex.RefinedIsolation.refineTo?_isSome {p : ZPoly} (rep : RefinedIsolation p) (target : ℤ) : (rep.refineTo? target).isSome = true

The local refinement budget is sufficient to reach every requested precision for an already certified simple-root atom under the default mixed strategy.

theorem Hex.RefinedIsolation.refineTo?_precision {p : ZPoly} (rep : RefinedIsolation p) (target : ℤ) (strategy : AtomStrategy := AtomStrategy.nkThenPellet) {out : { rep' : RefinedIsolation p // SimpleRoot.mk rep' = SimpleRoot.mk rep }} (h : rep.refineTo? target strategy = some out) : target ≤ (↑↑out).square.prec

Every successful refined result reaches the requested precision.

noncomputable def Hex.DyadicComplexBall.center (b : DyadicComplexBall) : ℂ

The complex centre represented by a dyadic complex ball.

Equations

• b.center = HexRootsMathlib.GaussDyadic.toComplex (b.re, b.im)

noncomputable def Hex.DyadicComplexBall.realRadius (b : DyadicComplexBall) : ℝ

The real radius represented by a dyadic complex ball.

Equations

• b.realRadius = HexRootsMathlib.Dyadic.toReal b.radius

noncomputable def Hex.DyadicComplexBall.set (b : DyadicComplexBall) : Set ℂ

The ordinary closed complex disc represented by an executable ball.

Equations

• b.set = Metric.closedBall b.center b.realRadius

@[simp]

theorem Hex.DyadicComplexBall.realRadius_add (a b : DyadicComplexBall) : (a.add b).realRadius = a.realRadius + b.realRadius

Ball addition adds the represented radii.

@[simp]

theorem Hex.DyadicComplexBall.realRadius_mul (a b : DyadicComplexBall) : (a.mul b).realRadius = HexRootsMathlib.Dyadic.toReal (GaussDyadic.hi (a.re, a.im)) * b.realRadius + HexRootsMathlib.Dyadic.toReal (GaussDyadic.hi (b.re, b.im)) * a.realRadius + a.realRadius * b.realRadius

Ball multiplication propagates centre and radius errors by the standard bilinear enclosure formula.

theorem Hex.DyadicComplexBall.realRadius_toBall_le {s : DyadicSquare} {prec : ℤ} (hprec : prec ≤ s.prec) : s.toBall.realRadius ≤ 2 * 2 ^ (-prec)

A square refined to prec has a dyadic-ball radius bounded by two ulps at that precision.

theorem Hex.DyadicComplexBall.realRadius_toBall_le_three_quarters {s : DyadicSquare} {prec : ℤ} (hprec : prec + 1 ≤ s.prec) : s.toBall.realRadius ≤ 3 / 4 * 2 ^ (-prec)

Refinement one bit beyond prec gives the sharper three-quarter-ulp radius used by the bounded Horner disambiguation majorant.

theorem Hex.DyadicComplexBall.realRadius_ofRat_le (q : ℚ) (prec : ℤ) : (ofRat q prec).realRadius ≤ 2 ^ (-prec)

The rational enclosure requested at precision prec has radius at most 2 ^ (-prec).

theorem Hex.DyadicComplexBall.add_mem {a b : DyadicComplexBall} {z w : ℂ} (hz : z ∈ a.set) (hw : w ∈ b.set) : z + w ∈ (a.add b).set

Minkowski addition encloses sums of enclosed values.

theorem Hex.DyadicComplexBall.meets_of_mem {a b : DyadicComplexBall} {z : ℂ} (ha : z ∈ a.set) (hb : z ∈ b.set) : a.meets b = true

Two certified balls containing the same point meet.

theorem Hex.DyadicComplexBall.ofRat_mem (q : ℚ) (prec : ℤ) : ↑q ∈ (ofRat q prec).set

A rational coefficient lies in its executable rounded enclosure.

theorem Hex.DyadicComplexBall.mul_mem {a b : DyadicComplexBall} {z w : ℂ} (hz : z ∈ a.set) (hw : w ∈ b.set) : z * w ∈ (a.mul b).set

Executable ball multiplication encloses products of enclosed values.

theorem Hex.DyadicComplexBall.mem_toBall {s : DyadicSquare} {z : ℂ} (hz : z ∈ HexRootsMathlib.DyadicSquare.closedDisc s) : z ∈ s.toBall.set

The dyadic ball view of a square contains its true circumscribed closed disc.

theorem Hex.DyadicComplexBall.evalRatBall_mem (f : DensePoly ℚ) (s : DyadicSquare) (coeffPrec : ℤ) {z : ℂ} (hz : z ∈ s.toBall.set) : Polynomial.eval₂ (algebraMap ℚ ℂ) z (HexPolyMathlib.toPolynomial f) ∈ (PolyQuot.evalRatBall f s coeffPrec).set

Executable Horner evaluation encloses polynomial evaluation throughout the supplied root ball.

theorem Hex.DyadicComplexBall.inv_mem {a b : DyadicComplexBall} {z : ℂ} {prec : ℤ} (hz : z ∈ a.set) (h : a.inv? prec = some b) : z⁻¹ ∈ b.set

A successful reciprocal ball encloses the reciprocal of every enclosed value.

theorem Hex.RefinedIsolation.mulRadius_le {p q : ZPoly} (a : RefinedIsolation p) (b : RefinedIsolation q) (prec : ℤ) (strategy : AtomStrategy) {ar : { r : RefinedIsolation p // SimpleRoot.mk r = SimpleRoot.mk a }} {br : { r : RefinedIsolation q // SimpleRoot.mk r = SimpleRoot.mk b }} (har : a.refineTo? (prec + ↑(8 + PolyQuot.rootBits (↑a).square + PolyQuot.rootBits (↑b).square)) strategy = some ar) (hbr : b.refineTo? (prec + ↑(8 + PolyQuot.rootBits (↑a).square + PolyQuot.rootBits (↑b).square)) strategy = some br) : ((↑↑ar).square.toBall.mul (↑↑br).square.toBall).realRadius ≤ 2 ^ (-(prec + 4))

Refining two root isolations by the multiplication guard makes the product ball four bits smaller than the requested operation precision. The literal guard formula mirrors AlgebraicRoot.mulGuardBits, which is defined in the downstream lazy-arithmetic module. This margin is stronger than singleton selection currently requires.

theorem Hex.RefinedIsolation.invBall_exists {p : ZPoly} (a : RefinedIsolation p) (prec : ℤ) (hprec : 0 ≤ prec) (strategy : AtomStrategy) (hlower : (↑(p.coeffAbsMax + 1))⁻¹ < ‖HexRootsMathlib.RefinedIsolation.root a‖) {ar : { r : RefinedIsolation p // SimpleRoot.mk r = SimpleRoot.mk a }} (har : a.refineTo? (prec + ↑(2 * ceilLog2 (p.coeffAbsMax + 1) + 16)) strategy = some ar) : ∃ (ball : DyadicComplexBall), (↑↑ar).square.toBall.inv? (prec + ↑(2 * ceilLog2 (p.coeffAbsMax + 1) + 16)) = some ball ∧ ball.realRadius ≤ 2 ^ (-(prec + 4))

The reciprocal guard separates a refined nonzero root ball from zero and leaves four bits of radius slack after reciprocal distortion and rounding. The literal guard formula mirrors AlgebraicRoot.invGuardBits, which is defined in the downstream lazy-arithmetic module. This margin is stronger than singleton selection currently requires.

theorem Hex.PolyQuot.approx_sound {p : ZPoly} {x : SimpleRoot p} (a : PolyQuot p x) (rep : RefinedIsolation p) (h : SimpleRoot.mk rep = x) (prec : ℤ) : a.toComplex rep h ∈ (a.approx rep h prec).2.set

Fixed-field approximation always encloses the represented complex value.

theorem Hex.PolyQuot.approx_radius {p : ZPoly} {x : SimpleRoot p} (a : PolyQuot p x) (rep : RefinedIsolation p) (h : SimpleRoot.mk rep = x) (prec : ℤ) : (a.approx rep h prec).2.realRadius ≤ 2 ^ (-prec)

The guarded approximation achieves the requested dyadic radius.