def Hex.twoPow (k : Int) : Dyadic

The exact dyadic 2^k for an integer exponent k, as 1 shifted left by k (a right shift when k < 0).

Equations

• Hex.twoPow k = 1 <<< k

def Hex.ceilLog2Nat (m : Nat) : Nat

The least k with m ≤ 2^k, for m ≥ 1; 0 for m ≤ 1.

For m ≥ 2 we have m ≤ 2^k ⟺ m − 1 < 2^k ⟺ ⌊log₂ (m − 1)⌋ < k, so the least such k is ⌊log₂ (m − 1)⌋ + 1. The m ≤ 1 branch returns 0, the least k with 1 ≤ 2^k.

Equations

• Hex.ceilLog2Nat m = if m ≤ 1 then 0 else (m - 1).log2 + 1

def Hex.ceilLog2Dyadic : Dyadic → Int

The least integer e with x ≤ 2^e, for a positive dyadic x; junk value 0 for x ≤ 0 (documented, never read).

A nonzero dyadic is ofOdd n k with value n · 2^{−k}. For n > 0, n · 2^{−k} ≤ 2^e ⟺ n ≤ 2^{e + k} ⟺ e + k ≥ ceilLog2Nat n ⟺ e ≥ ceilLog2Nat n − k, so the least such e is ceilLog2Nat n − k. Both zero (value 0) and ofOdd n k with n ≤ 0 (value ≤ 0) are outside the x > 0 domain and return the junk value 0.

Equations

• Hex.ceilLog2Dyadic Dyadic.zero = 0
• Hex.ceilLog2Dyadic (Dyadic.ofOdd n k hn) = if n ≤ 0 then 0 else ↑(Hex.ceilLog2Nat n.toNat) - k

def Hex.rootBound (p : ZPoly) : Dyadic

A power of two strictly exceeding the Cauchy root bound 1 + max_{i < n} |aᵢ| / |aₙ|, so every real root of p lies in (−rootBound p, rootBound p]. Integer arithmetic only.

With c := |aₙ| the leading coefficient and A := max_{i < n} |aᵢ| the largest non-leading coefficient in absolute value, the result is twoPow (ceilLog2Nat (⌊A / c⌋ + 2)). Since 2^k ≥ ⌊A / c⌋ + 2 > 1 + A / c ≥ 1 + max |aᵢ| / |aₙ|, this power of two strictly exceeds the Cauchy bound. For deg p ≤ 0 there are no roots to bound and the placeholder value 1 is returned; no theorem reads it.

Equations

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

theorem Hex.rootBound_of_degree?_none {p : ZPoly} (h : DensePoly.degree? p = none) : rootBound p = Dyadic.ofInt 1

rootBound on a polynomial with no degree is the junk value 1.

theorem Hex.rootBound_of_degree?_zero {p : ZPoly} (h : DensePoly.degree? p = some 0) : rootBound p = Dyadic.ofInt 1

rootBound on a degree-zero polynomial is the junk value 1.

theorem Hex.rootBound_of_degree?_pos {p : ZPoly} {d : Nat} (h : DensePoly.degree? p = some (d + 1)) : rootBound p = twoPow ↑(ceilLog2Nat (List.foldl (fun (acc i : Nat) => max acc (DensePoly.coeff p i).natAbs) 0 (List.range (d + 1)) / (DensePoly.leadingCoeff p).natAbs + 2))

The defining equation of rootBound on a polynomial of positive degree.

def Hex.sepPrec (p : ZPoly) : Nat

Separation precision: for squarefree p of degree n ≥ 2, 2^{−sepPrec p} < sep(p) / 4, where sep(p) := min_{i ≠ j} |αᵢ − αⱼ| over the distinct complex roots. The contract is pairwise, hence vacuous for deg p ≤ 1, which is exactly when nothing needs the placeholder 0.

Derivation of the closed form (the companion's proof script). The Mahler separation bound (Mahler 1964) gives

  sep(p) ≥ √3 · n^{−(n+2)/2} · |disc p|^{1/2} · M(p)^{−(n−1)}.

For a squarefree integer polynomial disc p is a nonzero integer, so |disc p| ≥ 1, and √3 ≥ 1; dropping both factors keeps a lower bound. Landau's inequality bounds the Mahler measure M(p) ≤ ‖p‖₂ ≤ L, where L := coeffL2NormBound p is the conservative integer L2-norm bound from HexPolyZ.Mignotte. Hence

  sep(p) ≥ n^{−(n+2)/2} · L^{−(n−1)}
         = 2^{−((n+2)/2 · log₂ n + (n−1) · log₂ L)}.

Rounding each logarithm up: `⌈(n+2)/2 · log₂ n⌉ ≤ ⌈((n+2) · ⌈log₂ n⌉ +

1. / 2⌉, realised by the integer form ((n + 2) * ceilLog2Nat n + 1) / 2\(the+1before the halving makes the truncating division round the half-integer exponent up\), and(n−1) · log₂ L ≤ (n − 1) · ceilLog2Nat L. This yields sep(p) ≥ 2^{−(E)}` with

  E = ((n + 2) * ceilLog2Nat n + 1) / 2 + (n − 1) * ceilLog2Nat L.

Finally sepPrec p := E + 3, where +2 provides the /4 margin (2^{−(E+2)} = 2^{−E} / 4 ≤ sep(p) / 4) and +1 makes the inequality strict. Every rounding enlarges sepPrec, so the bound is conservative.

Equations

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

def Hex.depthSlack : Nat

The fixed slack added to the separation-driven bisection depth.

Equations

• Hex.depthSlack = 8

def Hex.isolationDepth (p : ZPoly) : Nat

The bisection depth at which both isolation engines stop: enough halvings to shrink the initial interval (−rootBound p, rootBound p] (width 2 · rootBound p) below 2^{−sepPrec p}, plus depthSlack.

For positive degree the depth is sepPrec p + (ceilLog2Dyadic (2 · rootBound p)).toNat + depthSlack. The .toNat is lossless: 2 · rootBound p ≥ 2 (a positive power of two doubled), so its ceiling logarithm is ≥ 1 > 0. For deg p ≤ 0, isolationDepth returns depthSlack; that branch is special-cased, since the junk rootBound value 1 would otherwise contribute a spurious ceilLog2Dyadic 2 = 1.

Equations

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