The executable-to-Mathlib correspondence: the integer row lattice as a Submodule ℤ, its identification with Hex.Matrix.memLattice, the EuclideanSpace embeddings with their norm transport, and the conditional Euclidean short-vector bound for an already-reduced basis.

def HexLLLMathlib.latticeSubmodule {n m : ℕ} (b : Hex.Matrix ℤ n m) : Submodule ℤ (Fin m → ℤ)

The Mathlib Submodule ℤ generated by the rows of an executable integer matrix.

Equations

• HexLLLMathlib.latticeSubmodule b = Submodule.span ℤ (Set.range fun (i : Fin n) => HexMatrixMathlib.vectorEquiv (b.row i))

theorem HexLLLMathlib.mem_latticeSubmodule_iff {n m : ℕ} (b : Hex.Matrix ℤ n m) (v : Vector ℤ m) : HexMatrixMathlib.vectorEquiv v ∈ latticeSubmodule b ↔ b.memLattice v

theorem HexLLLMathlib.memLattice_iff_mem_latticeSubmodule {n m : ℕ} (b : Hex.Matrix ℤ n m) (v : Vector ℤ m) : b.memLattice v ↔ HexMatrixMathlib.vectorEquiv v ∈ latticeSubmodule b

theorem HexLLLMathlib.row_mem_latticeSubmodule {n m : ℕ} (b : Hex.Matrix ℤ n m) (i : Fin n) : HexMatrixMathlib.vectorEquiv (b.row i) ∈ latticeSubmodule b

def HexLLLMathlib.prefixSubmodule {n m : ℕ} (b : Hex.Matrix ℤ n m) (t : ℕ) : Submodule ℤ (Fin m → ℤ)

The submodule generated by rows whose indices are strictly below t.

Equations

• HexLLLMathlib.prefixSubmodule b t = Submodule.span ℤ (Set.range fun (i : { i : Fin n // ↑i < t }) => HexMatrixMathlib.vectorEquiv (b.row ↑i))

theorem HexLLLMathlib.row_mem_prefixSubmodule {n m : ℕ} (b : Hex.Matrix ℤ n m) (t : ℕ) (i : Fin n) (hi : ↑i < t) : HexMatrixMathlib.vectorEquiv (b.row i) ∈ prefixSubmodule b t

theorem HexLLLMathlib.prefixSubmodule_le_latticeSubmodule {n m : ℕ} (b : Hex.Matrix ℤ n m) (t : ℕ) : prefixSubmodule b t ≤ latticeSubmodule b

theorem HexLLLMathlib.vecMul_mem_prefixSubmodule_of_vector {n m : ℕ} (b : Hex.Matrix ℤ n m) (c : Vector ℤ n) (t : ℕ) (hc : ∀ (i : Fin n), t ≤ ↑i → c[i] = 0) : HexMatrixMathlib.vectorEquiv (Hex.Matrix.vecMul c b) ∈ prefixSubmodule b t

def HexLLLMathlib.intRowToEuclidean {m : ℕ} (row : Vector ℤ m) : EuclideanSpace ℝ (Fin m)

View an executable integer row as a vector in Mathlib's standard Euclidean space on Fin m.

Equations

• HexLLLMathlib.intRowToEuclidean row = WithLp.toLp 2 fun (j : Fin m) => ↑row[j]

def HexLLLMathlib.intVectorToEuclidean {m : ℕ} (x : Fin m → ℤ) : EuclideanSpace ℝ (Fin m)

View a Mathlib-side integer lattice vector in Mathlib's standard Euclidean space on Fin m.

Equations

• HexLLLMathlib.intVectorToEuclidean x = WithLp.toLp 2 fun (j : Fin m) => ↑(x j)

theorem HexLLLMathlib.norm_sq_intVectorToEuclidean {m : ℕ} (x : Fin m → ℤ) : ‖intVectorToEuclidean x‖ ^ 2 = ↑(HexMatrixMathlib.vectorEquiv.symm x).normSq

The Euclidean squared norm of a lattice vector embedded into EuclideanSpace ℝ (Fin m) equals the real cast of the executable integer squared norm of its Vector preimage.

theorem HexLLLMathlib.reduced_first_row_norm_sq_le {n m : ℕ} (b : Hex.Matrix ℤ n m) (δ η : ℚ) (hη : 1 / 2 ≤ η) (hδη : η * η < δ) (hδ' : δ ≤ 1) (hn : 1 ≤ n) (hli : b.independent) (hred : Hex.isLLLReduced b δ η) (x : Fin m → ℤ) (hx : x ∈ latticeSubmodule b) (hx0 : x ≠ 0) : ‖intRowToEuclidean (b.row ⟨0, ⋯⟩)‖ ^ 2 ≤ ↑((1 / (δ - η * η)) ^ (n - 1)) * ‖intVectorToEuclidean x‖ ^ 2

Mathlib-Euclidean-norm formulation of the LLL short-vector guarantee for an already (δ, η)-LLL-reduced executable basis.

The input vector is assumed to lie in the Mathlib latticeSubmodule. The proof route converts that hypothesis back through mem_latticeSubmodule_iff, applies the executable Hex.short_vector_bound_of_size_bound for the rational squared-norm inequality, then transports both sides through the concrete Euclidean norm coercions above.

Consumed downstream at η = 11/20 for the public Hex.lll headline (α = 1/(δ − 121/400), precondition 121/400 < δ); also at η = 1/2 for the native Hex.lllNative classical statement (α = 1/(δ − 1/4), precondition 1/4 < δ).