def Hex.softSqrt2Lo : Dyadic

The existing rational lower bound 181/128 < √2, duplicated here under a kernel-specific name so this module remains below Pellet in the import graph.

Equations

• Hex.softSqrt2Lo = Dyadic.ofIntWithPrec 181 7

def Hex.softSqrt2Hi : Dyadic

The existing rational upper bound √2 < 1449/1024.

Equations

• Hex.softSqrt2Hi = Dyadic.ofIntWithPrec 1449 10

structure Hex.CoeffBall : Type

A Gaussian dyadic centre with an L¹ error radius. The computational constructors below always produce a nonnegative radius; keeping that fact out of the structure leaves proof fields out of the hot path.

• center : GaussDyadic

  Rounded Gaussian-dyadic centre of the enclosure.

• radius : Dyadic

  Nonnegative L¹ error radius around center.

@[instance_reducible]

instance Hex.instDecidableEqCoeffBall : DecidableEq CoeffBall

Equations

• Hex.instDecidableEqCoeffBall = Hex.instDecidableEqCoeffBall.decEq

def Hex.instDecidableEqCoeffBall.decEq (x✝ x✝¹ : CoeffBall) : Decidable (x✝ = x✝¹)

Equations

• Hex.instDecidableEqCoeffBall.decEq { center := a, radius := a_1 } { center := b, radius := b_1 } = if h : a = b then h ▸ if h : a_1 = b_1 then h ▸ isTrue ⋯ else isFalse ⋯ else isFalse ⋯

def Hex.CoeffBall.zero : CoeffBall

The exact zero coefficient ball.

Equations

• Hex.CoeffBall.zero = { center := (0, 0), radius := 0 }

def Hex.CoeffBall.normOne (z : GaussDyadic) : Dyadic

|re z| + |im z|, an executable upper bound for the complex modulus.

Equations

• Hex.CoeffBall.normOne z = Hex.Dyadic.abs z.fst + Hex.Dyadic.abs z.snd

def Hex.CoeffBall.sigPrec (bits : Nat) (x : Dyadic) : Int

Signed endpoint precision retaining roughly bits significant binary digits.

Equations

• Hex.CoeffBall.sigPrec bits x = ↑bits - Hex.Dyadic.ceilLog2 (Hex.Dyadic.abs x)

def Hex.CoeffBall.roundRadius (bits : Nat) (x : Dyadic) : Dyadic

Round a nonnegative error bound upward while retaining about bits significant binary digits.

Equations

• Hex.CoeffBall.roundRadius bits x = x.roundUp (Hex.CoeffBall.sigPrec bits x)

def Hex.CoeffBall.normalize (bits : Nat) (z : GaussDyadic) (error : Dyadic) : CoeffBall

Round a Gaussian centre and add the exact L¹ displacement to an existing error bound.

Equations

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

def Hex.CoeffBall.point (bits : Nat) (z : GaussDyadic) : CoeffBall

A rounded ball enclosing one exact Gaussian dyadic.

Equations

• Hex.CoeffBall.point bits z = Hex.CoeffBall.normalize bits z 0

def Hex.CoeffBall.add (bits : Nat) (x y : CoeffBall) : CoeffBall

Outward-rounded sum.

Equations

• Hex.CoeffBall.add bits x y = Hex.CoeffBall.normalize bits (x.center.add y.center) (x.radius + y.radius)

def Hex.CoeffBall.sub (bits : Nat) (x y : CoeffBall) : CoeffBall

Outward-rounded difference.

Equations

• Hex.CoeffBall.sub bits x y = Hex.CoeffBall.normalize bits (x.center.sub y.center) (x.radius + y.radius)

def Hex.CoeffBall.mul (bits : Nat) (x y : CoeffBall) : CoeffBall

Outward-rounded product. The error formula is the standard L¹-submultiplicative bound |cx|₁·ey + |cy|₁·ex + ex·ey.

Equations

• Hex.CoeffBall.mul bits x y = Hex.CoeffBall.normalize bits (x.center.mul y.center) (Hex.CoeffBall.normOne x.center * y.radius + Hex.CoeffBall.normOne y.center * x.radius + x.radius * y.radius)

def Hex.CoeffBall.lo (x : CoeffBall) : Dyadic

Lower modulus bound: max(|re c|, |im c|) - error, clamped at zero.

Equations

• x.lo = Hex.Dyadic.max 0 (Hex.Dyadic.max (Hex.Dyadic.abs x.center.fst) (Hex.Dyadic.abs x.center.snd) - x.radius)

