The pure integer-arithmetic LLL reducer. LLLState carries only the integer basis, scaled Gram-Schmidt coefficients ν, and Gram determinants d; lllNative runs the fuel-bounded d/ν loop, the trusted exact reducer at the classical η = 1/2.

structure Hex.Internal.LLLState (n m : Nat) : Type

Integer-only state for later LLL reduction steps. The proof-facing fields connect the stored Gram determinants and scaled coefficients to the executable Gram-Schmidt integer data for b.

• b : Matrix Int n m

  The current integer basis, as a matrix of row vectors.

• ν : Matrix Int n n

  The integer scaled Gram-Schmidt coefficients of b.

• d : Vector Nat (n + 1)

  The leading Gram determinants of b (d[k] for k ≤ n).

structure Hex.Internal.LLLState.Valid {n m : Nat} (s : LLLState n m) : Prop

Correctness predicate for the proof-facing interpretation of an executable LLLState. Keeping this separate lets core state updates remain purely computational; Mathlib-side modules can prove preservation when they need the Gram-Schmidt interpretation.

• ν_eq (i j : Nat) (hi : i < n) (hj : j < n) : j < i → (s.ν.getRow ⟨i, hi⟩).get ⟨j, hj⟩ = ((GramSchmidt.Int.scaledCoeffs s.b).getRow ⟨i, hi⟩).get ⟨j, hj⟩

  Each below-diagonal ν entry equals the executable scaled Gram-Schmidt coefficient of s.b.

• d_eq (i : Nat) (hi : i < n + 1) : s.d.get ⟨i, hi⟩ = GramSchmidt.Int.gramDet s.b i ⋯

  Each d entry equals the corresponding leading Gram determinant of s.b.

def Hex.Internal.LLLState.nearestQuotient (νjk : Int) (dj1 : Nat) : Int

Integer nearest-quotient used by the LLL size-reduction test.

Equations

• Hex.Internal.LLLState.nearestQuotient νjk dj1 = (2 * νjk + Int.ofNat dj1).fdiv (2 * Int.ofNat dj1)

def Hex.Internal.LLLState.setEntry {n : Nat} (M : Matrix Int n n) (i j : Fin n) (x : Int) : Matrix Int n n

Targeted matrix entry update for LLL's integer coefficient state.

Uses Vector.modify rather than M.set i ((M.get i).set j x) so the underlying Array.modify swap-with-placeholder runs the inner row update in place when M is uniquely owned, avoiding the forced row copy that set i (… set j …) triggers via a lean_inc on the borrowed row.

Equations

• Hex.Internal.LLLState.setEntry M i j x = M.modifyRow ↑i fun (x_1 : Vector Int n) => x_1.set (↑j) x ⋯

