def Hex.ZPoly.spemStep (g r : ZPoly) : ZPoly

One reduction step of the sign-managed pseudo-remainder, applied to a remainder r with deg r ≥ deg g and g nonconstant.

Writing cg = lc g, lr = lc r, |cg| = if cg < 0 then -cg else cg, and sign(cg)·lr = if cg < 0 then -lr else lr, the step returns

scale |cg| r − scale (sign(cg)·lr) (shift (deg r − deg g) g).

The two leading terms are both at degree deg r, with coefficients |cg|·lr and sign(cg)·lr·cg = |cg|·lr, so they cancel exactly and the degree strictly drops. The multiplier introduced is |cg| > 0, so iterating multiplies the true rational remainder by a positive integer.

Engine internal, not user API: it is public (rather than private) only so the exposed spem/sturmChain closure the kernel-replay elaborator reduces can reference it. Callers want spem.

Equations

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

def Hex.ZPoly.spemAux (g : ZPoly) : Nat → ZPoly → ZPoly

The reduction loop for spem, driven by structural fuel.

Each iteration stops when the remainder is zero or has degree below deg g; otherwise it applies spemStep and recurses on one less fuel. Because every spemStep drops the degree by at least one, fuel = f.size = deg f + 1 at the top level is always sufficient and the fuel never truncates: the loop reaches a genuine stopping state (zero, or degree below deg g) before it runs out.

Engine internal, not user API: public only so the exposed spem/sturmChain closure the kernel-replay elaborator reduces can reference it. Callers want spem.

Equations

• g.spemAux 0 x✝ = x✝
• g.spemAux fuel.succ x✝ = if Hex.DensePoly.isZero x✝ = true then x✝ else if Hex.DensePoly.natDegree x✝ < Hex.DensePoly.natDegree g then x✝ else g.spemAux fuel (g.spemStep x✝)

def Hex.ZPoly.spem (f g : ZPoly) : ZPoly

The sign-managed pseudo-remainder of f by g.

The reduction loop repeatedly subtracts a shifted, scaled copy of g from f, each step multiplying by |lc g| (see spemStep), so the result is a positive integer multiple of the rational remainder f mod g. The accumulated multiplier is a product of |lc g| factors, hence positive; this differs from the conventional (lc g)^δ pseudo-remainder (with δ = deg f − deg g + 1, negated when (lc g)^δ < 0) only by a positive scalar, which the primitivePart in sturmChain erases. That is why the per-step |lc g| scheme has the same sign behavior.

Values outside the main positive-degree input:

• spem f 0 = f (the loop never starts: g has no degree).

• spem f g = 0 when g is a nonzero constant (a constant divides everything, so the remainder is 0).

• spem f g = f when deg f < deg g (the loop returns f on its first test).

Equations

• f.spem g = match Hex.DensePoly.degree? g with | none => f | some 0 => 0 | some val => g.spemAux (Hex.DensePoly.size f) f

def Hex.ZPoly.sturmChainAux : Nat → ZPoly → ZPoly → Array ZPoly → Array ZPoly

The chain-extension loop for sturmChain, driven by structural fuel.

Given the two most recent elements prev, cur and the accumulator acc, it computes r := spem prev cur; if r = 0 the chain is complete, otherwise it pushes next := −primitivePart r and recurses. primitivePart divides by the nonnegative content without sign-normalizing, so the explicit negation carries the required sign. The degree of cur strictly decreases along the recursion, so fuel = p.size at the top level never truncates.

Engine internal, not user API: public only so the exposed sturmChain closure the kernel-replay elaborator reduces can reference it. Callers want sturmChain.

Equations

• One or more equations did not get rendered due to their size.
• Hex.ZPoly.sturmChainAux 0 x✝² x✝¹ x✝ = x✝

def Hex.ZPoly.sturmChain (p : ZPoly) : Array ZPoly

The Sturm chain of p.

For deg p ≤ 0 the chain is empty (there is nothing to count). Otherwise s₀ = primitivePart p, s₁ = primitivePart p', and each further element is −primitivePart (spem sᵢ₋₁ sᵢ) while the pseudo-remainder is nonzero. Every element is a positive rational multiple of the classical signed-remainder chain of (p, p') over ℚ, the invariant the counting theorem needs. The last element is a nonzero constant exactly when p is squarefree of positive degree. The structural fuel p.size never truncates: the degree strictly decreases along the chain, so it terminates before the fuel is exhausted.

Equations

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

def Hex.ZPoly.hasSquarefreeSturmChain (p : ZPoly) : Bool

A decide-checkable squarefreeness certificate: p has positive degree and the last entry of its Sturm chain is a nonzero constant (size == 1). When this is true, p is squarefree over ℚ — proved as squareFreeRat_of_hasSquarefreeSturmChain in the Mathlib companion, whence a concrete SquareFreeRat p is dischargeable by by decide on this test.

This is a one-way certificate, not a decision procedure: it returns false on the zero polynomial and on nonzero constants (empty chain), even though SquareFreeRat is vacuously/trivially true there.

Equations

• p.hasSquarefreeSturmChain = match p.sturmChain.toList.getLast? with | some z => Hex.DensePoly.size z == 1 | none => false