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

Acceptance by the fixed-precision interval checker entails the exact rational reducedness predicate and independence. This is the trusted statement consumed by lllReducedCheck_sound / certCheck_sound; the exact-integer fallback path is covered by lllReduced_sound.