hex

17.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.lllReduced {n m : Nat} (b : Hex.Matrix Int n m) (δ : Rat := 3 / 4)
  (η : Rat := 1 / 2) : Bool
Hex.lllReduced {n m : Nat}
  (b : Hex.Matrix Int n m)
  (δ : Rat := 3 / 4) (η : Rat := 1 / 2) :
  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. The correspondence theorem HexLLLMathlib.lllReduced_sound relates this checker to rational LLL reducedness using Hex.GramSchmidt.Int.scaledCoeffs_eq, Hex.GramSchmidt.Int.basis_normSq, and Hex.GramSchmidt.Int.gramDet_pos. δ and η default to the classical 3/4 and 1/2, so lllReduced b tests textbook LLL-reducedness (the bound achieved by the native reducer).

The exact integer checker is complete, but its operands grow with the input. For larger inputs an unverified fixed-precision interval pass over the same integer data is usually faster at deciding reducedness, so the adaptive checker uses a cheap size predictor to pick between the two, always keeping the exact integer checker as a mandatory fallback when the interval pass is indecisive; completeness therefore stays structural rather than numerical. This is a choice between two checkers for a basis already in hand, and is independent of how that basis was reduced.

🔗def
Hex.lllReducedCheck {n m : Nat} (b : Hex.Matrix Int n m)
  (δ : Rat := 3 / 4) (η : Rat := 1 / 2) : Bool
Hex.lllReducedCheck {n m : Nat}
  (b : Hex.Matrix Int n m)
  (δ : Rat := 3 / 4) (η : Rat := 1 / 2) :
  Bool

Reducedness clause of the certified selection. On the same integer d/ν data, two checkers can decide reducedness: the exact integer checker Hex.lllReduced, always complete, and the fixed-precision Hex.lllReducedInterval. The size predictor Hex.Internal.intervalWins picks which to run first; when the interval pass is indecisive it falls back to the exact checker, so completeness stays structural rather than numerical. Records each decision in the checker tally, distinguishing all three outcomes.

Reducedness is only half of what an external candidate needs. We certify separately that the external certificate applies to the original input lattice: 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 a 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 Hex.Internal.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

An accepted Hex.Matrix.sameLatticeCert proves that the two bases generate 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-selection 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 Boolean checkers Hex.Matrix.sameLatticeCert and Hex.lllReducedCheck, whose interval decision has an exact Hex.lllReduced fallback. The correspondence theorem HexLLLMathlib.certCheck_sound entails the property triple (same lattice, B' independent, isLLLReduced B' δ η) and makes this check the trust boundary for certified external selection.