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

@[simp]

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.certifiedReduction_some_property {n m : ℕ} {b : Matrix ℤ n m} {δ : ℚ} {B' : Matrix ℤ n m} (h : Internal.ExternalReducer.certifiedReduction b δ = some B') : (∀ (v : Vector ℤ m), b.memLattice v ↔ B'.memLattice v) ∧ B'.independent ∧ isLLLReduced B' δ (11 / 20)

Property triple for an accepted external reduction: a B' returned by ExternalReducer.certifiedReduction b δ generates the same lattice as b, is independent, and is (δ, 11/20)-LLL-reduced. Composes certifiedReduction_some_certCheck with HexLLLTheory.certCheck_sound, the single trusted property-level correspondence of hex-lll §"Certified external selection".

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) δ (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-selection path it follows from certCheck_sound via certifiedReduction_some_property.

@[simp]

theorem Hex.lll_memLattice_iff {n m : ℕ} (b : Matrix ℤ n m) (δ : ℚ) (hδ : 121 / 400 < δ) (hδ' : δ ≤ 1) (hn : 1 ≤ n) (v : Vector ℤ m) : (lll b δ hδ hδ' hn).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).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).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 δ … has squared norm at most (1 / (δ − 121/400))^(n − 1) times the squared norm of any nonzero lattice vector.