Soundness of the fixed-precision interval reducedness checker.

Hex.lllReducedInterval runs an enclosure Gram-Schmidt pass over the exact integer Gram matrix of a candidate basis and accepts only when every independence, size-reduction, and Lovász inequality is decided with the enclosure strictly on the correct side. This module proves that acceptance entails the exact rational predicates: Hex.isLLLReduced b δ η together with Hex.Matrix.independent b.

The proof has three layers:

• per-operation containment lemmas for the dyadic interval kernel (Hex.Ival): each operation's result encloses the exact rational value whenever its inputs do;
• the exact Gram-Schmidt recurrence over the Gram matrix (gram_recurrence): ⟨b_i, b_j⟩ = ⟨b_i, b*_j⟩ + Σ_{k<j} μ[j][k]·⟨b_i, b*_k⟩, derived from basis_decomposition and basis_orthogonal, which is the recurrence the executable pass evaluates in interval arithmetic;
• a structural induction over the executable pass (pass_spec) showing every μ[i][j] and ‖b*_i‖² enclosure contains its exact rational value, then reading the three accepted clauses back through the enclosures. Independence follows from strict positivity of every ‖b*_i‖² enclosure via the unconditional Gram-determinant product identity gramDet_eq_prod_normSq_uncond.

Rounding helpers

Containment lemmas for the interval kernel

Exact Gram-Schmidt recurrence over the Gram matrix

Containment induction over the executable pass

Glue: the Gram array fed to the pass

Positivity of the Gram-determinant product

Soundness of the interval reducedness checker

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