Mathlib-side correctness of the executable LLL reducers. The per-step Valid/independence preservation, the potential strict-decrease and fuel sufficiency, and the loop-invariant induction culminate in the reducedness, lattice, and rational short-vector capstones for Hex.lllNative and Hex.lll.

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

The identity matrix is independent: every executable leading Gram determinant is positive. Used by Phase 4 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 core does not expose determinant-bound preservation surfaces.

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.

Prefix LLL invariants under swapStep

For row indices strictly below k - 1, both the Gram-Schmidt basis row and the rational coefficient entries are preserved by swapStep s k, because the swap only touches rows k - 1 and k. These prefix lemmas package that observation as the building blocks for the prefixLLLReduced preservation corollary below.

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).

Size-reduce Valid preservation

The single-column update sizeReduceColumn edits b, ν at row k, and leaves d alone. Validity is preserved because the integer (b, ν) update mirrors the Mathlib-side scaledCoeffs updates (scaledCoeffs_sizeReduce_pivot/_lower/_above_pivot/_other_row) and the Gram-determinants are unchanged (gramDet_sizeReduce).

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.

Size-reduce size-reducedness

After LLLState.sizeReduce s k, the row k of the integer scaled coefficients satisfies 2 * |ν[k][j]| ≤ d[j+1] for every j < k (the integer formulation of the rational size-reducedness bound |μ[k][j]| ≤ 1/2). Pair with scaledCoeffs_eq to get the rational bound 4 * μ[k][j]² ≤ 1 on the post-reduction Gram-Schmidt coefficients. Closes the size-reduction half of the LLL loop invariant.

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

