def Hex.GaussDyadic.lo (z : GaussDyadic) : Dyadic

lo(c) = max(|Re c|, |Im c|): lo(c) ≤ |c| ≤ √2·lo(c).

Equations

• z.lo = Hex.Dyadic.max (Hex.Dyadic.abs z.fst) (Hex.Dyadic.abs z.snd)

def Hex.GaussDyadic.hi (z : GaussDyadic) : Dyadic

hi(c) = |Re c| + |Im c|: |c| ≤ hi(c) ≤ √2·|c|.

Equations

• z.hi = Hex.Dyadic.abs z.fst + Hex.Dyadic.abs z.snd

def Hex.sqrt2Lo : Dyadic

181/128 < √2.

Equations

• Hex.sqrt2Lo = Dyadic.ofIntWithPrec 181 7

def Hex.sqrt2Hi : Dyadic

√2 < 1449/1024.

Equations

• Hex.sqrt2Hi = Dyadic.ofIntWithPrec 1449 10

theorem Hex.sqrt2Lo_sq_lt_two : sqrt2Lo * sqrt2Lo < 2

(181/128)² < 2, the defining inequality of sqrt2Lo (it reduces to 32761/16384 < 2).

theorem Hex.two_lt_sqrt2Hi_sq : 2 < sqrt2Hi * sqrt2Hi

2 < (1449/1024)², the defining inequality of sqrt2Hi (it reduces to 2 < 2099601/1048576).

def Hex.DyadicSquare.radiusLo (s : DyadicSquare) : Dyadic

Dyadic lower bound sqrt2Lo·2^{−prec} for the square's circumscribed radius 2^{−prec}·√2.

Equations

• s.radiusLo = Dyadic.ofIntWithPrec 181 (s.prec + 7)

def Hex.DyadicSquare.radiusHi (s : DyadicSquare) : Dyadic

Dyadic upper bound sqrt2Hi·2^{−prec} for the square's circumscribed radius 2^{−prec}·√2.

Equations

• s.radiusHi = Dyadic.ofIntWithPrec 1449 (s.prec + 10)

def Hex.pelletAt (cs : Array GaussDyadic) (k : Nat) (rlo rhi : Dyadic) : Bool

One Pellet inequality: lo(cs[k])·rlo^k > Σ_{i ≠ k} hi(cs[i])·rhi^i (strict), with cs the exact Taylor coefficients. The right side is a single fold over cs carrying the running power rhi^i, skipping the i = k term. Returns false when k ≥ cs.size (no such coefficient).

Equations

• One or more equations did not get rendered due to their size.

def Hex.TaylorShift.witnessCheck {p : ZPoly} (s : DyadicSquare) (shift : TaylorShift p s.center) (k : Nat) : Bool

Three-radius strong Pellet check from an already-computed Taylor shift. Keeping this coefficient-level kernel separate lets a certifier test every candidate root count at one centre without repeating the quadratic Taylor shift.

Equations

• One or more equations did not get rendered due to their size.

def Hex.TaylorShift.combinedWitnessCheck {p : ZPoly} (s : DyadicSquare) (shift : TaylorShift p s.center) (k : Nat) : Bool

At shallow centre precision, try the cached exact Taylor check first; this preserves its small constant on easy canonical inputs. At deep precision, try soft Graeffe first so successful witnesses avoid evaluating the increasingly large exact coefficients.

Equations

• One or more equations did not get rendered due to their size.

def Hex.witnessCheck (p : ZPoly) (s : DyadicSquare) (k : Nat) : Bool

Three-radius strong Pellet check for k roots (with multiplicity) in the circumscribed disc of s. It accepts either the exact Taylor comparison at the base, doubled, and quadrupled radii, or an outward-rounded comparison after transporting the polynomial and all three radii through Graeffe root-squaring. Both routes imply BSSY's three-radius root-count condition.

Equations

• Hex.witnessCheck p s k = Hex.TaylorShift.combinedWitnessCheck s (Hex.TaylorShift.compute p s.center) k

@[simp]

theorem Hex.TaylorShift.combinedWitnessCheck_eq {p : ZPoly} (s : DyadicSquare) (shift : TaylorShift p s.center) (k : Nat) : combinedWitnessCheck s shift k = Hex.witnessCheck p s k

The centre-indexed combined kernel is exactly the public polynomial witness check.

theorem Hex.witnessCheck_false {p : ZPoly} {s : DyadicSquare} {k : Nat} (h : DensePoly.size p ≤ k) : witnessCheck p s k = false

A root-count witness cannot select a coefficient outside the polynomial.

theorem Hex.TaylorShift.witnessCheck_implies {p : ZPoly} (s : DyadicSquare) (shift : TaylorShift p s.center) (k : Nat) (h : witnessCheck s shift k = true) : Hex.witnessCheck p s k = true

A successful exact centre-indexed check implies the public disjunctive witness check.

def Hex.witness (p : ZPoly) (s : DyadicSquare) (k : Nat) : Prop

Strong Pellet witness accepted by the exact or outward-rounded Graeffe route. Implies (Mathlib companion): p has exactly k roots, with multiplicity, in the circumscribed disc of s and in its doubled and quadrupled concentric discs, with no roots on their boundaries.

Equations

• Hex.witness p s k = (Hex.witnessCheck p s k = true)

@[instance_reducible]