def Hex.CoeffBall.hi (x : CoeffBall) : Dyadic

Upper modulus bound from the centre's L¹ norm plus the error radius.

Equations

• x.hi = Hex.CoeffBall.normOne x.center + x.radius

def Hex.softTaylorStep (p : ZPoly) (c : GaussDyadic) (bits k : Nat) (acc : CoeffBall × CoeffBall) (r : Nat) : CoeffBall × CoeffBall

One step of the soft Taylor coefficient fold.

Equations

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

def Hex.softTaylorState (p : ZPoly) (c : GaussDyadic) (bits k n : Nat) : CoeffBall × CoeffBall

State after n terms of one soft Taylor coefficient.

Equations

• Hex.softTaylorState p c bits k n = List.foldl (Hex.softTaylorStep p c bits k) (Hex.CoeffBall.zero, Hex.CoeffBall.point bits (Hex.GaussDyadic.ofInt 1)) (List.range n)

def Hex.softTaylorCoeff (p : ZPoly) (c : GaussDyadic) (h : Dyadic) (bits k : Nat) : CoeffBall

One bounded-precision coefficient of p(c + hX). The Taylor sum carries the next power of c in its fold, so all coefficients together cost O(n²) ball operations rather than recomputing powers.

Equations

• Hex.softTaylorCoeff p c h bits k = Hex.CoeffBall.mul bits (Hex.softTaylorState p c bits k (Hex.DensePoly.size p - k)).fst (Hex.CoeffBall.point bits (h ^ k, 0))

def Hex.taylorBalls (p : ZPoly) (s : DyadicSquare) (bits : Nat) : Array CoeffBall

Coefficient balls for the locally scaled Taylor polynomial p(s.center + 2^(−s.prec) X).

Equations

• Hex.taylorBalls p s bits = Array.map (fun (k : Nat) => Hex.softTaylorCoeff p s.center (Dyadic.ofIntWithPrec 1 s.prec) bits k) (Array.range (Hex.DensePoly.size p))

def Hex.seededTaylorBalls (cs : Array GaussDyadic) (s : DyadicSquare) (bits : Nat) : Array CoeffBall

Rounded balls made from a supplied exact Taylor coefficient array.

Equations

• Hex.seededTaylorBalls cs s bits = Array.map (fun (k : Nat) => Hex.CoeffBall.point bits ((cs.getD k (0, 0)).mul (Dyadic.ofIntWithPrec 1 s.prec ^ k, 0))) (Array.range cs.size)

def Hex.exactTaylorBalls (p : ZPoly) (s : DyadicSquare) (bits : Nat) : Array CoeffBall

Rounded balls made from a freshly computed exact Taylor shift. This compatibility wrapper is used by proof-facing and standalone callers; cached certification paths pass their existing coefficients to seededTaylorBalls.

Equations

• Hex.exactTaylorBalls p s bits = Hex.seededTaylorBalls (Hex.taylor p s.center) s bits

def Hex.graeffeEven (bits : Nat) (cs : Array CoeffBall) (k : Nat) : CoeffBall

Even-even convolution contributing coefficient k of one Graeffe step.

Equations

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

def Hex.graeffeOdd (bits : Nat) (cs : Array CoeffBall) (k : Nat) : CoeffBall

Odd-odd convolution contributing the shifted coefficient k+1 of one Graeffe step.

Equations

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

def Hex.graeffe (bits : Nat) (cs : Array CoeffBall) : Array CoeffBall

One outward-rounded Graeffe step. The output retains the input array size; out-of-range convolution terms are exact zero balls.

Equations

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

@[simp]

theorem Hex.graeffe_size (bits : Nat) (cs : Array CoeffBall) : (graeffe bits cs).size = cs.size

A Graeffe step preserves the number of stored coefficients.

def Hex.softPelletAt (cs : Array CoeffBall) (k : Nat) (rlo rhi : Dyadic) : Bool

One Pellet comparison on coefficient balls. The lower bound of the selected coefficient is compared with upper bounds for every other coefficient.

Equations

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

def Hex.graeffeRounds (degree : Nat) : Nat

BSSY's number of Graeffe rounds. The nested logarithm is tiny (at most nine rounds through degree 255), while the added five rounds give their fixed isolation-ratio constants.

Equations

• Hex.graeffeRounds degree = Hex.ceilLog2 (1 + Hex.ceilLog2 (Nat.max 2 degree)) + 5

structure Hex.SoftRadii : Type

The three radius intervals transported together through Graeffe iteration. All six endpoints are stored explicitly because every radius, not merely the base radius, must be squared after roots are squared.

