def Hex.ZPoly.coeffAbsMax (p : ZPoly) : Nat

‖p‖∞: the maximum absolute value of the coefficients of p, i.e. max_i |pᵢ|. Folds Nat.max over Int.natAbs of the stored coefficients; the zero polynomial has none, so it returns 0.

Equations

• p.coeffAbsMax = List.foldl (fun (acc i : Nat) => acc.max (Hex.DensePoly.coeff p i).natAbs) 0 (List.range (Hex.DensePoly.size p))

@[simp]

theorem Hex.ZPoly.coeffAbsMax_dilate_neg_one (p : ZPoly) : (dilate (-1) p).coeffAbsMax = p.coeffAbsMax

Reflection in the origin preserves coefficient height.

@[simp]

theorem Hex.ZPoly.coeffAbsMax_scale_neg_one (p : ZPoly) : coeffAbsMax (DensePoly.scale (-1) p) = p.coeffAbsMax

Multiplication by -1 preserves coefficient height.

@[simp]

theorem Hex.ZPoly.coeffAbsMax_normalizePrimitiveSign (p : ZPoly) : p.normalizePrimitiveSign.coeffAbsMax = p.coeffAbsMax

Primitive sign normalization preserves coefficient height.

def Hex.mahlerPrec (p : ZPoly) : Nat

Precision at which the circumscribed-disc radius 2^{−m}·√2 is strictly below sep(p)/4 (derivation in the module docstring). Pure integer arithmetic in O(n · log ‖p‖∞).

On degenerate inputs the Nat subtractions n − 1 truncate to 0 and ceilLog2's junk-0 branch handles n ≤ 1 and a = 0, so the value is a small harmless total (3 for n ≤ 1).

Equations

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

def Hex.sepSlack : Nat

The fixed slack added to mahlerPrec in separationDepth: one level for the factor-2 witness slack, at most two for the enclosing square of a multi-square component, one for the circumscribed √2, and margin.

Equations

• Hex.sepSlack = 8

def Hex.separationDepth (p : ZPoly) : Nat

Depth at which the completeness analysis says every Pellet witness certifies. Past mahlerPrec p each component's disc contains at most one distinct root; the ceilLog2 (max 2 (deg p)) term buys the degree-dependent isolation ratio the witness needs (one doubling per level), and sepSlack covers the fixed factors. It is the depth bound used by stopDepth.

Equations

• Hex.separationDepth p = Hex.mahlerPrec p + Hex.ceilLog2 (Nat.max 2 (Hex.DensePoly.natDegree p)) + Hex.sepSlack