def Hex.DyadicSquare.subdivide (s : DyadicSquare) : Array DyadicSquare

The four children of s, one bit finer, in a fixed order (SW, SE, NW, NE). They partition s: each child has half-width 2^{−(prec+1)} and centre offset by that half-width from s's centre along each axis.

Equations

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

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

Edge-or-corner adjacency of two same-prec grid squares, by exact dyadic centre differences. Centres must be less than four half-widths apart on both axes. On a common subdivision grid the centre spacing is two half-widths, so this is exactly one king move; the geometric form also handles translated grids without a lattice-origin side condition.

Equations

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

def Hex.DyadicSquare.touches (s : DyadicSquare) (component : List DyadicSquare) : Bool

Whether a square touches some member of a partial glued component.

Equations

• s.touches component = component.any fun (t : Hex.DyadicSquare) => s.adjacent t || t.adjacent s

def Hex.glueInsert (s : DyadicSquare) (components : List (List DyadicSquare)) : List (List DyadicSquare)

Insert one square into a component partition. Every component touched by the new square is merged with it; untouched components retain their order.

Equations

• Hex.glueInsert s components = match List.partition s.touches components with | (touching, separate) => (s :: touching.flatten) :: separate

def Hex.glueList : List DyadicSquare → List (List DyadicSquare)

Edge-or-corner-connected components of a list of squares. This union-by-insertion form makes coverage, connectedness, and maximality structural induction invariants while retaining the O(m²) adjacency complexity.

Equations

• Hex.glueList [] = []
• Hex.glueList (s :: sqs) = Hex.glueInsert s (Hex.glueList sqs)

def Hex.glue (sqs : Array DyadicSquare) : Array (Array DyadicSquare)

Edge-or-corner-connected components of an array of squares.

Equations

• Hex.glue sqs = (List.map List.toArray (Hex.glueList sqs.toList)).toArray

def Hex.glueCovered (sqs : Array DyadicSquare) : Array (Array DyadicSquare)

Connected-component gluing with an executable coverage guard. The normal glue result is used when every input square occurs in an output component; the defensive fallback returns singleton components. The Mathlib companion proves the structural glueList implementation always passes this guard, so the fallback is unreachable in the current implementation.

Equations

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

def Hex.Component.refine1 (p : ZPoly) (c : Component) : Array Component

One subdivision round: split every square into four children one bit finer, discard children whose disc certifiably contains no root (the T₀ test; a child whose T₀ test fails to certify is kept, which is always sound), and glue the survivors into edge-or-corner-connected components. Total: no certification is required during refinement.

Equations

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

def Hex.Component.refineAll (p : ZPoly) (work : Array Component) : Array Component

One globally normalized subdivision round. All component squares are subdivided, filtered, and glued together. The root-count hint is reset to one; it affects attempt order only, and every candidate is rechecked.

The isolation driver uses this operation until its completeness depth. Thus all Cauchy-started survivors remain on one common grid, and components that approach the same root can rejoin even if an earlier round separated their lineages.

Equations

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

def Hex.Component.certifyPelletAtShift? (p : ZPoly) (c : Component) (shift : TaylorShift p (encSquare c.squares).center) (k : Nat) : Option (Certified p)

Attempt Pellet certification for one positive candidate count from the cached Taylor shift at the component's enclosing-square centre. The proof argument ties the cache to that centre; it is erased from compiled code.

Equations

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

def Hex.Component.certifyPelletSoft? (p : ZPoly) (c : Component) (shift : TaylorShift p (encSquare c.squares).center) (ks : List Nat) : Option (Certified p)

Build a certificate directly from the first all-count soft Graeffe candidate. The threshold keeps bounded-precision setup off the small-degree path where the exact dyadic kernel is already cheaper.

Equations

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

def Hex.Component.certifyPelletExactAt? (p : ZPoly) (c : Component) (shift : TaylorShift p (encSquare c.squares).center) (k : Nat) : Option (Certified p)

Exact cached-Taylor certification for one count, used after the all-count soft search has failed.

Equations

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

def Hex.Component.certifyPelletAt? (p : ZPoly) (c : Component) (k : Nat) : Option (Certified p)

Public one-count Pellet attempt. It computes the enclosing-centre Taylor shift once and passes it to the cached implementation.

Equations

• Hex.Component.certifyPelletAt? p c k = Hex.Component.certifyPelletAtShift? p c (Hex.TaylorShift.compute p (Hex.encSquare c.squares).center) k

def Hex.Component.certifyPelletExactList? (p : ZPoly) (c : Component) (shift : TaylorShift p (encSquare c.squares).center) : List Nat → Option (Certified p)

First exact Pellet certificate in a candidate-count list, reusing one enclosing-centre Taylor shift for every failed count.

Equations

• Hex.Component.certifyPelletExactList? p c shift [] = none
• Hex.Component.certifyPelletExactList? p c shift (k :: ks) = (Hex.Component.certifyPelletExactAt? p c shift k).orElse fun (x : Unit) => Hex.Component.certifyPelletExactList? p c shift ks

def Hex.Component.certifyPelletListShift? (p : ZPoly) (c : Component) (shift : TaylorShift p (encSquare c.squares).center) (ks : List Nat) : Option (Certified p)

First soft all-count certificate. On success, rerun its single selected count through the cached-shift certifier so the guarded Newton candidate is reused instead of returning the coarse soft base square. Failure falls back to the exact cached list.

Equations

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

def Hex.Component.certifyPelletList? (p : ZPoly) (c : Component) (ks : List Nat) : Option (Certified p)

Public candidate-count search. The exact Taylor shift is shared by every attempt; only a successful count's speculative candidate needs a new shift for its witness recheck.

Equations

• Hex.Component.certifyPelletList? p c ks = Hex.Component.certifyPelletListShift? p c (Hex.TaylorShift.compute p (Hex.encSquare c.squares).center) ks

def Hex.Component.certifyPelletShift? (p : ZPoly) (c : Component) (shift : TaylorShift p (encSquare c.squares).center) : Option (Certified p)

The Pellet half of component certification using a supplied shift.

Equations

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

def Hex.Component.certifyPellet? (p : ZPoly) (c : Component) : Option (Certified p)

The public Pellet half of component certification. This proof-facing compatibility surface computes its own shift; certify? supplies the already-cached shift to certifyPelletShift?.

Equations

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

def Hex.Component.certify? (p : ZPoly) (strategy : AtomStrategy := AtomStrategy.nkThenPellet) (c : Component) : Option (Certified p)

Try to certify the component. For Pellet-enabled strategies, run the all-count bounded-precision Graeffe filter before the exact candidate fallback. Share one exact shift between the Newton-Kantorovich atom witness and the exact Pellet fallback. Pellet uses a quadrupled enclosing square with k = candidateK first and then the remaining k ≤ deg p; a k = 1 Pellet success is returned as an atom via atomize. Speculative Newton results are accepted only under the coverage guard: the base region must certify the same count in the same certificate form, and the recentred certified region must be contained in the base one.

Equations

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