• baseLo : Dyadic

  Lower endpoint for the base-radius interval.

• baseHi : Dyadic

  Upper endpoint for the base-radius interval.

• twoLo : Dyadic

  Lower endpoint for the doubled-radius interval.

• twoHi : Dyadic

  Upper endpoint for the doubled-radius interval.

• fourLo : Dyadic

  Lower endpoint for the quadrupled-radius interval.

• fourHi : Dyadic

  Upper endpoint for the quadrupled-radius interval.

@[instance_reducible]

instance Hex.instDecidableEqSoftRadii : DecidableEq SoftRadii

Equations

• Hex.instDecidableEqSoftRadii = Hex.instDecidableEqSoftRadii.decEq

def Hex.instDecidableEqSoftRadii.decEq (x✝ x✝¹ : SoftRadii) : Decidable (x✝ = x✝¹)

Equations

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

def Hex.SoftRadii.initial : SoftRadii

Initial local-coordinate bounds for √2, 2√2, and 4√2.

Equations

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

def Hex.SoftRadii.square (rs : SoftRadii) : SoftRadii

Transport all three radius intervals through one root-squaring step.

Equations

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

def Hex.softPelletThree (cs : Array CoeffBall) (k : Nat) (rs : SoftRadii) : Bool

Check the three transported Pellet radii at this Graeffe level.

Equations

• Hex.softPelletThree cs k rs = (Hex.softPelletAt cs k rs.baseLo rs.baseHi && Hex.softPelletAt cs k rs.twoLo rs.twoHi && Hex.softPelletAt cs k rs.fourLo rs.fourHi)

def Hex.softGraeffeLoop (bits k : Nat) : Nat → Array CoeffBall → SoftRadii → Bool

Try the initial locally scaled Taylor polynomial and every Graeffe level through rounds. Squaring the radius bounds in lockstep matches the root squaring transformation.

Equations

• Hex.softGraeffeLoop bits k 0 x✝¹ x✝ = Hex.softPelletThree x✝¹ k x✝
• Hex.softGraeffeLoop bits k rounds.succ x✝¹ x✝ = (Hex.softPelletThree x✝¹ k x✝ || Hex.softGraeffeLoop bits k rounds (Hex.graeffe bits x✝¹) x✝.square)

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

One working-precision attempt at the three-radius soft Graeffe witness.

Equations

• Hex.softWitnessAt p s k bits = Hex.softGraeffeLoop bits k (Hex.graeffeRounds (Hex.DensePoly.natDegree p)) (Hex.taylorBalls p s bits) Hex.SoftRadii.initial

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

Three-radius Graeffe witness seeded from one exact Taylor shift. This is the tighter and cheaper shallow-centre variant.

Equations

• Hex.softSeededWitness p s k bits = Hex.softGraeffeLoop bits k (Hex.graeffeRounds (Hex.DensePoly.natDegree p)) (Hex.exactTaylorBalls p s bits) Hex.SoftRadii.initial

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

Three-radius exact-seeded witness reusing an existing Taylor shift.

Equations

• Hex.TaylorShift.softSeededWitness s shift k bits = Hex.softGraeffeLoop bits k (Hex.graeffeRounds (Hex.DensePoly.natDegree p)) (Hex.seededTaylorBalls shift.coeffs s bits) Hex.SoftRadii.initial

theorem Hex.TaylorShift.softSeededWitness_eq {p : ZPoly} (s : DyadicSquare) (shift : TaylorShift p s.center) (k bits : Nat) : softSeededWitness s shift k bits = Hex.softSeededWitness p s k bits

A valid cached shift gives the standalone exact-seeded witness.

def Hex.softPrecisions : List Nat

Working precisions tried by the soft filter. Failure at all tiers is not negative evidence: callers retain the exact Pellet fallback.

Equations

• Hex.softPrecisions = [64, 128, 256]

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

Adaptive soft Graeffe witness reusing an existing exact shift on the shallow seeded route.

Equations

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

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

Adaptive soft Graeffe witness. Standalone callers compute the shallow exact seed once; cached certifiers use TaylorShift.softWitnessCheck.

Equations

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

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

No soft root-count witness can select a coefficient outside the polynomial's coefficient array.

theorem Hex.TaylorShift.softWitnessCheck_eq {p : ZPoly} (s : DyadicSquare) (shift : TaylorShift p s.center) (k : Nat) : softWitnessCheck s shift k = Hex.softWitnessCheck p s k

Any valid cached shift gives the same adaptive soft witness as the public standalone wrapper.

