26.3. The Mathlib correspondence🔗

HexLLLMathlib is the proof-facing bridge for the Mathlib-free executable library. It identifies the row lattice used by the reducer with a Mathlib Submodule ℤ (Fin m → ℤ), transports reducedness and lattice preservation through both reduction paths, and states the short-vector guarantee with the norm on EuclideanSpace ℝ (Fin m). Importing it does not replace or wrap the computational path: calls to Hex.lll and Hex.lllNative still run the same native Lean definitions from HexLLL.

The generated submodule is characterized by the executable membership predicate, so a proof can cross the boundary in either direction with one rewrite.

theorem

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

Executable row-lattice membership agrees with membership in the generated submodule.

Reduction preserves this submodule. The public-path theorem needs no independence hypothesis: same-lattice certification is valid independently of the reducedness and short-vector arguments that use independence.

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

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

The integer row and integer function embeddings have explicit squared-norm characterizations. They connect the executable Vector.normSq quantity to the standard Euclidean norm without introducing a second lattice representation.

theorem

HexLLLMathlib.norm_sq_intRowToEuclidean {m : ℕ} (row : Vector ℤ m) :
  ‖HexLLLMathlib.intRowToEuclidean row‖ ^ 2 = ↑row.normSq
HexLLLMathlib.norm_sq_intRowToEuclidean
  {m : ℕ} (row : Vector ℤ m) :
  ‖HexLLLMathlib.intRowToEuclidean row‖ ^
      2 =
    ↑row.normSq

The Euclidean squared norm of an integer row embedded into EuclideanSpace ℝ (Fin m) equals the real cast of the executable integer squared norm.

theorem

HexLLLMathlib.norm_sq_intVectorToEuclidean {m : ℕ} (x : Fin m → ℤ) :
  ‖HexLLLMathlib.intVectorToEuclidean x‖ ^ 2 =
    ↑(HexMatrixMathlib.vectorEquiv.symm x).normSq
HexLLLMathlib.norm_sq_intVectorToEuclidean
  {m : ℕ} (x : Fin m → ℤ) :
  ‖HexLLLMathlib.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.

The headline theorem composes the reducedness proof, same-lattice result, and norm transport. Its hypotheses are exactly the public reducer's range conditions, nonempty and independent basis assumptions, and a nonzero vector in the input submodule; callers do not need to prove anything about the selected native or externally certified branch.

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 ∈ HexLLLMathlib.latticeSubmodule b) (hx0 : x ≠ 0) :
  ‖HexLLLMathlib.intRowToEuclidean
          ((Hex.lll b δ hδ hδ' hn).row ⟨0, ⋯⟩)‖ ^
      2 ≤
    ↑((1 / (δ - 121 / 400)) ^ (n - 1)) *
      ‖HexLLLMathlib.intVectorToEuclidean x‖ ^ 2
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 ∈ HexLLLMathlib.latticeSubmodule b)
  (hx0 : x ≠ 0) :
  ‖HexLLLMathlib.intRowToEuclidean
          ((Hex.lll b δ hδ hδ' hn).row
            ⟨0, ⋯⟩)‖ ^
      2 ≤
    ↑((1 / (δ - 121 / 400)) ^ (n - 1)) *
      ‖HexLLLMathlib.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.