def Hex.mobiusTransform (p : ZPoly) (I : DyadicInterval) : ZPoly

The integer Möbius transform of p relative to (a, b]: the numerator of (1 + x)^{deg p} · p((a + bx)/(1 + x)) after clearing the dyadic denominators (a positive power of two). Its positive real roots correspond bijectively, with multiplicity, to the real roots of p in the open interval (a, b).

The pipeline, with n = deg p fixed up front and (α, β, s) from mobiusEndpoints (so a = α·2^{-s}, b = β·2^{-s}):

• (b) clear the dyadic denominator. Replace x by x·2^{-s}, i.e. form 2^{s·n}·p(x·2^{-s}): coefficient aᵢ ↦ aᵢ·2^{s·(n−i)}. This scales every root by 2^s, so the interval becomes (α, β] with integer endpoints.

• (c) Taylor shift the right endpoint to the origin. q ↦ q(x + β) via compose with the degree-one argument x + β; a root y of the cleared polynomial becomes y − β, so the interval's roots now lie in [α−β, 0).

• (d) rescale to (0, 1]. dilate (α−β) evaluates at (α−β)·x (a negative dilation), sending a root y − β to u = (β−y)/(β−α), so roots in (α, β) map to (0, 1) with y = α ↦ u = 1 and y = β ↦ u = 0.

• (e) reverse at the original degree n. Build the coefficient array of length n+1 with entry i equal to coeff (n − i) and renormalize; this is the x ↦ 1/x homogenization (1+x)^{deg p}, sending (0, 1) to (1, ∞). Reversing at n rather than the current degree is essential: when p(b) = 0 with multiplicity m, the m lowest coefficients after (c)/(d) vanish; the reversal turns them into trailing zeros, which ofCoeffs trims, dropping the degree by m. Those roots correctly disappear (their image under x ↦ 1/x is ∞ — a root at b is not in the open (a, b)).

• (f) shift back to the positive axis. r ↦ r(x + 1) via compose, sending (1, ∞) to (0, ∞). Chasing the maps: a root x₀ of p corresponds to the final root t with x₀ = (a + b·t)/(1 + t) — the required Möbius map, with t > 0 ⟺ x₀ ∈ (a, b). A root at a lands at t = 0 (a vanishing constant term, not a positive root), a root at b disappears at ∞ via the degree drop in (e), so the positive real roots of the result are exactly the images of p's roots in the open (a, b), with multiplicity.

No content/primitivePart division is taken anywhere: sign variations are scale-invariant, so a content gcd would be pure cost against the O(n²) per-node budget.

For deg p ≤ 0 (p constant or zero) there is no interval structure to transform; p is returned unchanged as a documented junk value (no theorem reads it).

Equations

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

def Hex.descartesVar (p : ZPoly) : Nat

Sign variations of the coefficient list: the Descartes bound. Each stored coefficient is reduced to its exact sign in {−1, 0, 1} and the resulting list is fed to signVar (zero-skipping sign-variation count).

Equations

• Hex.descartesVar p = Hex.signVar (List.map Int.sign (Hex.DensePoly.toArray p).toList)