Soundness of the executable reducedness checkers: acceptance of the exact lllReducedInt, the dispatched lllReducedCheck, and the bundled certCheck entails the rational Hex.isLLLReduced predicate, independence, and the same-lattice property. The interval branch consumes lllReducedInterval_sound.

Soundness of the integer reducedness checker

Hex.lllReducedInt b δ η accepts iff three integer-only inequalities hold over Hex.GramSchmidt.Int.data b. This section bridges those integer inequalities to the rational predicate Hex.isLLLReduced b δ η and to b.independent, the last theorem (Hex.lllReducedInt_sound) being the D2 deliverable used by the combined certCheck_sound of hex-lll §"Certified external dispatch".

theorem HexLLLMathlib.lllReducedInt_sound {n m : ℕ} (b : Hex.Matrix ℤ n m) (δ η : ℚ) : Hex.lllReducedInt 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 dispatch". 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 dispatched 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 lllReducedInt_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-dispatch 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-dispatch correctness of lll.