Validity of the executable LLLState against its Gram-Schmidt interpretation: ofBasis_valid, the scaled-coefficient identification lllState_ν_eq_coeffs, and the integer Lovász test as the rational isLLLReduced Lovász clause.

theorem HexLLLMathlib.LLLState.ofBasis_valid {n m : ℕ} (b : Hex.Matrix ℤ n m) : (Hex.Internal.LLLState.ofBasis b).Valid

The canonical LLLState constructor packages the executable Gram-Schmidt data. Lives on the Mathlib side because the diagonal Gram-determinant identification (gramDetVec_eq_gramDet) consumes a StepWitness b, which is supplied by StepWitness.ofGram.

theorem HexLLLMathlib.lllState_ν_eq_coeffs {n m : ℕ} (s : Hex.Internal.LLLState n m) (hvalid : s.Valid) (i j : ℕ) (hi : i < n) (hj : j < n) (hji : j < i) : ↑((s.ν.getRow ⟨i, hi⟩).get ⟨j, hj⟩) = ↑(s.d.get ⟨j + 1, ⋯⟩) * ((Hex.GramSchmidt.Int.coeffs s.b).getRow ⟨i, hi⟩).get ⟨j, hj⟩

Mathlib-side correspondence from the executable LLL state scaled-coefficient certificate to the rational Gram-Schmidt coefficient relation.

theorem HexLLLMathlib.lovasz_check_iff_isLLLReduced_pair {n m : ℕ} (s : Hex.Internal.LLLState n m) (k : ℕ) (hk : k < n) (hk0 : 0 < k) (hvalid : s.Valid) (hind : s.b.independent) {δ : ℚ} (_hδ : 1 / 4 < δ) (_hδ' : δ ≤ 1) : have hkm1lt := ⋯; have hkm1ltN1 := ⋯; have hkltN1 := ⋯; have hkSuccLt := ⋯; Int.ofNat δ.den * (Int.ofNat (s.d.get ⟨k + 1, hkSuccLt⟩) * Int.ofNat (s.d.get ⟨k - 1, hkm1ltN1⟩) + (s.ν.getRow ⟨k, hk⟩).get ⟨k - 1, hkm1lt⟩ ^ 2) ≥ δ.num * Int.ofNat (s.d.get ⟨k, hkltN1⟩) ^ 2 ↔ δ * Hex.Internal.LLLCore.basisNormSq (Hex.GramSchmidt.Int.basis s.b) ⟨k - 1, hkm1lt⟩ ≤ Hex.Internal.LLLCore.basisNormSq (Hex.GramSchmidt.Int.basis s.b) ⟨k, hk⟩ + ((Hex.GramSchmidt.Int.coeffs s.b).getRow ⟨k, hk⟩).get ⟨k - 1, hkm1lt⟩ * ((Hex.GramSchmidt.Int.coeffs s.b).getRow ⟨k, hk⟩).get ⟨k - 1, hkm1lt⟩ * Hex.Internal.LLLCore.basisNormSq (Hex.GramSchmidt.Int.basis s.b) ⟨k - 1, hkm1lt⟩

Integer Lovász check ↔ rational Lovász condition at pair (k - 1, k).

Hex.Internal.lllLoop dispatches on the integer comparison

δ.den * (d[k+1] * d[k-1] + ν[k][k-1]²) ≥ δ.num * d[k]²

while Hex.isLLLReduced quantifies the rational Lovász condition

δ * ‖b*[i]‖² ≤ ‖b*[i+1]‖² + μ[i+1][i]² · ‖b*[i]‖²

over every adjacent pair (i, i+1). Under s.Valid and s.b.independent, the two formulations agree at pair (k - 1, k): the integer scaled Gram-Schmidt data carried by s faithfully encodes the rational Lovász predicate at that position. This bridges the loop's executable check to the specification side of isLLLReduced so the loop-invariant proof can read off "the loop advances ⇒ Lovász holds at this pair."