Fixed-precision dyadic interval-arithmetic kernel (Ival, IntervalGS): closed integer-mantissa intervals at a shared power-of-two scale, used by the enclosure reducedness checker. Mathlib-free; no floating point.

Fixed-precision dyadic interval kernel

The certified-dispatch reducedness clause is decided first by a sound enclosure pass at fixed working precision; only on indecision does it fall back to the exact integer checker. The kernel below is the Mathlib-free executable surface: closed dyadic intervals whose endpoints are Int mantissas at a shared power-of-two scale. Per-operation containment lemmas and the composed soundness theorem (lllReducedInterval_sound) live in HexLLLMathlib.

structure Hex.Internal.Ival : Type

Closed dyadic interval [lo / S, hi / S] whose endpoints are integer mantissas at a shared power-of-two scale S = 2 ^ prec. The scale is not stored; every operation that rounds takes S explicitly, so the working precision stays a parameter of the checker.

• lo : Int
• hi : Int

def Hex.Internal.instReprIval.repr : Ival → Nat → Std.Format

Equations

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

@[implicit_reducible]

instance Hex.Internal.instReprIval : Repr Ival

Equations

• Hex.Internal.instReprIval = { reprPrec := Hex.Internal.instReprIval.repr }

def Hex.Internal.instBEqIval.beq : Ival → Ival → Bool

Equations

• Hex.Internal.instBEqIval.beq { lo := a, hi := a_1 } { lo := b, hi := b_1 } = (a == b && a_1 == b_1)
• Hex.Internal.instBEqIval.beq x✝¹ x✝ = false

@[implicit_reducible]

instance Hex.Internal.instBEqIval : BEq Ival

Equations

• Hex.Internal.instBEqIval = { beq := Hex.Internal.instBEqIval.beq }

@[implicit_reducible]

instance Hex.Internal.instInhabitedIval : Inhabited Ival

Equations

• Hex.Internal.instInhabitedIval = { default := Hex.Internal.instInhabitedIval.default }

def Hex.Internal.Ival.mem (S : Int) (I : Ival) (x : Rat) : Prop

The rational x lies in the dyadic interval I read at scale S.

Equations

• Hex.Internal.Ival.mem S I x = (↑I.lo ≤ x * ↑S ∧ x * ↑S ≤ ↑I.hi)

def Hex.Internal.Ival.ofInt (S z : Int) : Ival

Exact embedding of an integer at scale S.

Equations

• Hex.Internal.Ival.ofInt S z = { lo := z * S, hi := z * S }

def Hex.Internal.Ival.cdiv (a b : Int) : Int

Ceiling division for a positive divisor, via Int.fdiv of the negated dividend.

Equations

• Hex.Internal.Ival.cdiv a b = -(-a).fdiv b

def Hex.Internal.Ival.ofRat (S : Int) (q : Rat) : Ival

One-ulp enclosure of a rational at scale S.

Equations

• Hex.Internal.Ival.ofRat S q = { lo := (q.num * S).fdiv ↑q.den, hi := Hex.Internal.Ival.cdiv (q.num * S) ↑q.den }

def Hex.Internal.Ival.add (a b : Ival) : Ival

Interval addition. Fixed-point addition is exact: no rounding.

Equations

• a.add b = { lo := a.lo + b.lo, hi := a.hi + b.hi }

def Hex.Internal.Ival.sub (a b : Ival) : Ival

Interval subtraction. Exact, like add.

Equations

• a.sub b = { lo := a.lo - b.hi, hi := a.hi - b.lo }

def Hex.Internal.Ival.mul (S : Int) (a b : Ival) : Ival

Interval multiplication. Endpoint products land at scale S², so the result rounds outward through one floor / ceiling division by S.

Equations

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

def Hex.Internal.Ival.divPos (S : Int) (a b : Ival) : Ival

Interval division by an interval the caller has checked to be strictly positive (0 < b.lo). The numerator rescales by S so the quotient lands back at scale S. Well-defined but junk when the positivity precondition fails; the containment lemma is conditional on it.

