theorem HexLLLMathlib.lllReduced_sound {n m : ℕ} (b : Hex.Matrix ℤ n m) (δ η : ℚ) : Hex.lllReduced b δ η = true → Hex.isLLLReduced b δ η ∧ b.independent

D2 soundness theorem: the executable integer reducedness checker entails both b.independent and the rational isLLLReduced b δ η predicate.

This is one of the two soundness ingredients feeding the combined certCheck_sound of hex-lll §"Certified external selection". The companion same-lattice piece is Hex.Matrix.sameLatticeCert_sound.

theorem HexLLLMathlib.lllReducedCheck_sound {n m : ℕ} (b : Hex.Matrix ℤ n m) (δ η : ℚ) : Hex.lllReducedCheck b δ η = true → Hex.isLLLReduced b δ η ∧ b.independent

Soundness of the selected reducedness clause Hex.lllReducedCheck: whichever side decided; the fixed-precision interval checker (HexLLLMathlib.lllReducedInterval_sound), the exact integer checker chosen by the size predictor, or the exact fallback after interval indecision (both via lllReduced_sound above); acceptance entails the rational isLLLReduced predicate and independence. The predictor Hex.Internal.intervalWins only selects between sound checkers, so no hypothesis about it is needed.

theorem HexLLLMathlib.certCheck_sound {n m : ℕ} {B B' : Hex.Matrix ℤ n m} {U V : Hex.Matrix ℤ n n} {δ η : ℚ} : Hex.certCheck B B' U V δ η = true → (∀ (v : Vector ℤ m), B.memLattice v ↔ B'.memLattice v) ∧ B'.independent ∧ Hex.isLLLReduced B' δ η

Soundness of the certified-selection checker Hex.certCheck: an accepted certificate (B', U, V) proves that B and B' generate the same integer row lattice, that B' is independent, and that B' is (δ, η)-LLL-reduced.

Composes the two soundness ingredients:

• Hex.Matrix.sameLatticeCert_sound (Mathlib-free, HexLLL/Basic.lean) for the same-lattice clause, and

• lllReducedCheck_sound (above) for independence and reducedness, covering both the interval decision and the exact integer fallback.

No validity hypothesis on η: the 1/2 ≤ η, η² < δ conditions for the LLL short-vector bound live on short_vector_bound_of_size_bound, not on the checker. This is the single trusted soundness theorem feeding the certified-selection correctness of lll.