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.hornerDyadic (n e c : Int) (acc : Int × Int) : Int × Int

One Horner operation on an unnormalized numerator and binary precision. The pair (a, k) represents a * 2^(-k). Zero accumulators discard the precision, so constants and exact cancellations do not shift by an unused endpoint exponent. Zero coefficients retain the signed precision without materializing powers of two, including at enormous integral endpoints.

Equations

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

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.

At integer points, the array fold carries an integer numerator and binary precision, normalizing only the final result. At fractional points, ordinary dyadic arithmetic normalizes intermediate values to avoid accumulating cancellable powers of two. Coefficients are stored in ascending degree order.

Equations

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