@[simp]

theorem HexLLLMathlib.lllNative_mem_latticeSubmodule_iff {n m : ℕ} (b : Hex.Matrix ℤ n m) (δ : ℚ) (hδ : 1 / 4 < δ) (hδ' : δ ≤ 1) (hn : 1 ≤ n) (x : Fin m → ℤ) : x ∈ latticeSubmodule (Hex.lllNative b δ hδ hδ' hn) ↔ x ∈ latticeSubmodule b

Membership in the Mathlib latticeSubmodule is preserved by Hex.lllNative.

@[simp]

theorem HexLLLMathlib.lll_mem_latticeSubmodule_iff {n m : ℕ} (b : Hex.Matrix ℤ n m) (δ : ℚ) (hδ : 121 / 400 < δ) (hδ' : δ ≤ 1) (hn : 1 ≤ n) (x : Fin m → ℤ) : x ∈ latticeSubmodule (Hex.lll b δ hδ hδ' hn) ↔ x ∈ latticeSubmodule b

Membership in the Mathlib latticeSubmodule is preserved by Hex.lll.

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

Classical Mathlib-Euclidean LLL short-vector bound on Hex.lllNative at η = 1/2. Combines Hex.lllNative_isLLLReduced with the conditional Euclidean bound reduced_first_row_norm_sq_le at η = 1/2.

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

Mathlib-Euclidean LLL short-vector bound on Hex.lll at η = 11/20. Combines Hex.lll_isLLLReduced (η = 11/20) with the conditional Euclidean bound reduced_first_row_norm_sq_le at η = 11/20, discharging its isLLLReduced hypothesis so the bound holds for the raw Hex.lll output.