structure Hex.DyadicInterval : Type

A half-open dyadic interval (lower, upper].

The isolation convention throughout the library is half-open on the left: a root at upper belongs to the interval, a root at lower does not. This is what makes bisection at a midpoint have no endpoint case analysis — a root exactly at the midpoint m lands in the left child (lower, m]. The lt field records that the interval is nonempty.

• lower : Dyadic

  The excluded left endpoint.

• upper : Dyadic

  The included right endpoint.

• lt : self.lower < self.upper

  The interval is nonempty: lower < upper.

def Hex.DyadicInterval.midpoint (I : DyadicInterval) : Dyadic

The dyadic midpoint (lower + upper) / 2 of the interval, computed by an exact arithmetic right shift of the sum by one bit.

Equations

• I.midpoint = (I.lower + I.upper) >>> 1

def Hex.DyadicInterval.width (I : DyadicInterval) : Dyadic

The exact width upper - lower of the interval.

Equations

• I.width = I.upper - I.lower

def Hex.dyadicSign : Dyadic → Int

The exact sign of a dyadic value as an integer in {-1, 0, 1}.

A nonzero dyadic is ofOdd n k with n odd, and its sign is the sign of the odd numerator n (the power-of-two scale 2^{-k} is positive), so no evaluation is needed.

Equations

• Hex.dyadicSign Dyadic.zero = 0
• Hex.dyadicSign (Dyadic.ofOdd n k hn) = if n < 0 then -1 else 1

def Hex.ZPoly.evalDyadic (p : ZPoly) (x : Dyadic) : Dyadic

Evaluate an integer polynomial at a dyadic point by Horner's rule, returning an exact Dyadic value.

This is exact witness arithmetic: a plain fold over the coefficient array with no rounding, so the sign of p(x) at a dyadic x is exact. Coefficients are stored in ascending degree order, so folding from the right accumulates c₀ + x·(c₁ + x·(⋯ + x·cₙ)).

Equations

• p.evalDyadic x = Array.foldr (fun (c : Int) (acc : Dyadic) => Dyadic.ofInt c + x * acc) 0 (Hex.DensePoly.toArray p)