17.4. The reduction entry points🔗

The exact all-integer reducer Hex.lllNative drives the standard LLL outer loop of integer size reduction and adjacent Lovász swaps directly on the exact d/ν Gram-Schmidt data. Its size-reduction step produces exact |μ| ≤ 1/2, so it satisfies the classical η = 1/2 bound and is the direct 1/4 < δ entry point.

def

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

Native (non-selected) executable LLL entry point. Builds the canonical integer state via Hex.Internal.LLLState.ofBasis and runs Hex.Internal.lllAux. Its output achieves the classical size-reduction bound |μ| ≤ 1/2 (η = 1/2), so its short-vector guarantee uses α = 1/(δ − 1/4) with the classical precondition 1/4 < δ. δ defaults to the classical 3/4, so lllNative b reduces at that parameter.

The public entry point unifies two internal paths behind one signature. Given a basis with independent rows and δ in the classical range, Hex.lll returns a reduced basis for the same lattice. It gets there either by running Hex.lllNative directly, or, when an external fpLLL reducer is available at runtime, by certifying the reducer's candidate with the verified checker and returning that instead (the next section describes the switch). Accepting a black-box candidate is what forces the slightly weaker η = 11/20 bound described below; both paths meet the same short-vector and same-lattice post-conditions, so callers and proofs never see which one ran.

def

Hex.lll {n m : Nat} (b : Hex.Matrix Int n m) (δ : Rat := 3 / 4)
  (hδ : 121 / 400 < δ := by grind) (hδ' : δ ≤ 1 := by grind)
  (hn : 1 ≤ n := by grind) : Hex.Matrix Int n m
Hex.lll {n m : Nat}
  (b : Hex.Matrix Int n m)
  (δ : Rat := 3 / 4)
  (hδ : 121 / 400 < δ := by grind)
  (hδ' : δ ≤ 1 := by grind)
  (hn : 1 ≤ n := by grind) :
  Hex.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.

17.4.1. The size-reduction bound and its constants🔗

The public Hex.lll certifies its output (δ, 11/20)-reduced: every Gram-Schmidt coefficient satisfies |μ| ≤ 11/20. Two numbers in its signature follow from η = 11/20. The precondition is 121/400 < δ, because 121/400 = (11/20)² = η² and the bound is well-defined only when η² < δ. The short-vector constant is 1/(δ − 121/400). So the 121/400 stands exactly where the classical bound would put 1/4 = (1/2)².

Why 11/20 rather than the classical 1/2? Solely the external reducer. The exact Hex.lllNative already lands at |μ| ≤ 1/2, but a black-box reducer cannot be forced to exactly 1/2 (fpLLL's default size-reduction target sits slightly above it), so the certified path accepts its candidate at the looser 11/20. When you want the tighter guarantee, call Hex.lllNative directly: its Mathlib-side short-vector theorem lllNative_short_vector carries the precondition 1/4 < δ and the strictly better constant 1/(δ − 1/4).

17.4.2. Short vectors🔗

Two functions read the short vectors off the reduced basis. Hex.lll.firstShortVector is the single short vector used by recombination. Hex.lll.shortVectors returns the whole reduced basis as an ordered candidate list.

def

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

def

Hex.lll.shortVectors {n m : Nat} (b : Hex.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)
Hex.lll.shortVectors {n m : Nat}
  (b : Hex.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.

Each has a counterpart under the Hex.lllNative namespace. Hex.lllNative.firstShortVector and Hex.lllNative.shortVectors call Hex.lllNative directly, so they take the tighter native precondition 1/4 < δ and skip the external reduction and its certification. They also omit the b.independent hypothesis. Independence is a precondition of the theorems about the output, not of the computation. The reducer runs on any input; the native-namespace variants simply forgo the reduced-basis guarantees, so you get the reduced rows back without having to discharge an independence proof. That is what makes them convenient for quick experimentation.

def

Hex.lllNative.firstShortVector {n m : Nat} (b : Hex.Matrix Int n m)
  (δ : Rat := 3 / 4) (hδ : 1 / 4 < δ := by grind)
  (hδ' : δ ≤ 1 := by grind) (hn : 1 ≤ n := by grind) : Vector Int m
Hex.lllNative.firstShortVector {n m : Nat}
  (b : Hex.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.

def

Hex.lllNative.shortVectors {n m : Nat} (b : Hex.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)
Hex.lllNative.shortVectors {n m : Nat}
  (b : Hex.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.