theorem Hex.Internal.LLLState.foldl_finRange_set_outerSubMul_get_eq {n : Nat} (jVal : Nat) (hjn : jVal ≤ n) (base outerK outerJ : Vector Int n) (r : Int) (l : Fin n) : (Fin.foldl jVal (fun (row : Vector Int n) (l' : Fin jVal) => let lFin := ⟨↑l', ⋯⟩; row.set (↑lFin) (outerK.get lFin - r * outerJ.get lFin) ⋯) base).get l = if ↑l < jVal then outerK.get l - r * outerJ.get l else base.get l

Closed form for the entry-wise size-reduction sweep: folding the update row ← row.set l' (outerK l' − r · outerJ l') over the first jVal indices replaces exactly the entries below jVal by outerK − r · outerJ and leaves the rest of base untouched. Reading position l afterwards gives the reduced value when l.val < jVal and the original base.get l otherwise.

def Hex.Internal.LLLState.sizeReduceColumn {n m : Nat} (s : LLLState n m) (j k : Fin n) (hjk : ↑j < ↑k) : LLLState n m

Single-column size reduction update for row k against row j.

Equations

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

def Hex.Internal.LLLState.sizeReduce {n m : Nat} (s : LLLState n m) (k : Nat) : LLLState n m

Size-reduce row k against each earlier row using the stored integer scaled coefficients.

Equations

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

def Hex.Internal.LLLState.swapStep {n m : Nat} (s : LLLState n m) (k : Nat) : LLLState n m

Swap adjacent rows k - 1 and k, updating the stored scaled coefficients and Gram determinants with the integer formulas from the LLL specification.

Equations

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

theorem Hex.Internal.LLLState.sizeReduce_d {n m : Nat} (s : LLLState n m) (k : Nat) : (s.sizeReduce k).d = s.d

Size reduction leaves the stored Gram determinants unchanged.

theorem Hex.Internal.LLLState.sizeReduce_basis {n m : Nat} (s : LLLState n m) (k : Nat) : GramSchmidt.Int.basis (s.sizeReduce k).b = GramSchmidt.Int.basis s.b

Size reduction preserves the Gram-Schmidt basis of the state basis matrix.

theorem Hex.Internal.LLLState.swapStep_memLattice_iff {n m : Nat} (s : LLLState n m) (k : Nat) (v : Vector Int m) : (s.swapStep k).b.memLattice v ↔ s.b.memLattice v

Adjacent swaps preserve the generated lattice.

theorem Hex.Internal.LLLState.sizeReduceColumn_memLattice_iff {n m : Nat} (s : LLLState n m) (j k : Fin n) (hjk : ↑j < ↑k) (v : Vector Int m) : (s.sizeReduceColumn j k hjk).b.memLattice v ↔ s.b.memLattice v

A single-column size reduction preserves the generated lattice.

theorem Hex.Internal.LLLState.sizeReduce_memLattice_iff {n m : Nat} (s : LLLState n m) (k : Nat) (v : Vector Int m) : (s.sizeReduce k).b.memLattice v ↔ s.b.memLattice v

Size reduction preserves the generated lattice.

theorem Hex.Internal.LLLState.swapStep_ν_eq {n m : Nat} (s : LLLState n m) (k : Nat) (hvalid : (s.swapStep k).Valid) (i j : Nat) (hi : i < n) (hj : j < n) (hji : j < i) : ((s.swapStep k).ν.getRow ⟨i, hi⟩).get ⟨j, hj⟩ = ((GramSchmidt.Int.scaledCoeffs (s.swapStep k).b).getRow ⟨i, hi⟩).get ⟨j, hj⟩

The updated swap state still packages the intended scaled coefficient representation for its basis.

theorem Hex.Internal.LLLState.swapStep_d_eq {n m : Nat} (s : LLLState n m) (k : Nat) (hvalid : (s.swapStep k).Valid) (i : Nat) (hi : i < n + 1) : (s.swapStep k).d.get ⟨i, hi⟩ = GramSchmidt.Int.gramDet (s.swapStep k).b i ⋯

The updated swap state still packages the intended Gram-determinant representation for its basis.

noncomputable def Hex.Internal.LLLState.gramSchmidtCoeff {n m : Nat} (s : LLLState n m) (i j : Nat) (hi : i < n) (hj : j < n) : Rat

Recover a single rational Gram-Schmidt coefficient from the integer state. This exists for the proof layer; later executable code continues to work over the stored integer data.

Equations

• s.gramSchmidtCoeff i j hi hj = ↑((s.ν.getRow ⟨i, hi⟩).get ⟨j, hj⟩) / ↑(s.d.get ⟨j + 1, ⋯⟩)

def Hex.Internal.LLLState.potential {n m : Nat} (s : LLLState n m) : Nat

The multiplicative potential used by the LLL termination argument: d₁ * ... * dₙ₋₁.

Equations

• s.potential = Fin.foldl (n - 1) (fun (acc : Nat) (i : Fin (n - 1)) => acc * s.d.get ⟨↑i + 1, ⋯⟩) 1

theorem Hex.Internal.LLLState.potential_eq_gramDetProduct {n m : Nat} (s : LLLState n m) (hvalid : s.Valid) : s.potential = Fin.foldl (n - 1) (fun (acc : Nat) (i : Fin (n - 1)) => acc * GramSchmidt.Int.gramDet s.b (↑i + 1) ⋯) 1

Unfold the termination potential through the state's Gram-determinant certificate. The product only ranges over d₁, ..., dₙ₋₁, so later termination proofs do not need to reason about dₙ.

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

Initial LLLState constructor: build the integer state directly from a basis matrix. The ν field is the integral scaled Gram-Schmidt coefficient matrix and the d field is the leading Gram-determinant vector.

Takes no independence hypothesis: the construction is purely executable, and the resulting state is even Valid unconditionally (see HexLLLMathlib.LLLState.ofBasis_valid). b.independent enters only in the theorems about the reducer's output (lllNative_isLLLReduced and the short-vector bounds), never in building the state. Mathlib-free callers (benchmarks, fixture emitters, BHKS projected-row computation) use it directly.

Equations

• Hex.Internal.LLLState.ofBasis b = { b := b, ν := (Hex.GramSchmidt.Int.data b).ν, d := (Hex.GramSchmidt.Int.data b).d }

def Hex.Internal.lllLoop {n m : Nat} (s : LLLState n m) (k : Nat) (δ : Rat) (hδ : 1 / 4 < δ) (hδ' : δ ≤ 1) (hk : 1 ≤ k) (hkn : k ≤ n) : Nat → Matrix Int n m

Fuel-bounded outer LLL loop, dispatched by lllAux.

At row k, the loop size-reduces the current row, checks the integer Lovasz condition, and either advances to k + 1 or swaps adjacent rows and continues from the previous position.

The fuel = 0 branch returns the current basis as the total fallback for a pipeline-unreachable case: issue #6567 tracks the fuel-sufficiency theorem showing that lllFuel is enough for public pipeline calls.

Equations

• One or more equations did not get rendered due to their size.
• Hex.Internal.lllLoop s k δ hδ hδ' hk hkn 0 = s.b

theorem Hex.Internal.lllLoop_memLattice_iff {n m : Nat} (s : LLLState n m) (k : Nat) (δ : Rat) (hδ : 1 / 4 < δ) (hδ' : δ ≤ 1) (hk : 1 ≤ k) (hkn : k ≤ n) (fuel : Nat) (v : Vector Int m) : (lllLoop s k δ hδ hδ' hk hkn fuel).memLattice v ↔ s.b.memLattice v

lllLoop preserves the generated lattice: every iteration is either a sizeReduce (preserved by sizeReduce_memLattice_iff) or an adjacent swap (preserved by swapStep_memLattice_iff).

def Hex.Internal.lllFuel {n m : Nat} (s : LLLState n m) : Nat

Initial fuel bound for lllLoop; issue #6567 tracks the proof that this bound is sufficient for the public LLL pipeline.

Equations

• Hex.Internal.lllFuel s = (s.potential + 1) * (n + 1)

def Hex.Internal.lllAux {n m : Nat} (s : LLLState n m) (k : Nat) (δ : Rat) (hδ : 1 / 4 < δ) (hδ' : δ ≤ 1) (hk : 1 ≤ k) (hkn : k ≤ n) : Matrix Int n m

Outer LLL loop, dispatched by lll.

Compatibility wrapper preserving the original lllAux signature while the executable recursion is structurally bounded by lllFuel.

Equations

• Hex.Internal.lllAux s k δ hδ hδ' hk hkn = Hex.Internal.lllLoop s k δ hδ hδ' hk hkn (Hex.Internal.lllFuel s)

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

Native (non-dispatched) executable LLL entry point. Builds the canonical integer state via LLLState.ofBasis and dispatches to lllAux. This is the body the public lll runs by default; 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 < δ.

Equations

• Hex.lllNative b δ hδ hδ' hn = Hex.Internal.lllAux (Hex.Internal.LLLState.ofBasis b) 1 δ hδ hδ' Hex.lllNative._proof_1 hn

theorem Hex.Internal.one_quarter_lt_of_eta_eleven_twentieths {δ : Rat} (hδ : 121 / 400 < δ) : 1 / 4 < δ

121/400 < δ implies 1/4 < δ: relays the public lll (η = 11/20) precondition through to the native body (η = 1/2).