def Hex.Dyadic.abs (x : Dyadic) : Dyadic

Absolute value of a dyadic number.

Equations

• Hex.Dyadic.abs x = if x < 0 then -x else x

def Hex.Dyadic.max (x y : Dyadic) : Dyadic

The larger of two dyadic numbers.

Equations

• Hex.Dyadic.max x y = if x ≤ y then y else x

def Hex.Dyadic.min (x y : Dyadic) : Dyadic

The smaller of two dyadic numbers.

Equations

• Hex.Dyadic.min x y = if x ≤ y then x else y

def Hex.ceilLog2 (n : Nat) : Nat

Smallest t with n ≤ 2^t (junk 0 for n ≤ 1).

Equations

• Hex.ceilLog2 n = if n ≤ 1 then 0 else (n - 1).log2 + 1

def Hex.Dyadic.ceilLog2 : Dyadic → Int

For x > 0: smallest t : Int with x ≤ 2^t; junk 0 for x ≤ 0. For x = n·2^{−k} with odd n > 0: ceilLog2 n − k.

Equations

• Hex.Dyadic.ceilLog2 Dyadic.zero = 0
• Hex.Dyadic.ceilLog2 (Dyadic.ofOdd n k hn) = if n < 0 then 0 else ↑(Hex.ceilLog2 n.toNat) - k

@[reducible, inline]

abbrev Hex.GaussDyadic : Type

A Gaussian dyadic number re + im·i, represented as the pair (re, im).

Equations

• Hex.GaussDyadic = (Dyadic × Dyadic)

def Hex.GaussDyadic.ofInt (i : Int) : GaussDyadic

The Gaussian dyadic i + 0·i for an integer i.

Equations

• Hex.GaussDyadic.ofInt i = (Dyadic.ofInt i, 0)

def Hex.GaussDyadic.add (z w : GaussDyadic) : GaussDyadic

Sum of two Gaussian dyadics, (a+bi) + (c+di) = (a+c) + (b+d)i.

Equations

• z.add w = (z.fst + w.fst, z.snd + w.snd)

def Hex.GaussDyadic.sub (z w : GaussDyadic) : GaussDyadic

Difference of two Gaussian dyadics, (a+bi) − (c+di) = (a−c) + (b−d)i.

Equations

• z.sub w = (z.fst - w.fst, z.snd - w.snd)

def Hex.GaussDyadic.conj (z : GaussDyadic) : GaussDyadic

Complex conjugate a − b·i of a + b·i.

Equations

• z.conj = (z.fst, -z.snd)

def Hex.GaussDyadic.mul (z w : GaussDyadic) : GaussDyadic

Product of two Gaussian dyadics, (a+bi)(c+di) = (ac − bd) + (ad + bc)i.

Equations

• z.mul w = (z.fst * w.fst - z.snd * w.snd, z.fst * w.snd + z.snd * w.fst)

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

The squared modulus a² + b² of a + b·i, an exact dyadic.

Equations

• z.normSq = z.fst * z.fst + z.snd * z.snd

def Hex.GaussDyadic.distSq (z w : GaussDyadic) : Dyadic

The squared distance |z − w|² between two Gaussian dyadics, an exact dyadic.

Equations

• z.distSq w = (z.sub w).normSq

structure Hex.DyadicSquare : Type

A closed axis-aligned dyadic square in the complex plane: centre re + im·i, half-width 2^{−prec}, circumscribed disc radius 2^{−prec}·√2.

• re : Dyadic

  Real part of the centre.

• im : Dyadic

  Imaginary part of the centre.

• prec : Int

  Base-2 exponent of the half-width 2^{−prec}.

@[instance_reducible]

instance Hex.instDecidableEqDyadicSquare : DecidableEq DyadicSquare

Equations

• Hex.instDecidableEqDyadicSquare = Hex.instDecidableEqDyadicSquare.decEq

def Hex.instDecidableEqDyadicSquare.decEq (x✝ x✝¹ : DyadicSquare) : Decidable (x✝ = x✝¹)

Equations

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

def Hex.DyadicSquare.center (s : DyadicSquare) : GaussDyadic

The Gaussian-dyadic centre re + im·i of the square.

Equations

• s.center = (s.re, s.im)

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

The half-width 2^{−prec} of the square, an exact dyadic.

Equations

• s.halfWidth = Dyadic.ofIntWithPrec 1 s.prec

def Hex.DyadicSquare.discsMeet (s t : DyadicSquare) : Bool

The circumscribed discs of s and t intersect (closed discs): distSq centres ≤ (r_s + r_t)² with r = √2·2^{−prec}, so (r_s + r_t)² = 2·4^{−p_s} + 2·4^{−p_t} + 4·2^{−p_s−p_t}, all exact dyadics.

