theorem Hex.PolyQuot.norm_rat_le_ratAbsCeil (q : ℚ) : ‖↑q‖ ≤ ↑(ratAbsCeil q)

The executable rational ceiling majorizes the complex norm of the rational coefficient.

theorem Hex.PolyQuot.norm_toComplex_le_valueMajorant {p : ZPoly} {x : SimpleRoot p} (a : PolyQuot p x) (rep : RefinedIsolation p) (h : SimpleRoot.mk rep = x) : ‖a.toComplex rep h‖ ≤ ↑a.valueMajorant

The coordinate majorant bounds the complex norm at the selected field embedding.

theorem Hex.AlgebraicRoot.norm_lt_rootBound (a : AlgebraicRoot) : ‖a.toComplex‖ < ↑(2 ^ cauchyExp a.p + 1)

The executable Cauchy root bound majorizes the represented complex norm.

theorem Hex.ZPoly.normalizeEval_ne_zero {q : ZPoly} (hq : q ≠ 0) : q.normalizeEval ≠ 0

Normalizing an evaluation eliminant preserves nonzeroness.

theorem Hex.ZPoly.normalizeEval_isRoot {q : ZPoly} {z : ℂ} (hq : q ≠ 0) (hz : z ≠ 0) (hroot : (HexRootsMathlib.toPolyℂ q).IsRoot z) : (HexRootsMathlib.toPolyℂ q.normalizeEval).IsRoot z

Normalizing an evaluation eliminant preserves every nonzero complex root.

theorem Hex.ZPoly.normalizeEval_root_norm_lower {q : ZPoly} {z : ℂ} (hq : q ≠ 0) (hz : z ≠ 0) (hroot : (HexRootsMathlib.toPolyℂ q).IsRoot z) : (↑q.evalLowerDenom)⁻¹ < ‖z‖

The normalized evaluation eliminant gives the lower bound used by the bounded zero test.

theorem Hex.DyadicComplexBall.realRadius_horner_le {z value coefficient : ℂ} (zBall valueBall coefficientBall : DyadicComplexBall) (B V E δ : ℝ) (hz : z ∈ zBall.set) (hvalue : value ∈ valueBall.set) (hcoefficient : coefficient ∈ coefficientBall.set) (hzNorm : ‖z‖ ≤ B) (hvalueNorm : ‖value‖ ≤ V) (hzRadius : zBall.realRadius ≤ 3 / 4 * δ) (hvalueRadius : valueBall.realRadius ≤ E * δ) (hcoefficientRadius : coefficientBall.realRadius ≤ δ) (hB : 0 ≤ B) (hV : 0 ≤ V) (hE : 0 ≤ E) (hδ : 0 ≤ δ) (hδ1 : δ ≤ 1) : (coefficientBall.add (zBall.mul valueBall)).realRadius ≤ (2 * V + 2 * B * E + 3 * E + 1) * δ

One Horner step preserves the executable error-majorant recurrence.

theorem Hex.DyadicComplexBall.excludesZero_sound {b : DyadicComplexBall} {z : ℂ} (hz : z ∈ b.set) (hexcludes : b.excludesZero = true) : z ≠ 0

A ball that passes the executable zero-exclusion test cannot contain zero.

theorem Hex.DyadicComplexBall.excludesZero_of_mem_of_lower {b : DyadicComplexBall} {z : ℂ} {D : ℕ} (hD : 0 < D) (hz : z ∈ b.set) (hlower : (↑D)⁻¹ < ‖z‖) (hsmall : 3 * ↑D * b.realRadius < 1) : b.excludesZero = true

A sufficiently small ball containing a value above a reciprocal lower bound passes the executable zero-exclusion test.

theorem Hex.PolyQuot.Roots.evalBall?_radius {p : ZPoly} {x : SimpleRoot p} [p.CheckedIrreducible] (f : DensePoly (PolyQuot p x)) (rep : RefinedIsolation p) (h : SimpleRoot.mk rep = x) (candidate : AlgebraicRoot) (prec : ℕ) {ball : DyadicComplexBall} (hrun : evalBall? f rep h candidate prec = some ball) : ball.realRadius ≤ ↑(evalMajorant f candidate.p) * 2 ^ (-↑prec)

