theorem Hex.Matrix.identity_independent {n : ℕ} : (Matrix.identity n).independent

The identity matrix is independent: every executable leading Gram determinant is positive. Used by benchmarks of lll.firstShortVector, where the identity basis is the degenerate BZ-style recombination input with all-zero lift coefficients.

theorem Hex.Internal.LLLState.sizeReduce_independent {n m : ℕ} (s : LLLState n m) (k : ℕ) (hind : s.b.independent) (hvalid : s.Valid) (hvalid' : (s.sizeReduce k).Valid) : (s.sizeReduce k).b.independent

Size reduction preserves the executable Gram-determinant independence predicate. This public theorem lives in the Mathlib-side library so the Mathlib-free LLL implementation does not expose determinant-bound preservation theorems.

theorem Hex.Internal.LLLState.swapStep_independent {n m : ℕ} (s : LLLState n m) (k : ℕ) (hind : s.b.independent) (_hvalid : s.Valid) (hk0 : 0 < k) (hk : k < n) : (s.swapStep k).b.independent

Adjacent swap preserves the executable Gram-determinant independence predicate. Mirrors sizeReduce_independent for the swap step of the LLL inner loop.

theorem Hex.Internal.LLLState.swapStep_basisNormSq_below {n m : ℕ} (s : LLLState n m) (k : ℕ) (hk : k < n) (hk0 : 0 < k) (i : ℕ) (hi : i + 1 < k) : LLLCore.basisNormSq (GramSchmidt.Int.basis (s.swapStep k).b) ⟨i, ⋯⟩ = LLLCore.basisNormSq (GramSchmidt.Int.basis s.b) ⟨i, ⋯⟩

For i + 1 < k, the squared norm of the i-th Gram-Schmidt basis row is unchanged by swapStep s k.

theorem Hex.Internal.LLLState.swapStep_coeffs_below {n m : ℕ} (s : LLLState n m) (k : ℕ) (hk : k < n) (hk0 : 0 < k) (i j : ℕ) (hi : i + 1 < k) (hji : j < i) : (GramSchmidt.Int.coeffs (s.swapStep k).b)[⟨i, ⋯⟩][⟨j, ⋯⟩] = (GramSchmidt.Int.coeffs s.b)[⟨i, ⋯⟩][⟨j, ⋯⟩]

For j < i and i + 1 < k, the rational Gram-Schmidt coefficient at position (i, j) is unchanged by swapStep s k.

def Hex.prefixLLLReduced {n m : ℕ} (b : Matrix ℤ n m) (k : ℕ) (δ : ℚ) : Prop

The prefix δ-LLL-reduced predicate: the first k Gram-Schmidt rows satisfy size reduction (for all i < k, j < i) and the adjacent Lovász condition at (i, i + 1) (for all i + 1 < k). At k = n this coincides with isLLLReduced; at k ≤ 1 it is vacuously true.

Equations

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

theorem Hex.prefixLLLReduced.mono {n m : ℕ} {b : Matrix ℤ n m} {k k' : ℕ} {δ : ℚ} (h : prefixLLLReduced b k δ) (hk : k' ≤ k) : prefixLLLReduced b k' δ

Shrinking the row prefix weakens the predicate.

theorem Hex.prefixLLLReduced.advance {n m : ℕ} {b : Matrix ℤ n m} {k : ℕ} (hk : k < n) {δ : ℚ} (hpre : prefixLLLReduced b k δ) (hsize : ∀ (j : ℕ) (hj : j < k), have kFin := ⟨k, hk⟩; let jFin := ⟨j, ⋯⟩; have μ := (GramSchmidt.Int.coeffs b)[kFin][jFin]; 4 * μ * μ ≤ 1) (hlovasz : ∀ (hk0 : 0 < k), have kFin := ⟨k, hk⟩; let km1Fin := ⟨k - 1, ⋯⟩; have μ := (GramSchmidt.Int.coeffs b)[kFin][km1Fin]; δ * Internal.LLLCore.basisNormSq (GramSchmidt.Int.basis b) km1Fin ≤ Internal.LLLCore.basisNormSq (GramSchmidt.Int.basis b) kFin + μ * μ * Internal.LLLCore.basisNormSq (GramSchmidt.Int.basis b) km1Fin) : prefixLLLReduced b (k + 1) δ

Extending the prefix by one row: given prefixLLLReduced b k δ, the new size-reducedness data for row k and the new Lovász data at the pair (k - 1, k) (vacuous when k = 0) jointly yield prefixLLLReduced b (k + 1) δ. This is the "add one row to the certified prefix" lemma consumed by the lllLoop advance branch.

theorem Hex.prefixLLLReduced_one {n m : ℕ} (b : Matrix ℤ n m) (δ : ℚ) : prefixLLLReduced b 1 δ

At the empty prefix k = 1, prefixLLLReduced holds vacuously: the i < 1 (so i = 0, then j < 0 impossible) and i + 1 < 1 quantifiers are empty. This is the starting state for the lllLoop invariant induction.

theorem Hex.prefixLLLReduced_to_isLLLReduced {n m : ℕ} (b : Matrix ℤ n m) (δ : ℚ) (h : prefixLLLReduced b n δ) : isLLLReduced b δ (1 / 2)

At the full prefix k = n, prefixLLLReduced upgrades to isLLLReduced b δ (1/2): prefixLLLReduced always carries the algorithm's classical |μ| ≤ 1/2 size-reduction guarantee, which is the η = 1/2 instance of the size-reduced condition μ² ≤ η².

theorem Hex.Internal.LLLState.swapStep_prefixLLLReduced {n m : ℕ} (s : LLLState n m) (k : ℕ) (δ : ℚ) (h : prefixLLLReduced s.b k δ) : prefixLLLReduced (s.swapStep k).b (max (k - 1) 1) δ

swapStep s k preserves the prefix LLL-reduced predicate, with the prefix shrunk by one (clamped below by 1 to stay in the trivially-true regime when k ≤ 2). Mechanism: the swap only touches rows k - 1 and k, so every Gram-Schmidt quantity at indices strictly below k - 1 is preserved (swapStep_basisNormSq_below, swapStep_coeffs_below).

theorem Hex.Internal.LLLState.sizeReduceColumn_valid {n m : ℕ} (s : LLLState n m) (j k : Fin n) (hjk : ↑j < ↑k) (hvalid : s.Valid) : (s.sizeReduceColumn j k hjk).Valid

The single-column size reduction preserves Valid.

theorem Hex.Internal.LLLState.sizeReduce_valid {n m : ℕ} (s : LLLState n m) (k : ℕ) (hvalid : s.Valid) : (s.sizeReduce k).Valid

The size-reduction outer foldl preserves Valid.

theorem Hex.Internal.LLLState.sizeReduce_ν_bound {n m : ℕ} (s : LLLState n m) (k : ℕ) (hk : k < n) (hvalid : s.Valid) (hind : s.b.independent) (j : ℕ) (hj : j < k) : have kFin := ⟨k, hk⟩; have jFin := ⟨j, ⋯⟩; 2 * (((s.sizeReduce k).ν.getRow kFin).get jFin).natAbs ≤ s.d.get ⟨j + 1, ⋯⟩

Integer formulation: after s.sizeReduce k, every column j < k of row k of the scaled coefficients satisfies 2 * |ν[k][j]| ≤ d[j+1].

theorem Hex.Internal.LLLState.sizeReduce_size_reduced {n m : ℕ} (s : LLLState n m) (k : ℕ) (hk : k < n) (hvalid : s.Valid) (hind : s.b.independent) (j : ℕ) (hj : j < k) : have kFin := ⟨k, hk⟩; have jFin := ⟨j, ⋯⟩; have μ := GramSchmidt.entry (GramSchmidt.Int.coeffs (s.sizeReduce k).b) kFin jFin; 4 * μ * μ ≤ 1

After LLLState.sizeReduce s k, the row k of the rational Gram-Schmidt coefficients is size-reduced: 4 * μ[k][j]² ≤ 1 for every j < k.

theorem Hex.Internal.LLLState.sizeReduce_potential {n m : ℕ} (s : LLLState n m) (k : ℕ) : (s.sizeReduce k).potential = s.potential

Size reduction leaves the multiplicative termination potential unchanged, since it does not modify the stored Gram determinants.

theorem Hex.Internal.LLLState.swapStep_d_pivot {n m : ℕ} (s : LLLState n m) (k : ℕ) (hk : k < n) (hk0 : 0 < k) : have hkm1lt := ⋯; (s.swapStep k).d.get ⟨k, ⋯⟩ = ((Int.ofNat (s.d.get ⟨k + 1, ⋯⟩) * Int.ofNat (s.d.get ⟨k - 1, ⋯⟩) + (s.ν.getRow ⟨k, hk⟩).get ⟨k - 1, hkm1lt⟩ ^ 2) / Int.ofNat (s.d.get ⟨k, ⋯⟩)).toNat

Value lemma for the post-swap Gram-determinant slot at the pivot index. Reads swapStep directly: at index k, the updated d holds Int.toNat ⌊(d_{k+1}·d_{k-1} + B²)/d_k⌋, where B = ν[k][k-1]. Pairs with swapStep_d_eq to identify this slot with the post-swap basis' Gram determinant via gramDet_adjacentSwap_pivot.

theorem Hex.Internal.LLLState.swapStep_potential_lt {n m : ℕ} (s : LLLState n m) (k : ℕ) (hind : s.b.independent) (hvalid : s.Valid) (hk0 : 0 < k) (hk : k < n) (δnum : ℤ) (δden : ℕ) (_hδnum_pos : 0 < δnum) (hδden_pos : 0 < δden) (hδ_le_one : δnum ≤ Int.ofNat δden) (hfail : Int.ofNat δden * (Int.ofNat (s.d.get ⟨k + 1, ⋯⟩) * Int.ofNat (s.d.get ⟨k - 1, ⋯⟩) + (s.ν.getRow ⟨k, hk⟩).get ⟨k - 1, ⋯⟩ ^ 2) < δnum * Int.ofNat (s.d.get ⟨k, ⋯⟩) ^ 2) : (s.swapStep k).potential < s.potential

Strict decrease of the LLL termination potential across a swap that fails the integer Lovász test at row k.

Hypotheses:

• s.Valid, s.b.independent: the proof-facing interpretation of the state. Independence gives positivity of all d_j factors.

• 0 < k < n: the swap acts on adjacent rows k - 1, k.

• 0 < δnum and δnum ≤ δden: the Lovász parameter δ ∈ (0, 1] as an integer inequality on its numerator and denominator (in the form lllLoop's integer Lovász test consumes; follows from 1/4 < δ ≤ 1).

• hfail: the failing integer Lovász condition at k, exactly the test lllLoop evaluates before selecting the swap branch.

Conclusion: (s.swapStep k).potential < s.potential.

theorem Hex.Internal.LLLState.lllLoop_fuel_sufficient {n m : ℕ} (s : LLLState n m) (δ : ℚ) (hδ : 1 / 4 < δ) (hδ' : δ ≤ 1) (hn : 1 ≤ n) (hvalid : s.Valid) (hind : s.b.independent) {fuel' : ℕ} (hfuel : lllFuel s ≤ fuel') : lllLoop s 1 δ hδ hδ' ⋯ hn (lllFuel s) = lllLoop s 1 δ hδ hδ' ⋯ hn fuel'

Fuel sufficiency for lllLoop. For a valid state s with an independent basis, started at row k = 1, the bound lllFuel s = (s.potential + 1) * (n + 1) is enough fuel to reach the k = n base case. Equivalently, lllLoop is fuel-stable above this threshold: running with any fuel' ≥ lllFuel s returns the same matrix. Thus the fuel = 0 fallback in lllLoop is unreachable from valid public computation inputs.

theorem Hex.Internal.LLLState.sizeReduce_coeffs_row_of_ne {n m : ℕ} (s : LLLState n m) (k : ℕ) (i : Fin n) (hik : ↑i ≠ k) : (GramSchmidt.Int.coeffs (s.sizeReduce k).b).row i = (GramSchmidt.Int.coeffs s.b).row i

Coefficient rows at i ≠ k survive s.sizeReduce k intact.

theorem Hex.Internal.LLLState.sizeReduce_prefixLLLReduced {n m : ℕ} (s : LLLState n m) (k : ℕ) (δ : ℚ) (h : prefixLLLReduced s.b k δ) : prefixLLLReduced (s.sizeReduce k).b k δ

Size reduction preserves prefixLLLReduced at the same prefix length: rows strictly below k are unaffected by the row-k update, so the prefix invariant on the input transfers to the output.

theorem Hex.Internal.LLLState.lllLoop_isLLLReduced_of_fuel_gt_measure {n m : ℕ} (δ : ℚ) (hδ : 1 / 4 < δ) (hδ' : δ ≤ 1) (fuel : ℕ) (s : LLLState n m) (k : ℕ) (hk : 1 ≤ k) (hkn : k ≤ n) : s.Valid → s.b.independent → prefixLLLReduced s.b k δ → s.potential * (n + 1) + (n - k) < fuel → isLLLReduced (lllLoop s k δ hδ hδ' hk hkn fuel) δ (1 / 2)

With enough fuel and a starting state carrying prefixLLLReduced s.b k δ, lllLoop produces a δ-LLL-reduced basis. The fuel hypothesis s.potential * (n + 1) + (n - k) < fuel matches the measure used by lllLoop_eq_of_fuel_gt_measure.

theorem Hex.Internal.LLLState.lllLoop_independent {n m : ℕ} (δ : ℚ) (hδ : 1 / 4 < δ) (hδ' : δ ≤ 1) (fuel : ℕ) (s : LLLState n m) (k : ℕ) (hk : 1 ≤ k) (hkn : k ≤ n) : s.Valid → s.b.independent → (lllLoop s k δ hδ hδ' hk hkn fuel).independent

lllLoop preserves the independence of the starting basis: every iteration is either a sizeReduce (preserved by sizeReduce_independent) or an adjacent swap (preserved by swapStep_independent).