Equations

• Hex.Internal.Ival.divPos S a b = { lo := min ((a.lo * S).fdiv b.lo) ((a.lo * S).fdiv b.hi), hi := max (Hex.Internal.Ival.cdiv (a.hi * S) b.lo) (Hex.Internal.Ival.cdiv (a.hi * S) b.hi) }

@[inline]

def Hex.Internal.Ival.prodBounds (a b : Ival) : Int × Int

Endpoint bounds of the product of two intervals, sign-cased so the common (sign-definite) cases cost two integer multiplications instead of four products plus comparisons. Returns (lo, hi) at the product scale of its inputs.

Equations

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

def Hex.Internal.IntervalGS.dotStep (S : Int) (mu r : Array Ival) (g : Int) (t : Nat) : Ival

One step of the Gram-Schmidt dot recurrence on enclosures: g − Σ_{k < t} mu[k] · r[k], with g an exact Gram entry. With mu = μ[j][·] and r = r[i][·] this encloses ⟨b_i, b*_j⟩; with mu = r = row i's own data it encloses ‖b*_i‖².

The sum accumulates exactly at scale S² (endpoint products of scale-S mantissas) and rounds outward through a single floor / ceiling division at the end, so a length-t dot recurrence costs one rounding division rather than t of them.

Equations

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

@[inline]

def Hex.Internal.IntervalGS.rowStep (S : Int) (gRow : Array Int) (mus : Array (Array Ival)) (bstars : Array Ival) (acc : Array Ival × Array Ival) (j : Nat) : Array Ival × Array Ival

One column step of the per-row fold: extend the r row with the enclosure of ⟨b_i, b*_j⟩ and the μ row with the enclosure of μ[i][j] = ⟨b_i, b*_j⟩ / ‖b*_j‖².

Equations

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

def Hex.Internal.IntervalGS.row (S : Int) (gRow : Array Int) (mus : Array (Array Ival)) (bstars : Array Ival) (i : Nat) : Array Ival × Ival

Enclosure pass for one basis row: from the exact Gram row gRow and the enclosure rows of all earlier indices, produce the μ[i][·] enclosure row and the ‖b*_i‖² enclosure. The intermediate r row encloses the dot products ⟨b_i, b*_j⟩.

Equations

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

@[inline]

def Hex.Internal.IntervalGS.passStep (S : Int) (g : Array (Array Int)) (acc : Array (Array Ival) × Array Ival) (i : Nat) : Option (Array (Array Ival) × Array Ival)

One row step of the pass fold: run row, demand a strictly positive norm enclosure, and extend the accumulated enclosure state.

Equations

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

def Hex.Internal.IntervalGS.pass (S : Int) (g : Array (Array Int)) (n : Nat) : Option (Array (Array Ival) × Array Ival)

Full interval Gram-Schmidt pass over the exact n × n Gram matrix: O(n³) interval operations on fixed-scale mantissas, independent of the Gram-determinant bit growth of the input family. Returns the enclosure rows of the Gram-Schmidt coefficients and the squared basis norms, or none as soon as some norm enclosure fails strict positivity (the division by that norm would be unsound, and reducedness could not be decided either way).

Equations

• Hex.Internal.IntervalGS.pass S g n = List.foldlM (Hex.Internal.IntervalGS.passStep S g) (#[], #[]) (List.range n)

def Hex.Internal.IntervalGS.sizeOK (S : Int) (η : Rat) (mus : Array (Array Ival)) (n : Nat) : Bool

Size-reduction clause on enclosures: every μ[i][j] interval lies inside [−η, η], compared exactly through η = η.num / η.den.

Equations

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

def Hex.Internal.IntervalGS.lovaszOK (S : Int) (δ : Rat) (mus : Array (Array Ival)) (bstars : Array Ival) (n : Nat) : Bool

Lovász clause on enclosures at every adjacent pair: the largest possible δ‖b*_i‖² is at most the smallest possible ‖b*_{i+1}‖² + μ²‖b*_i‖².

Equations

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