instance Hex.instDecidableWitness {p : ZPoly} {s : DyadicSquare} {k : Nat} : Decidable (witness p s k)

Equations

• Hex.instDecidableWitness = Hex.instDecidableWitness._aux_1

def Hex.exactRootFree (p : ZPoly) (s : DyadicSquare) : Bool

Exact single-radius T_0 exclusion: the circumscribed disc of s certifiably contains no root of p, i.e. lo(c₀) > Σ_{i ≥ 1} hi(c_i)·ρhi^i (the rlo^0 = 1 power makes the base radius bound rlo unused). This fires more often than the three-radius witness _ _ 0; discarding a square during refinement needs certification while keeping one is always sound, so refinement uses this.

Equations

• Hex.exactRootFree p s = Hex.pelletAt (Hex.taylor p s.center) 0 s.radiusLo s.radiusHi

def Hex.rootFree (p : ZPoly) (s : DyadicSquare) : Bool

Graeffe T₀ discard with exact fallback. Shallow centres seed the coefficient balls from one exact Taylor shift; large centres use the fully soft constructor whose mantissas are independent of centre bit-length.

Equations

• One or more equations did not get rendered due to their size.

theorem Hex.exactRootFree_implies_rootFree {p : ZPoly} {s : DyadicSquare} (h : exactRootFree p s = true) : rootFree p s = true

Exact exclusion remains a sufficient result for the combined filter.

def Hex.DyadicSquare.toBall (s : DyadicSquare) : DyadicComplexBall

The circumscribed disc of s as a ball, with the dyadic upper-bound radius radiusHi (≥ the true radius 2^{−prec}·√2).

Equations

• s.toBall = { re := s.re, im := s.im, radius := s.radiusHi }

def Hex.DyadicComplexBall.zero : DyadicComplexBall

The exact zero complex ball.

Equations

• Hex.DyadicComplexBall.zero = { re := 0, im := 0, radius := 0 }

def Hex.DyadicComplexBall.add (a b : DyadicComplexBall) : DyadicComplexBall

Minkowski sum of two closed dyadic complex balls.

Equations

• a.add b = { re := a.re + b.re, im := a.im + b.im, radius := a.radius + b.radius }

def Hex.DyadicComplexBall.mul (a b : DyadicComplexBall) : DyadicComplexBall

Product enclosure for two closed dyadic complex balls.

Equations

• One or more equations did not get rendered due to their size.

def Hex.DyadicComplexBall.ofRat (q : Rat) (prec : Int) : DyadicComplexBall

Enclose a rational number by a real-centred dyadic complex ball. Exact dyadic rationals receive radius zero; otherwise one ulp encloses the downward rounding error. At nonnegative precision the denominator test avoids materializing and normalizing a large intermediate rational.

Equations

• One or more equations did not get rendered due to their size.

def Hex.evalBall (p : ZPoly) (s : DyadicSquare) : DyadicComplexBall

A ball containing p(z) for every z in the circumscribed disc of s: centred at the exact value p(centre) = c₀, with radius Σ_{i ≥ 1} hi(cᵢ)·radiusHi^i ≥ |p(z) − p(centre)| by the triangle inequality on the Taylor expansion. rootFree is the corollary lo(c₀) > radius (kept separate so the audited pelletAt shape is unchanged).

Equations

• One or more equations did not get rendered due to their size.

def Hex.DyadicComplexBall.excludesZero (b : DyadicComplexBall) : Bool

The ball certifiably excludes 0: radius < lo(centre) ≤ |centre|, an exact dyadic comparison. The sound direction for "this value is certainly nonzero"; failing this test means only that 0 could not be excluded.

Equations

• b.excludesZero = decide (b.radius < Hex.Dyadic.max (Hex.Dyadic.abs b.re) (Hex.Dyadic.abs b.im))

def Hex.DyadicComplexBall.meets (b₁ b₂ : DyadicComplexBall) : Bool

The closed balls intersect: squared centre distance at most the squared radius sum, all exact dyadics.

Equations

• b₁.meets b₂ = decide (Hex.GaussDyadic.distSq (b₁.re, b₁.im) (b₂.re, b₂.im) ≤ (b₁.radius + b₂.radius) * (b₁.radius + b₂.radius))

def Hex.DyadicSquare.meetsBall (s : DyadicSquare) (b : DyadicComplexBall) : Bool

The ball meets the circumscribed disc of s (conservative: uses the radiusHi upper bound for the disc radius, so a false certifies disjointness from the true disc as well).

Equations

• s.meetsBall b = s.toBall.meets b

structure Hex.DyadicRootCluster (p : ZPoly) : Type

A certified cluster: an edge-connected set of grid squares at a common prec, whose enclosing disc contains exactly k roots with multiplicity. The component squares are the data that refinement operates on; subdividing the enclosing square instead would stall (it can equal the parent square when a root sits on a grid line, even as the component squares themselves shrink). The Pellet certificate, by contrast, is attached to the circumscribed disc of encSquare squares. This is an output type; the refinement worklist holds uncertified Component values.

• squares : Array DyadicSquare

  The component's grid squares: nonempty, common prec, edge-connected.

• k : Nat

  The number of roots, counted with multiplicity, in the enclosing disc.

• k_pos : 0 < self.k

  A cluster carries at least one root.

• witness : Hex.witness p (encSquare self.squares) self.k

  The strong Pellet certificate on the enclosing square's disc.