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

Speculative Newton step from already-computed Taylor coefficients. The caller is responsible for supplying the shift at s.center; this kernel exists so certification can reuse the shift that established its base witness.

Equations

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

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

Speculative Newton step x' = x − k·c₀/c₁ from the centre of s, returning the recentred, much smaller square at prec' = max (s.prec + 2) (2·s.prec). k = 1 is the atom form; general k is the k-order cluster step (BSSY §5). Purely speculative: the caller must re-certify and apply the coverage guard. Degree < 1 (cs.size < 2) returns s unchanged; c₁ = 0 gives 1/|c₁|² = 0, so the centre is returned unchanged (x' = x) at the finer prec'. Either way the degenerate result is rejected by the re-check.

Equations

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

@[simp]

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

The centre-indexed coefficient kernel is exactly the public polynomial Newton step.

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

The square concentric with s, one level coarser (half-width doubled). The Newton-Kantorovich certification convention tests and stores this.

Equations

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