def Hex.firstSoftCandidate? (cs : Array CoeffBall) (rs : SoftRadii) : List Nat → Option Nat

First positive root count whose three-radius comparison succeeds at one Graeffe level.

Equations

• Hex.firstSoftCandidate? cs rs [] = none
• Hex.firstSoftCandidate? cs rs (k :: ks) = if (decide (0 < k) && Hex.softPelletThree cs k rs) = true then some k else Hex.firstSoftCandidate? cs rs ks

def Hex.softCandidateLoop (bits : Nat) (ks : List Nat) : Nat → Array CoeffBall → SoftRadii → Option Nat

Scan all candidate counts at each Graeffe level before transforming the coefficient array once.

Equations

• One or more equations did not get rendered due to their size.
• Hex.softCandidateLoop bits ks 0 x✝¹ x✝ = Hex.firstSoftCandidate? x✝¹ x✝ ks

def Hex.softCandidateAt? (p : ZPoly) (s : DyadicSquare) (ks : List Nat) (bits : Nat) : Option Nat

One working-precision all-count candidate search.

Equations

• Hex.softCandidateAt? p s ks bits = Hex.softCandidateLoop bits ks (Hex.graeffeRounds (Hex.DensePoly.natDegree p)) (Hex.taylorBalls p s bits) Hex.SoftRadii.initial

def Hex.softSeededCandidate? (p : ZPoly) (s : DyadicSquare) (ks : List Nat) (bits : Nat) : Option Nat

One-precision all-count candidate search seeded from an exact Taylor shift.

Equations

• Hex.softSeededCandidate? p s ks bits = Hex.softCandidateLoop bits ks (Hex.graeffeRounds (Hex.DensePoly.natDegree p)) (Hex.exactTaylorBalls p s bits) Hex.SoftRadii.initial

def Hex.TaylorShift.softSeededCandidate? {p : ZPoly} (s : DyadicSquare) (shift : TaylorShift p s.center) (ks : List Nat) (bits : Nat) : Option Nat

One-precision all-count candidate search reusing an existing exact Taylor shift for its coefficient balls.

Equations

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

def Hex.softCandidateAdaptive? (p : ZPoly) (s : DyadicSquare) (ks : List Nat) : List Nat → Option Nat

Try an all-count candidate search at each working precision.

Equations

• Hex.softCandidateAdaptive? p s ks [] = none
• Hex.softCandidateAdaptive? p s ks (k :: ks_1) = (Hex.softCandidateAt? p s ks k).orElse fun (x : Unit) => Hex.softCandidateAdaptive? p s ks ks_1

def Hex.softCandidate? (p : ZPoly) (s : DyadicSquare) (ks : List Nat) : Option Nat

Adaptive all-count soft Graeffe search.

Equations

• Hex.softCandidate? p s ks = Hex.softCandidateAdaptive? p s ks Hex.softPrecisions

def Hex.TaylorShift.softRefinementCandidate? {p : ZPoly} (s : DyadicSquare) (shift : TaylorShift p s.center) (ks : List Nat) : Option Nat

Certification search tuned for subdivision and reusing its cached exact shift: one seeded 64-bit pass while exact centres are still cheap, then the fully soft ladder once centre bit-length reaches 32.

Equations

• Hex.TaylorShift.softRefinementCandidate? s shift ks = if s.prec < 32 then Hex.TaylorShift.softSeededCandidate? s shift ks 64 else Hex.softCandidate? p s ks

def Hex.softRefinementCandidate? (p : ZPoly) (s : DyadicSquare) (ks : List Nat) : Option Nat

Standalone refinement candidate search. Cached certifiers call the TaylorShift method directly.

Equations

• Hex.softRefinementCandidate? p s ks = Hex.TaylorShift.softRefinementCandidate? s (Hex.TaylorShift.compute p s.center) ks

theorem Hex.TaylorShift.softRefinementCandidate?_eq {p : ZPoly} (s : DyadicSquare) (shift : TaylorShift p s.center) (ks : List Nat) : softRefinementCandidate? s shift ks = Hex.softRefinementCandidate? p s ks

A valid cached shift gives the public standalone candidate result.

def Hex.firstSoftRootCount? (cs : Array CoeffBall) (rlo rhi : Dyadic) : List Nat → Option Nat

First candidate count at one base radius. Unlike firstSoftCandidate?, this includes k = 0, so callers can distinguish a certified discard from a certified positive root count.

Equations