The size-reduce size-reducedness theorem (Sub-issue A of #6576). 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.

Potential strict-decrease under failing Lovász

These lemmas package the multiplicative termination potential d_1 · … · d_{n-1} behaviour under the two inner-loop updates:

• sizeReduce_potential: size reduction is potential-neutral (it only edits ν, never d).
• swapStep_d_pivot: the post-swap Gram-determinant slot reads Int.toNat ⌊(d_{k+1}·d_{k-1} + B²)/d_k⌋ directly off swapStep's definition (pairs with swapStep_d_eq to identify this slot with gramDet (adjacentSwap b k) k).
• swapStep_potential_lt: when the integer Lovász test fails at row k (the swap branch of lllLoop), the potential strictly decreases.

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 dispatching the swap branch.

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

Fuel sufficiency for lllLoop

The outer LLL loop lllLoop was made total in #6564 by structural recursion on a fuel argument, with fuel = 0 returning the current basis as a pipeline-unreachable fallback (per SPEC §8). This section proves the fallback unreachable for valid input: the bound lllFuel s = (s.potential + 1) * (n + 1) is sufficient for the loop started at k = 1 on s = ofBasis b.

The argument tracks the lexicographic measure s.potential * (n + 1) + (n - k):

• size reduction is potential-neutral (sizeReduce_potential) and is immediately followed by either an advance (decreases n - k by 1) or a swap;
• swaps strictly decrease the potential (swapStep_potential_lt), swallowing the n - k reset.

So each loop iteration strictly decreases the measure by ≥ 1, and the measure starts strictly below lllFuel s, so the loop hits the k = n base case before fuel exhausts.

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. This discharges the SPEC §8 "unreachable-by-pipeline-invariant" classification for the fuel = 0 fallback in lllLoop (introduced by the Route A totality refactor #6564).

Size-reduce coefficient-row preservation

Size reduction at row k rewrites only that row's coefficients; rows at indices i ≠ k are preserved by every iteration of the inner foldl. This packages the preservation as a single statement so the loop-invariant proof below can quote it without re-running the inductive coeffs_sizeReduce_other_row chain.

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.

Loop invariant induction

The prefixLLLReduced predicate is preserved by every iteration of lllLoop under the standard validity / independence hypotheses, and at the k = n base case it coincides with isLLLReduced. This packages those two facts into a single fuel-bounded induction.

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).

Capstones

The unconditional LLL guarantees split across two surfaces:

• Native (Hex.lllNative, classical bound, precondition 1/4 < δ). Carries isLLLReduced … δ (1/2) because the integer size-reduction step inside the loop produces exact |μ| ≤ 1/2. The short-vector denominator is δ − 1/4.
• Public (Hex.lll, precondition 121/400 < δ). Wraps lllNative and carries isLLLReduced … δ (11/20) (the η = 1/2 native bound weakens to η = 11/20 by isLLLReduced.mono_η). The short-vector denominator is δ − 121/400. This is the uniform bound an external reducer can promise.

theorem Hex.lllNative_isLLLReduced {n m : ℕ} (b : Matrix ℤ n m) (δ : ℚ) (hδ : 1 / 4 < δ) (hδ' : δ ≤ 1) (hn : 1 ≤ n) (hind : b.independent) : isLLLReduced (lllNative b δ hδ hδ' hn) δ (1 / 2)

The native LLL body produces a (δ, 1/2)-LLL-reduced matrix. Combines the fuel-sufficiency theorem (lllLoop_fuel_sufficient) with the loop invariant induction (lllLoop_isLLLReduced_of_fuel_gt_measure).

theorem Hex.lllNative_memLattice_iff {n m : ℕ} (b : Matrix ℤ n m) (δ : ℚ) (hδ : 1 / 4 < δ) (hδ' : δ ≤ 1) (hn : 1 ≤ n) (v : Vector ℤ m) : (lllNative b δ hδ hδ' hn).memLattice v ↔ b.memLattice v

The generated lattice is preserved by Hex.lllNative.

theorem Hex.lllNative_independent {n m : ℕ} (b : Matrix ℤ n m) (δ : ℚ) (hδ : 1 / 4 < δ) (hδ' : δ ≤ 1) (hn : 1 ≤ n) (hind : b.independent) : (lllNative b δ hδ hδ' hn).independent

Independence is preserved by Hex.lllNative.

theorem Hex.lllNative_short_vector {n m : ℕ} (b : Matrix ℤ n m) (δ : ℚ) (hδ : 1 / 4 < δ) (hδ' : δ ≤ 1) (hn : 1 ≤ n) (hind : b.independent) {v : Vector ℤ m} (hv : b.memLattice v) (hv' : v ≠ 0) : ↑((lllNative b δ hδ hδ' hn).row ⟨0, ⋯⟩).normSq ≤ (1 / (δ - 1 / 4)) ^ (n - 1) * ↑v.normSq

Classical native LLL short-vector bound at η = 1/2. For any independent integer basis b, the first row of Hex.lllNative b δ ... has squared norm at most (1 / (δ − 1/4))^(n − 1) times the squared norm of any nonzero lattice vector.

theorem Hex.dispatch_some_property {n m : ℕ} {b : Matrix ℤ n m} {δ : ℚ} {B' : Matrix ℤ n m} (h : Internal.LLLProvider.dispatch b δ = some B') : (∀ (v : Vector ℤ m), b.memLattice v ↔ B'.memLattice v) ∧ B'.independent ∧ isLLLReduced B' δ (11 / 20)

Property triple for an accepted dispatch result: a B' returned by LLLProvider.dispatch b δ generates the same lattice as b, is independent, and is (δ, 11/20)-LLL-reduced. Composes dispatch_some_certCheck with HexLLLMathlib.certCheck_sound, the single trusted property-level bridge of hex-lll §"Certified external dispatch".

theorem Hex.lll_isLLLReduced {n m : ℕ} (b : Matrix ℤ n m) (δ : ℚ) (hδ : 121 / 400 < δ) (hδ' : δ ≤ 1) (hn : 1 ≤ n) (hind : b.independent) : isLLLReduced (lll b δ hδ hδ' hn hind) δ (11 / 20)

The public LLL lll produces a (δ, 11/20)-LLL-reduced matrix. On the native path this is lllNative_isLLLReduced (η = 1/2) lifted to η = 11/20 by isLLLReduced.mono_η. On the certified-dispatch path it follows from certCheck_sound via dispatch_some_property.

theorem Hex.lll_memLattice_iff {n m : ℕ} (b : Matrix ℤ n m) (δ : ℚ) (hδ : 121 / 400 < δ) (hδ' : δ ≤ 1) (hn : 1 ≤ n) (hind : b.independent) (v : Vector ℤ m) : (lll b δ hδ hδ' hn hind).memLattice v ↔ b.memLattice v

The generated lattice is preserved by Hex.lll.

theorem Hex.lll_independent {n m : ℕ} (b : Matrix ℤ n m) (δ : ℚ) (hδ : 121 / 400 < δ) (hδ' : δ ≤ 1) (hn : 1 ≤ n) (hind : b.independent) : (lll b δ hδ hδ' hn hind).independent

Independence is preserved by Hex.lll.

theorem Hex.lll_short_vector {n m : ℕ} (b : Matrix ℤ n m) (δ : ℚ) (hδ : 121 / 400 < δ) (hδ' : δ ≤ 1) (hn : 1 ≤ n) (hind : b.independent) {v : Vector ℤ m} (hv : b.memLattice v) (hv' : v ≠ 0) : ↑((lll b δ hδ hδ' hn hind).row ⟨0, ⋯⟩).normSq ≤ (1 / (δ - 121 / 400)) ^ (n - 1) * ↑v.normSq

Public LLL short-vector bound at η = 11/20. For any independent integer basis b, the first row of Hex.lll b δ ... hind has squared norm at most (1 / (δ − 121/400))^(n − 1) times the squared norm of any nonzero lattice vector.