def Hex.Dyadic.invFloor (x : Dyadic) (q : Int) : Dyadic

Floor of 1/x at precision q, for positive x: with x = n·2^{−k} (n odd positive), 1/x = 2^k/n, so the floor on the 2^{−q} grid is ⌊2^{q+k}/n⌋·2^{−q}, one integer division. This agrees with Dyadic.invAtPrec on positive arguments (both floor 1/x to the 2^{−q} grid, so 0 ≤ 1/x − result < 2^{−q}), but it kernel-reduces: invAtPrec routes through Rat normalisation, whose Nat.gcd well-founded recursion decide cannot unfold. Junk 0 on x ≤ 0 (and on q + k < 0, where the floor is 0 anyway since n ≥ 1).

Equations

• Hex.Dyadic.invFloor Dyadic.zero q = 0
• Hex.Dyadic.invFloor (Dyadic.ofOdd n k hn) q = if n < 0 then 0 else have e := q + k; if e < 0 then 0 else Dyadic.ofIntWithPrec (↑(2 ^ e.toNat) / n) q

theorem Hex.Dyadic.invFloor_eq_invAtPrec_of_pos {x : Dyadic} (hx : 0 < x) (q : Int) : invFloor x q = x.invAtPrec q

On positive inputs, the kernel-reducible reciprocal used by nkWitnessCheck agrees with the standard dyadic reciprocal.

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

The Newton-Kantorovich contraction check from an already-computed Taylor shift on the closed square s itself (sup norm), with r = 2^{−s.prec} the half-width. Requiring 2 ≤ cs.size with 0 < normSq c₁, it builds the exact reciprocal w = conj(c₁)·invFloor (normSq c₁) q (pinned precision q = 8 + max 0 (ceilLog2 (normSq c₁))), the residuals dₖ = w·cₖ, and the exact dyadic bounds y = lo(d₀), z₁ = hi(1 − d₁), and the radial Lipschitz bound z₂ = 2·Σ_{k=2}^{n} k·hi(dₖ)·ρ^{k−2} with ρ = s.radiusHi. It then returns the conjunction of the three strict exact-dyadic comparisons 0 < normSq c₁, y + z₁·r + z₂·r²/2 < r, and z₁ + z₂·r < 1.

Equations

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

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

The Newton-Kantorovich contraction check on the closed square s itself, using the exact Taylor shift of p at s.center.

Equations

• Hex.nkWitnessCheck p s = Hex.TaylorShift.nkWitnessCheck s (Hex.TaylorShift.compute p s.center)

theorem Hex.nkWitnessCheck_false {p : ZPoly} {s : DyadicSquare} (h : DensePoly.size p ≤ 1) : nkWitnessCheck p s = false

A Newton--Kantorovich witness needs the linear Taylor coefficient.

@[simp]

theorem Hex.TaylorShift.nkWitnessCheck_eq {p : ZPoly} (s : DyadicSquare) (shift : TaylorShift p s.center) : nkWitnessCheck s shift = Hex.nkWitnessCheck p s

The centre-indexed coefficient kernel is exactly the public polynomial Newton–Kantorovich check.

def Hex.nkWitness (p : ZPoly) (s : DyadicSquare) : Prop

Newton-Kantorovich contraction witness on the closed square s itself (sup norm), with r = 2^{−s.prec} the half-width and y, z₁, z₂ the exact dyadic bounds:

0 < normSq c₁ ∧ y + z₁·r + z₂·r²/2 < r ∧ z₁ + z₂·r < 1.

Implies (Mathlib companion): p has exactly one root in the closed square, it is simple, and it lies in the open square.

Equations

• Hex.nkWitness p s = (Hex.nkWitnessCheck p s = true)

@[instance_reducible]

instance Hex.instDecidableNkWitness {p : ZPoly} {s : DyadicSquare} : Decidable (nkWitness p s)

Equations

• Hex.instDecidableNkWitness = Hex.instDecidableNkWitness._aux_1

def Hex.atomWitness (p : ZPoly) (s : DyadicSquare) : Prop

An atom certificate: either certificate form for "exactly one simple root in the certified region". The two disjuncts certify different regions (the closed square for nkWitness, the circumscribed disc for the Pellet form); every consumer needs only the shared consequence that the root lies in the stored square's circumscribed disc.

Equations

• Hex.atomWitness p s = (Hex.nkWitness p s ∨ Hex.witness p s 1)

@[instance_reducible]

instance Hex.instDecidableAtomWitness {p : ZPoly} {s : DyadicSquare} : Decidable (atomWitness p s)

Equations

• Hex.instDecidableAtomWitness = Hex.instDecidableAtomWitness._aux_1

def Hex.ZPoly.negRoots (p : ZPoly) : ZPoly

Primitive positive-leading polynomial whose roots are the negatives of the roots of p. Primitive-part normalization precedes the exact X ↦ -X reflection so primitive inputs reduce directly to a parity sign change.

Equations

• p.negRoots = (Hex.ZPoly.dilate (-1) p.primitivePart).normalizePrimitiveSign