The certified fixed-field Horner evaluator has the radius promised by its executable error majorant.

theorem Hex.evalRadiusSmall_real {q : ZPoly} {radius : Dyadic} (hsmall : evalRadiusSmall q radius = true) : 3 * ↑q.evalLowerDenom * HexRootsMathlib.Dyadic.toReal radius < 1

The executable radius predicate is its stated real inequality.

theorem Hex.evalRadiusSmall_of_real {q : ZPoly} {radius : Dyadic} (hsmall : 3 * ↑q.evalLowerDenom * HexRootsMathlib.Dyadic.toReal radius < 1) : evalRadiusSmall q radius = true

The real radius inequality implies the executable radius predicate.

theorem Hex.evalDisambiguationLimit_radius_small (q : ZPoly) (majorant : ℕ) (ball : DyadicComplexBall) (hradius : ball.realRadius ≤ ↑(Nat.max 1 majorant) * 2 ^ (-↑(evalDisambiguationLimit q majorant))) : evalRadiusSmall q ball.radius = true

The prescribed endpoint has enough logarithmic slack: any ball whose radius is bounded by max 1 majorant ulps at that precision satisfies the zero-test radius predicate.

theorem Hex.evalDisambiguationPrec_sound {q : ZPoly} {majorant prec : ℕ} {evalAt : ℕ → Option DyadicComplexBall} (hrun : evalDisambiguationPrec q majorant evalAt = some prec) : ∃ (ball : DyadicComplexBall), evalAt prec = some ball ∧ evalRadiusSmall q ball.radius = true

A successful bounded precision search exposes an available ball satisfying the requested radius predicate.

theorem Hex.evalDisambiguationPrec_isSome_of_endpoint (q : ZPoly) (majorant : ℕ) (evalAt : ℕ → Option DyadicComplexBall) {ball : DyadicComplexBall} (hball : evalAt (evalDisambiguationLimit q majorant) = some ball) (hsmall : evalRadiusSmall q ball.radius = true) : (evalDisambiguationPrec q majorant evalAt).isSome = true

The bounded search succeeds whenever its prescribed endpoint produces a ball satisfying the radius predicate.

theorem Hex.PolyQuot.Roots.evalPrec_isSome {p : ZPoly} {x : SimpleRoot p} [p.CheckedIrreducible] (q : ZPoly) (f : DensePoly (PolyQuot p x)) (rep : RefinedIsolation p) (h : SimpleRoot.mk rep = x) (candidate : AlgebraicRoot) : (evalDisambiguationPrec q (evalMajorant f candidate.p) (evalBall? f rep h candidate)).isSome = true

The prescribed bounded precision search succeeds for the fixed-field ball evaluator.

theorem Hex.PolyQuot.Roots.retainZero?_isSome {p : ZPoly} {x : SimpleRoot p} [p.CheckedIrreducible] (q : ZPoly) (f : DensePoly (PolyQuot p x)) (rep : RefinedIsolation p) (h : SimpleRoot.mk rep = x) (candidate : AlgebraicRoot) : (retainZero? q (evalMajorant f candidate.p) (evalBall? f rep h candidate)).isSome = true

The bounded zero-retention test cannot fail for the fixed-field ball evaluator.

theorem Hex.retainZero?_sound {q : ZPoly} {majorant : ℕ} {evalAt : ℕ → Option DyadicComplexBall} {z : ℂ} {keep : Bool} (hq : q ≠ 0) (hroot : (HexRootsMathlib.toPolyℂ q).IsRoot z) (hsound : ∀ (prec : ℕ) (ball : DyadicComplexBall), evalAt prec = some ball → z ∈ ball.set) (hrun : retainZero? q majorant evalAt = some keep) : keep = true ↔ z = 0

Conditional correctness of the bounded zero test. Whenever the search returns, it retains exactly the zero value represented by the eliminant root and the certified evaluation balls.