def Hex.Internal.intervalPrec : Nat

Working precision (bits) of the interval reducedness checker. The inequalities being certified carry slack by design: the selection 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 := 3 / 4) (η : Rat := 1 / 2) : 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 Hex.lllReduced checker, which keeps completeness structural. The correspondence theorem HexLLLMathlib.lllReducedInterval_sound proves that acceptance entails independence and LLL reducedness at the exact rational parameters.

Equations

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

def Hex.lllReduced {n m : Nat} (b : Matrix Int n m) (δ : Rat := 3 / 4) (η : Rat := 1 / 2) : 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. The correspondence theorem HexLLLMathlib.lllReduced_sound relates this checker to rational LLL reducedness using Hex.GramSchmidt.Int.scaledCoeffs_eq, Hex.GramSchmidt.Int.basis_normSq, and Hex.GramSchmidt.Int.gramDet_pos. δ and η default to the classical 3/4 and 1/2, so lllReduced b tests textbook LLL-reducedness (the bound achieved by the native reducer).

Equations

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

inductive Hex.Internal.CheckerOutcome : Type

Outcome of one certified-selection 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

  The interval calculation certified reducedness.

• exactPrimary : CheckerOutcome

  The predictor selected exact arithmetic immediately.

• exactFallback : CheckerOutcome

  Exact arithmetic followed an inconclusive interval calculation.

@[instance_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.

@[instance_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 ExternalReducer.Diagnostics for the selection outcomes; this tally is the observability hook that lets measurements verify the selection predictor and confirm the interval path never reached indecision (exactFallback = 0).

• interval : Nat

  Decisions completed by interval arithmetic.

• exactPrimary : Nat

  Decisions sent directly to the exact checker.

• exactFallback : Nat

  Decisions sent to the exact checker after an inconclusive interval check.

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

Equations

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

@[instance_reducible]

instance Hex.Internal.instReprCheckerTally : Repr CheckerTally

Equations

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

@[instance_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

@[instance_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-selection 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 handling.

Equations

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

def Hex.Internal.checkerTally : IO CheckerTally

Read the certified-selection 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 ExternalReducer.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-selection outcome in compiled code and otherwise returns k. This keeps the checker API usable from pure code while still giving benchmark harnesses handling diagnostics.

Equations

• Hex.Internal.withRecordCheckerOutcome _o k = k

def Hex.Internal.dispatchFactor : Nat

Selection 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 selects 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 selection: 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 := 3 / 4) (η : Rat := 1 / 2) : Bool

Reducedness clause of the certified selection. On the same integer d/ν data, two checkers can decide reducedness: the exact integer checker Hex.lllReduced, always complete, and the fixed-precision Hex.lllReducedInterval. The size predictor Hex.Internal.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-selection 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 Boolean checkers Hex.Matrix.sameLatticeCert and Hex.lllReducedCheck, whose interval decision has an exact Hex.lllReduced fallback. The correspondence theorem HexLLLMathlib.certCheck_sound entails the property triple (same lattice, B' independent, isLLLReduced B' δ η) and makes this check the trust boundary for certified external selection.

Equations

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