theorem Hex.ZPoly.negRoots_eq_reflect {p : ZPoly} (hprim : p.Primitive) : p.negRoots = (dilate (-1) p).normalizePrimitiveSign

On primitive input, root negation is just reflection followed by one leading-sign normalization.

@[simp]

theorem Hex.ZPoly.size_negRoots {p : ZPoly} (hprim : p.Primitive) : DensePoly.size p.negRoots = DensePoly.size p

Root negation preserves coefficient count on primitive input.

def Hex.DyadicSquare.neg (s : DyadicSquare) : DyadicSquare

Reflect a square through the origin.

Equations

• s.neg = { re := -s.re, im := -s.im, prec := s.prec }

inductive Hex.AtomCertificate (p : ZPoly) (s : DyadicSquare) : Type

Structural evidence that an atom is certified. Checker-produced atoms retain their original NK/Pellet form; exact reflection transports an existing certificate without re-running either checker.

• nk {p : ZPoly} {s : DyadicSquare} (h : nkWitness p s) : AtomCertificate p s
• pellet {p : ZPoly} {s : DyadicSquare} (h : witness p s 1) : AtomCertificate p s
• neg {p : ZPoly} {s : DyadicSquare} (hprim : p.Primitive) (certificate : AtomCertificate p s) : AtomCertificate p.negRoots s.neg
• normalize {p : ZPoly} {s : DyadicSquare} (certificate : AtomCertificate p s) : AtomCertificate p.normalizePrimitiveSign s

def Hex.AtomCertificate.ofWitness {p : ZPoly} {s : DyadicSquare} : atomWitness p s → AtomCertificate p s

Package either checker result as structural atom evidence.

Equations

• Hex.AtomCertificate.ofWitness h = if hnk : Hex.nkWitness p s then Hex.AtomCertificate.nk hnk else Hex.AtomCertificate.pellet ⋯

def Hex.AtomCertificate.isNK {p : ZPoly} {s : DyadicSquare} : AtomCertificate p s → Bool

Whether the certificate selects the closed square (NK) rather than the circumscribed disc (Pellet). Reflection preserves this region choice.

Equations

• (Hex.AtomCertificate.nk h).isNK = true
• (Hex.AtomCertificate.pellet h).isNK = false
• (Hex.AtomCertificate.neg hprim certificate).isNK = certificate.isNK
• certificate.normalize.isNK = certificate.isNK

inductive Hex.AtomStrategy : Type

Which atom certificates certify? attempts, and in which order. nkThenPellet is the default; the singleton strategies exist for the side-by-side comparison of the two atom forms.

• nk : AtomStrategy
• pellet : AtomStrategy
• nkThenPellet : AtomStrategy

@[instance_reducible]

instance Hex.instDecidableEqAtomStrategy : DecidableEq AtomStrategy

Equations

• Hex.instDecidableEqAtomStrategy x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Hex.instReprAtomStrategy.repr : AtomStrategy → Nat → Std.Format

Equations

• One or more equations did not get rendered due to their size.
• Hex.instReprAtomStrategy.repr Hex.AtomStrategy.nk prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Hex.AtomStrategy.nk")).group prec✝
• Hex.instReprAtomStrategy.repr Hex.AtomStrategy.pellet prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Hex.AtomStrategy.pellet")).group prec✝

@[instance_reducible]

instance Hex.instReprAtomStrategy : Repr AtomStrategy

Equations

• Hex.instReprAtomStrategy = { reprPrec := Hex.instReprAtomStrategy.repr }

structure Hex.DyadicRootIsolation (p : ZPoly) : Type

An atom: one square whose certified region (the square itself for the Newton-Kantorovich disjunct, the circumscribed disc for the Pellet disjunct) contains exactly one simple root.

• square : DyadicSquare

  The isolating square.

• witness : AtomCertificate p self.square

  An NK/Pellet atom certificate, possibly transported through reflection.

inductive Hex.Certified (p : ZPoly) : Type

The result of certifying one component: an atom (either atom certificate) or a k ≥ 1 Pellet cluster.

• atom {p : ZPoly} (iso : DyadicRootIsolation p) : Certified p

  Exactly one simple root, isolated as an atom.

• cluster {p : ZPoly} (cl : DyadicRootCluster p) : Certified p

  Exactly k roots with multiplicity, certified as a Pellet cluster.

def Hex.DyadicRootCluster.atomize {p : ZPoly} (c : DyadicRootCluster p) (h : c.k = 1) : DyadicRootIsolation p

Repackage a certified k = 1 cluster as an atom, taking the Pellet disjunct of atomWitness on the enclosing square. Total: the cluster's Pellet witness already certifies exactly one root in the enclosing disc.

Equations

• c.atomize h = { square := Hex.encSquare c.squares, witness := Hex.AtomCertificate.pellet ⋯ }

def Hex.certifyAtom? (p : ZPoly) (s : DyadicSquare) : Option (DyadicRootIsolation p)

Certify an arbitrary candidate square as an atom, deciding both atomWitness disjuncts fresh. This is the documented way to build a DyadicRootIsolation outside the drivers, e.g. after transforming an isolation's square (hex-number-field's inv? re-certification).

Equations

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