hex

6.3. Verified integer checkers🔗

The predicates above mention rational Gram-Schmidt data. Deciding them directly would require rational (or interval) arithmetic. The checkers instead work over the scaled integer Gram-Schmidt representation (the leading Gram determinants d and the integer scaled coefficients ν), so a Bool answer needs only exact integer comparisons. The base checker clears denominators in both the size-reduced and Lovász clauses.

🔗def
Hex.lllReducedInt {n m : Nat} (b : Hex.Matrix Int n m) (δ η : Rat) :
  Bool
Hex.lllReducedInt {n m : Nat}
  (b : Hex.Matrix Int n m) (δ η : Rat) :
  Bool

Executable integer Bool reducedness checker over the GramSchmidt.Int representation: leading Gram determinants d and integer scaled Gram-Schmidt coefficients ν.

Verifies, over integer arithmetic only:

  • independence: every d[k+1] is positive (k < n);

  • size-reduced at η: η.den · |ν[i][j]| ≤ η.num · d[j+1] for all j < i — the integer form of |μ| ≤ η;

  • integer Lovász at δ: δ.den · (d[i+2] · d[i] + ν[i+1][i]²) ≥ δ.num · d[i+1]² for all i + 1 < n.

No validity hypothesis on η is required: a malformed η (e.g. negative) is incompatible with a positive d[j+1] and the size-reduced bound, so the checker simply returns false. Soundness (lllReducedInt_sound, HexLLLMathlib) bridges to the rational predicate isLLLReduced via the integer correspondence (Hex.GramSchmidt.Int.scaledCoeffs_eq, basis_normSq, gramDet_pos).

For larger inputs an unverified fixed-precision interval pass is usually faster. The dispatching checker uses a size predictor to choose it, but always keeps the exact integer checker as a mandatory fallback when the interval pass is indecisive, so completeness stays structural rather than numerical.

🔗def
Hex.lllReducedCheck {n m : Nat} (b : Hex.Matrix Int n m) (δ η : Rat) :
  Bool
Hex.lllReducedCheck {n m : Nat}
  (b : Hex.Matrix Int n m) (δ η : Rat) :
  Bool

Reducedness clause of the certified dispatch. The size predictor intervalWins picks the checker expected to be faster on this input: the fixed-precision interval pass (with the exact integer checker as the mandatory fallback on indecision, keeping completeness structural rather than numerical), or the exact checker directly. Records each decision in the checker tally, distinguishing all three outcomes.

The same-lattice side of an external candidate is certified separately. A pair of integer transforms U, V witnessing U·B = B' and V·B' = B proves the two bases generate the same lattice. The certificate is a denominator-free Bool check with an overflow-safe packed-row comparison.

🔗def
Hex.Matrix.sameLatticeCert {n m : Nat} (B B' : Hex.Matrix Int n m)
  (U V : Hex.Matrix Int n n) : Bool
Hex.Matrix.sameLatticeCert {n m : Nat}
  (B B' : Hex.Matrix Int n m)
  (U V : Hex.Matrix Int n n) : Bool

Executable same-lattice certificate: two integer transforms that multiply the bases into each other. Each product equality is verified by the packed certificate mulEqCert, so neither product matrix is ever formed.

🔗theorem
Hex.Matrix.sameLatticeCert_sound {n m : Nat} {B B' : Hex.Matrix Int n m}
  {U V : Hex.Matrix Int n n} :
  B.sameLatticeCert B' U V = true →
    ∀ (v : Vector Int m), B.memLattice v ↔ B'.memLattice v
Hex.Matrix.sameLatticeCert_sound
  {n m : Nat} {B B' : Hex.Matrix Int n m}
  {U V : Hex.Matrix Int n n} :
  B.sameLatticeCert B' U V = true →
    ∀ (v : Vector Int m),
      B.memLattice v ↔ B'.memLattice v

Soundness of sameLatticeCert: accepted certificates prove identical integer row lattices.

The full external-candidate check composes the same-lattice certificate with the reducedness checker.

🔗def
Hex.certCheck {n m : Nat} (B B' : Hex.Matrix Int n m)
  (U V : Hex.Matrix Int n n) (δ η : Rat) : Bool
Hex.certCheck {n m : Nat}
  (B B' : Hex.Matrix Int n m)
  (U V : Hex.Matrix Int n n) (δ η : Rat) :
  Bool

Executable certified-dispatch checker: verifies that (B', U, V) is a valid external candidate for reducing B, i.e. B and B' generate the same integer row lattice (witnessed by U, V) and B' is (δ, η)-reduced.

Composes the Mathlib-free Bool checkers Matrix.sameLatticeCert and lllReducedCheck (interval decision with exact lllReducedInt fallback). Soundness (certCheck_sound, HexLLLMathlib) entails the property triple (same lattice, B' independent, isLLLReduced B' δ η) and is the single trusted bridge that the certified-dispatch path of lll depends on.