Equations

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

def Hex.DyadicSquare.discContains (s : DyadicSquare) (z : GaussDyadic) : Bool

The circumscribed disc of s contains the Gaussian-dyadic point z, including boundary contact. Squaring the radius removes the irrational √2, so the test is one exact dyadic comparison.

Equations

• s.discContains z = decide (s.center.distSq z ≤ 2 * Dyadic.ofIntWithPrec 1 (2 * s.prec))

def Hex.DyadicSquare.discInside (inner outer : DyadicSquare) : Bool

inner's circumscribed disc is contained in outer's: r_i ≤ r_o (i.e. outer.prec ≤ inner.prec) and distSq centres ≤ (r_o − r_i)² = 2·4^{−p_o} + 2·4^{−p_i} − 4·2^{−p_o−p_i}.

Equations

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

def Hex.DyadicSquare.squareInside (inner outer : DyadicSquare) : Bool

inner's closed square is contained in outer's closed square: max |Δre| |Δim| + 2^{−p_i} ≤ 2^{−p_o} (exact dyadics).

Equations

• inner.squareInside outer = decide (Hex.Dyadic.max (Hex.Dyadic.abs (inner.re - outer.re)) (Hex.Dyadic.abs (inner.im - outer.im)) + inner.halfWidth ≤ outer.halfWidth)

structure Hex.DyadicComplexBall : Type

A complex ball with dyadic data, the output type of numerical evaluation here and in hex-number-field.

• re : Dyadic

  Real part of the centre.

• im : Dyadic

  Imaginary part of the centre.

• radius : Dyadic

  Radius of the ball.

structure Hex.Component : Type

An uncertified component in the refinement worklist: an edge-connected set of grid squares at a common prec, plus the root count of its most recently certified ancestor. candidateK only selects the order of the speculative Newton step; it is never trusted, since every output is re-certified.

• squares : Array DyadicSquare

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

• candidateK : Nat

  Root count carried from the most recently certified ancestor; an untrusted hint for step ordering.

structure Hex.SquareBounds : Type

Exact axis-aligned bounds used to enclose an array of dyadic squares.

• xmin : Dyadic

  Lower real-coordinate bound.

• xmax : Dyadic

  Upper real-coordinate bound.

• ymin : Dyadic

  Lower imaginary-coordinate bound.

• ymax : Dyadic

  Upper imaginary-coordinate bound.

def Hex.DyadicSquare.bounds (s : DyadicSquare) : SquareBounds

The exact coordinate bounds contributed by one dyadic square.

Equations

• s.bounds = { xmin := s.re - s.halfWidth, xmax := s.re + s.halfWidth, ymin := s.im - s.halfWidth, ymax := s.im + s.halfWidth }

def Hex.SquareBounds.merge (b : SquareBounds) (s : DyadicSquare) : SquareBounds

Extend exact coordinate bounds by one dyadic square.

Equations

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

def Hex.SquareBounds.extend (b : Option SquareBounds) (s : DyadicSquare) : Option SquareBounds

Add one square to an optional bounding box.

Equations

• Hex.SquareBounds.extend none s = some s.bounds
• Hex.SquareBounds.extend (some b_2) s = some (b_2.merge s)

def Hex.boundingBox (squares : Array DyadicSquare) : Option SquareBounds

Exact bounding box of an array of dyadic squares.

Equations

• Hex.boundingBox squares = Array.foldl Hex.SquareBounds.extend none squares

def Hex.encSquare (squares : Array DyadicSquare) : DyadicSquare

The smallest square with power-of-two half-width, centred at the bounding-box centre, containing every square. Junk ⟨0,0,0⟩ on the empty array (callers keep components nonempty).

Each square contributes its own half-width to the bounding box (robust to mixed prec), the centre is the exact midpoint of the box (a right shift by one bit), and the result prec is chosen so that its half-width 2^{−q} is the smallest power of two at least the box half-width. On a single square input this returns that square exactly.

Equations

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

def Hex.HasOnlySimpleRoots (p : ZPoly) : Prop

p has only simple complex roots when the executable rational gcd of p and p' is constant. This is definitionally Hex.ZPoly.SquareFreeRat; the Mathlib bridge proves its equivalence to polynomial squarefreeness when p ≠ 0.

Equations

• Hex.HasOnlySimpleRoots p = p.SquareFreeRat

@[instance_reducible]

instance Hex.instDecidableHasOnlySimpleRoots (p : ZPoly) : Decidable (HasOnlySimpleRoots p)

Equations

• Hex.instDecidableHasOnlySimpleRoots p = Hex.instDecidableHasOnlySimpleRoots._aux_1 p