Executable reducedness checkers: the exact integer lllReducedInt, the fixed-precision lllReducedInterval, their cost-predicted dispatch lllReducedCheck, and the bundled external-candidate checker certCheck.

def Hex.Internal.intervalPrec : Nat

Working precision (bits) of the interval reducedness checker. The inequalities being certified carry slack by design: the dispatch requests a (requestedDelta δ, requestedEta)-reduced basis but certifies it against the weaker (δ, 11/20), so size reduction clears 11/20 by 11/20 − requestedEta and Lovász clears δ by (requestedDelta δ − δ)·d[i+1]². A fixed precision decides them on a correctly-reduced candidate; any indecision falls back to the exact checker rather than failing. The 128-bit width is fixed (independent of input size) and chosen to comfortably exceed the per-step slack margins for the documented input families, keeping every enclosure at a small, predictable arithmetic cost.

Equations

• Hex.Internal.intervalPrec = 128

def Hex.lllReducedInterval {n m : Nat} (b : Matrix Int n m) (δ η : Rat) : Bool

Fixed-precision interval reducedness checker. Computes enclosures of the Gram-Schmidt data of b from its exact integer Gram matrix and accepts only when every independence, size-reduction, and Lovász inequality is decided with the enclosure strictly on the correct side. false means "not reduced or indecisive at this precision": callers must fall back to the exact checker lllReducedInt, which keeps completeness structural. Soundness (lllReducedInterval_sound, HexLLLMathlib) entails b.independent ∧ isLLLReduced b δ η at the exact rational parameters.

Equations

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

def Hex.lllReducedInt {n m : Nat} (b : Matrix Int n m) (δ η : Rat) : Bool

Executable integer Bool reducedness checker over the GramSchmidt.Int representation: leading Gram determinants d and integer scaled Gram-Schmidt coefficients ν.

Verifies, over integer arithmetic only:

• independence: every d[k+1] is positive (k < n);
• size-reduced at η: η.den · |ν[i][j]| ≤ η.num · d[j+1] for all j < i — the integer form of |μ| ≤ η;
• integer Lovász at δ: δ.den · (d[i+2] · d[i] + ν[i+1][i]²) ≥ δ.num · d[i+1]² for all i + 1 < n.

No validity hypothesis on η is required: a malformed η (e.g. negative) is incompatible with a positive d[j+1] and the size-reduced bound, so the checker simply returns false. Soundness (lllReducedInt_sound, HexLLLMathlib) bridges to the rational predicate isLLLReduced via the integer correspondence (Hex.GramSchmidt.Int.scaledCoeffs_eq, basis_normSq, gramDet_pos).

Equations

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

inductive Hex.Internal.CheckerOutcome : Type

Outcome of one certified-dispatch reducedness decision: decided by the interval checker, decided by the exact checker because the size predictor chose it (exactPrimary), or referred to the exact checker after an indecisive interval pass (exactFallback).

• interval : CheckerOutcome
• exactPrimary : CheckerOutcome
• exactFallback : CheckerOutcome

@[implicit_reducible]

instance Hex.Internal.instReprCheckerOutcome : Repr CheckerOutcome

Equations

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

def Hex.Internal.instReprCheckerOutcome.repr : CheckerOutcome → Nat → Std.Format

Equations

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

@[implicit_reducible]

instance Hex.Internal.instBEqCheckerOutcome : BEq CheckerOutcome

Equations

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

def Hex.Internal.instBEqCheckerOutcome.beq : CheckerOutcome → CheckerOutcome → Bool

Equations

• Hex.Internal.instBEqCheckerOutcome.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

structure Hex.Internal.CheckerTally : Type

Tally of reducedness decisions, distinguishing enclosure-accepted from the two exact-checker modes. Mirrors LLLProvider.Diagnostics for the dispatch outcomes; this tally is the observability hook that lets measurements verify the dispatch predictor and confirm the interval path never reached indecision (exactFallback = 0).

• interval : Nat
• exactPrimary : Nat
• exactFallback : Nat

@[implicit_reducible]

instance Hex.Internal.instReprCheckerTally : Repr CheckerTally

Equations

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

def Hex.Internal.instReprCheckerTally.repr : CheckerTally → Nat → Std.Format

Equations

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

@[implicit_reducible]

instance Hex.Internal.instBEqCheckerTally : BEq CheckerTally

Equations

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

def Hex.Internal.instBEqCheckerTally.beq : CheckerTally → CheckerTally → Bool

Equations

• One or more equations did not get rendered due to their size.
• Hex.Internal.instBEqCheckerTally.beq x✝¹ x✝ = false

@[implicit_reducible]

instance Hex.Internal.instInhabitedCheckerTally : Inhabited CheckerTally

Equations

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

opaque Hex.Internal.checkerTallyRef : IO.Ref CheckerTally

def Hex.Internal.resetCheckerTally : IO Unit

Reset the certified-dispatch reducedness tally to zero. Bench and conformance harnesses call this before a measured run so the subsequent checkerTally snapshot describes only that run's interval/exact routing.

Equations

• Hex.Internal.resetCheckerTally = ST.Ref.set Hex.Internal.checkerTallyRef { }

def Hex.Internal.checkerTally : IO CheckerTally

