Embedding an integer at scale S gives an interval containing that integer.
theorem
HexLLLMathlib.sub_mem
{S : ℤ}
{I J : Hex.Internal.Ival}
{x y : ℚ}
(hx : Hex.Internal.Ival.mem S I x)
(hy : Hex.Internal.Ival.mem S J y)
:
Hex.Internal.Ival.mem S (I.sub J) (x - y)
Subtracting containing intervals gives an interval containing the difference.
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.