def Hex.lll {n m : Nat} (b : Matrix Int n m) (δ : Rat := 3 / 4) (hδ : 121 / 400 < δ := by grind) (hδ' : δ ≤ 1 := by grind) (hn : 1 ≤ n := by grind) : Matrix Int n m

Top-level LLL entry point. It first tries certified external reduction: if ExternalReducer.externalReducerAvailable () is true and the candidate passes certCheck B B' U V δ (11/20), the certified B' is returned; otherwise Hex.lllNative runs. Both paths satisfy the identical post-condition (isLLLReduced (lll …) δ (11/20), same lattice, the public short-vector bound), so the choice is invisible to callers and to proofs. δ defaults to the classical LLL parameter 3/4, so a call can be as short as lll b.

Equations

• Hex.lll b δ hδ hδ' hn = match Hex.Internal.ExternalReducer.certifiedReduction b δ with | some B' => B' | none => Hex.lllNative b δ ⋯ hδ' hn

def Hex.lll.loadExternalReducer (path : System.FilePath) : IO Bool

Install an external LLL reducer from the shared library at path for the rest of this process, returning whether the load succeeded.

The library must export lean_fplll_lll_reduce (the fpLLL-ffi shim built by scripts/oracle/setup_fplll_ffi.sh); the loader calls dlopen, resolves that symbol, and records the reduction function. Once installed, a Hex.lll call whose candidate certifies under Hex.certCheck returns the accelerated basis; an absent reducer, a load failure, or a rejected candidate all fall through to the exact Hex.lllNative. Loading is an explicit action; there is no environment-variable read and no implicit load; and the trust boundary is unchanged: every external candidate is checked before use.

A later successful load replaces the current reducer; a failed load leaves the existing state untouched and returns false (writing the dlopen/dlsym diagnostic to stderr) when the library cannot be loaded or does not export the expected symbol.

Equations

• Hex.lll.loadExternalReducer path = Hex.Internal.ExternalReducer.loadExternalReducerImpl path.toString

def Hex.lll.externalReducerActive : IO Bool

Whether an external LLL reducer is currently installed in this process (via Hex.lll.loadExternalReducer or a statically linked symbol). When this is false, Hex.lll runs the exact Hex.lllNative; when it is true, Hex.lll attempts the certified external path first. Querying availability is side-effect-free apart from the one-shot static-symbol trial it may trigger.

Equations

• Hex.lll.externalReducerActive = pure (Hex.Internal.ExternalReducer.externalReducerAvailable ())

def Hex.lllNative.firstShortVector {n m : Nat} (b : Matrix Int n m) (δ : Rat := 3 / 4) (hδ : 1 / 4 < δ := by grind) (hδ' : δ ≤ 1 := by grind) (hn : 1 ≤ n := by grind) : Vector Int m

First row of Hex.lllNative's output on the exact native path. It is the non-selected counterpart of the public short-vector entry point below, never consults an external reducer, and takes no b.independent hypothesis, so Mathlib-free callers can use it directly; its short-vector guarantee at η = 1/2 is proved by HexLLLMathlib.lllNative_first_row_norm_sq_le.

Equations

• Hex.lllNative.firstShortVector b δ hδ hδ' hn = (Hex.lllNative b δ hδ hδ' hn).getRow ⟨0, hn⟩

def Hex.lll.firstShortVector {n m : Nat} (b : Matrix Int n m) (δ : Rat := 3 / 4) (hδ : 121 / 400 < δ := by grind) (hδ' : δ ≤ 1 := by grind) (hn : 1 ≤ n := by grind) : Vector Int m

The first row of the reduced basis: a provably short vector, bounded by the LLL approximation factor relative to any nonzero lattice vector, though not necessarily the shortest lattice vector. The precise correspondence theorem is HexLLLMathlib.lll_first_row_norm_sq_le. This is the canonical short-vector entry point for integer-polynomial recombination algorithms.

Equations

• Hex.lll.firstShortVector b δ hδ hδ' hn = (Hex.lll b δ hδ hδ' hn).getRow ⟨0, hn⟩

def Hex.lllNative.shortVectors {n m : Nat} (b : Matrix Int n m) (δ : Rat := 3 / 4) (hδ : 1 / 4 < δ := by grind) (hδ' : δ ≤ 1 := by grind) (hn : 1 ≤ n := by grind) : Array (Vector Int m)

Full Hex.lllNative output as an ordered array of candidate short vectors on the exact native path, forgoing the external reducer and the b.independent hypothesis.

Equations

• Hex.lllNative.shortVectors b δ hδ hδ' hn = (Hex.lllNative b δ hδ hδ' hn).rows.toArray

def Hex.lll.shortVectors {n m : Nat} (b : Matrix Int n m) (δ : Rat := 3 / 4) (hδ : 121 / 400 < δ := by grind) (hδ' : δ ≤ 1 := by grind) (hn : 1 ≤ n := by grind) : Array (Vector Int m)

The full reduced basis viewed as an ordered array of candidate short vectors.

Equations

• Hex.lll.shortVectors b δ hδ hδ' hn = (Hex.lll b δ hδ hδ' hn).rows.toArray