Read the certified-dispatch reducedness tally accumulated since the last resetCheckerTally. The counts expose whether calls were accepted by the interval checker, sent directly to the exact checker, or needed an exact fallback after interval indecision.

Equations

• Hex.Internal.checkerTally = ST.Ref.get Hex.Internal.checkerTallyRef

unsafe def Hex.Internal.withRecordCheckerOutcomeImpl {α : Type} (o : CheckerOutcome) (k : α) : α

Side-effecting tally bump callable from pure code; definitionally the continuation k, with an @[implemented_by] side effect in compiled code. The continuation value is returned through unsafeBaseIO, so the compiler cannot eliminate the effect as an unused pure binding (the match unsafeBaseIO … with | () => k shape of LLLProvider.withRecordOutcome is erasable and its tally is known not to fire eagerly; see the workaround comment on runDispatchedFirstShortVectorChecksum).

Equations

• Hex.Internal.withRecordCheckerOutcomeImpl o k = unsafeBaseIO do ST.Ref.modify Hex.Internal.checkerTallyRef fun (t : Hex.Internal.CheckerTally) => Hex.Internal.bumpChecker✝ t o pure k

@[implemented_by Hex.Internal.withRecordCheckerOutcomeImpl]

def Hex.Internal.withRecordCheckerOutcome {α : Type} (_o : CheckerOutcome) (k : α) : α

Pure-facing wrapper that records one reducedness-dispatch outcome in compiled code and otherwise returns k. This keeps the checker API usable from pure code while still giving benchmark harnesses routing diagnostics.

Equations

• Hex.Internal.withRecordCheckerOutcome _o k = k

def Hex.Internal.dispatchFactor : Nat

Dispatch threshold of the size predictor intervalWins, as a multiple of the working precision. Derived from the per-operation cost ratio of the two checkers: the exact d/ν checker performs n³/3 multiplications on operands averaging n·maxDiagBits/4 bits, while the interval pass performs ~n³/6 products on fixed (intervalPrec + maxDiagBits)-bit mantissas, so enclosures win once n·maxDiagBits exceeds a fixed multiple of intervalPrec + maxDiagBits. On the two committed bench families this crosses over between n=25 and n=30 for harsh-cubic and between n=150 and n=180 for random-bounded (paired bench on carica). The boundary rungs are entangled: lowering the constant to pull harsh-cubic n=25 (where the interval pass runs ~10% faster, about 0.5 ms) onto the interval side also pulls random-bounded n=150 there, where the exact checker runs ~2% faster. On that ~360 ms rung the ~7 ms cost outweighs the harsh-cubic saving, so the constant stays at the value that keeps random-bounded n=150 on the exact side and minimizes total absolute misroute cost across both families.

Equations

• Hex.Internal.dispatchFactor = 16

def Hex.Internal.maxDiagBits {n m : Nat} (b : Matrix Int n m) : Nat

Nat.log2 (floor of the base-2 log) of the largest squared row norm. The Gram diagonal dominates all Gram entries by Cauchy-Schwarz, so this single scalar bounds the operand size of every checker and reducer pass. O(n·m) work — negligible against either. A deterministic function of the input alone, so the dispatches that read it keep per-input timing deterministic.

Equations

• Hex.Internal.maxDiagBits b = Fin.foldl n (fun (acc : Nat) (i : Fin n) => max acc (b.row i).normSq.natAbs.log2) 0

def Hex.Internal.intervalWins {n m : Nat} (b : Matrix Int n m) : Bool

Size predictor for the reducedness dispatch: true when the fixed-precision interval pass is predicted to beat the exact integer checker on this input. Reads only maxDiagBits, so the predictor is a function of the input alone, never of checker indecision, keeping per-input timing deterministic.

Equations

• Hex.Internal.intervalWins b = decide (n * Hex.Internal.maxDiagBits b ≥ Hex.Internal.dispatchFactor * (Hex.Internal.intervalPrec + Hex.Internal.maxDiagBits b))

def Hex.lllReducedCheck {n m : Nat} (b : Matrix Int n m) (δ η : Rat) : Bool

Reducedness clause of the certified dispatch. On the same integer d/ν data, two checkers can decide reducedness: the exact integer checker lllReducedInt, always complete, and a faster fixed-precision interval pass. The size predictor intervalWins picks which to run first; when the interval pass is indecisive it falls back to the exact checker, so completeness stays structural rather than numerical. Records each decision in the checker tally, distinguishing all three outcomes.

Equations

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

def Hex.certCheck {n m : Nat} (B B' : Matrix Int n m) (U V : Matrix Int n n) (δ η : Rat) : Bool

Executable certified-dispatch checker: verifies that (B', U, V) is a valid external candidate for reducing B, i.e. B and B' generate the same integer row lattice (witnessed by U, V) and B' is (δ, η)-reduced.

Composes the Mathlib-free Bool checkers Matrix.sameLatticeCert and lllReducedCheck (interval decision with exact lllReducedInt fallback). Soundness (certCheck_sound, HexLLLMathlib) entails the property triple (same lattice, B' independent, isLLLReduced B' δ η) and is the single trusted bridge that the certified-dispatch path of lll depends on.

Equations

• Hex.certCheck B B' U V δ η = (B.sameLatticeCert B' U V && Hex.lllReducedCheck B' δ η)