• Hex.firstSoftRootCount? cs rlo rhi [] = none
• Hex.firstSoftRootCount? cs rlo rhi (k :: ks) = if Hex.softPelletAt cs k rlo rhi = true then some k else Hex.firstSoftRootCount? cs rlo rhi ks

def Hex.softRootCountLoop (bits : Nat) (ks : List Nat) : Nat → Array CoeffBall → Dyadic → Dyadic → Option Nat

Search all requested root counts at the base radius, reusing each Graeffe transform for the whole list.

Equations

• One or more equations did not get rendered due to their size.
• Hex.softRootCountLoop bits ks 0 x✝² x✝¹ x✝ = Hex.firstSoftRootCount? x✝² x✝¹ x✝ ks

def Hex.softSeededRootCount? (p : ZPoly) (s : DyadicSquare) (ks : List Nat) (bits : Nat) : Option Nat

Base-radius all-count filter seeded by one exact Taylor shift.

Equations

• Hex.softSeededRootCount? p s ks bits = Hex.softRootCountLoop bits ks (Hex.graeffeRounds (Hex.DensePoly.natDegree p)) (Hex.exactTaylorBalls p s bits) Hex.softSqrt2Lo Hex.softSqrt2Hi

theorem Hex.firstSoftCandidate?_sound {cs : Array CoeffBall} {rs : SoftRadii} {ks : List Nat} {k : Nat} (h : firstSoftCandidate? cs rs ks = some k) : 0 < k ∧ softPelletThree cs k rs = true

A returned first-level candidate is positive and passes its comparison.

theorem Hex.softCandidateLoop_sound {bits : Nat} {ks : List Nat} {rounds : Nat} {cs : Array CoeffBall} {rs : SoftRadii} {k : Nat} (h : softCandidateLoop bits ks rounds cs rs = some k) : 0 < k ∧ softGraeffeLoop bits k rounds cs rs = true

An all-count loop result is also a successful per-count loop result.

theorem Hex.softCandidateAt?_sound {p : ZPoly} {s : DyadicSquare} {ks : List Nat} {bits k : Nat} (h : softCandidateAt? p s ks bits = some k) : 0 < k ∧ softWitnessAt p s k bits = true

One-precision candidate search implies the ordinary witness check at that precision.

theorem Hex.softSeededCandidate?_sound {p : ZPoly} {s : DyadicSquare} {ks : List Nat} {bits k : Nat} (h : softSeededCandidate? p s ks bits = some k) : 0 < k ∧ softSeededWitness p s k bits = true

An exact-seeded candidate is accepted by its exact-seeded per-count witness.

theorem Hex.softCandidate?_sound {p : ZPoly} {s : DyadicSquare} {ks : List Nat} {k : Nat} (h : softCandidate? p s ks = some k) : 0 < k ∧ softWitnessCheck p s k = true

The adaptive all-count search returns only a positive count accepted by the public per-count soft witness.

theorem Hex.softRefinementCandidate?_sound {p : ZPoly} {s : DyadicSquare} {ks : List Nat} {k : Nat} (h : softRefinementCandidate? p s ks = some k) : 0 < k ∧ softWitnessCheck p s k = true

The depth-aware candidate search still returns an ordinary public soft witness.

def Hex.softRootFreeLoop (bits : Nat) : Nat → Array CoeffBall → Dyadic → Dyadic → Bool

Base-radius T₀ comparison at the initial level and every Graeffe level. Unlike the three-radius atom witness, exclusion needs only the square's circumscribed disc.

Equations

• Hex.softRootFreeLoop bits 0 x✝² x✝¹ x✝ = Hex.softPelletAt x✝² 0 x✝¹ x✝
• Hex.softRootFreeLoop bits rounds.succ x✝² x✝¹ x✝ = (Hex.softPelletAt x✝² 0 x✝¹ x✝ || Hex.softRootFreeLoop bits rounds (Hex.graeffe bits x✝²) (x✝¹ * x✝¹) (x✝ * x✝))

def Hex.softRootFreeAt (p : ZPoly) (s : DyadicSquare) (bits : Nat) : Bool

Soft single-radius Graeffe T₀ filter for subdivision.

Equations

• Hex.softRootFreeAt p s bits = Hex.softRootFreeLoop bits (Hex.graeffeRounds (Hex.DensePoly.natDegree p)) (Hex.taylorBalls p s bits) Hex.softSqrt2Lo Hex.softSqrt2Hi

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

Adaptive soft T₀ discard.

Equations

• Hex.softRootFree p s = Hex.softPrecisions.any fun (bits : Nat) => Hex.softRootFreeAt p s bits