5.4. Row-operation updates🔗

Lattice reduction modifies the input by elementary row operations and needs to know how the Gram-Schmidt data changes. HexGramSchmidt packages the two operations LLL uses (size reduction and adjacent swap) and states the resulting update formulas. The row operations themselves live in HexMatrix. HexGramSchmidt supplies the API for reasoning about their effect on the Gram-Schmidt data.

def

Hex.GramSchmidt.Int.sizeReduce {n m : Nat} (b : Hex.Matrix Int n m)
  (j k : Fin n) (r : Int) : Hex.Matrix Int n m
Hex.GramSchmidt.Int.sizeReduce {n m : Nat}
  (b : Hex.Matrix Int n m) (j k : Fin n)
  (r : Int) : Hex.Matrix Int n m

Size-reduce row k against an earlier row j by replacing b[k] with b[k] - r * b[j].

def

Hex.GramSchmidt.Int.adjacentSwap {n m : Nat} (b : Hex.Matrix Int n m)
  (k : Fin n) (hk : 0 < ↑k) : Hex.Matrix Int n m
Hex.GramSchmidt.Int.adjacentSwap
  {n m : Nat} (b : Hex.Matrix Int n m)
  (k : Fin n) (hk : 0 < ↑k) :
  Hex.Matrix Int n m

Swap adjacent rows k - 1 and k.

Size reduction subtracts an integer multiple of an earlier row from a later one. This unimodular operation leaves the entire Gram-Schmidt basis unchanged, so LLL can size-reduce freely without changing the orthogonalized vectors or the Gram determinants the swap step depends on.

theorem

Hex.GramSchmidt.Int.basis_sizeReduce {n m : Nat}
  (b : Hex.Matrix Int n m) (j k : Fin n) (hjk : ↑j < ↑k) (r : Int) :
  Hex.GramSchmidt.Int.basis (Hex.GramSchmidt.Int.sizeReduce b j k r) =
    Hex.GramSchmidt.Int.basis b
Hex.GramSchmidt.Int.basis_sizeReduce
  {n m : Nat} (b : Hex.Matrix Int n m)
  (j k : Fin n) (hjk : ↑j < ↑k)
  (r : Int) :
  Hex.GramSchmidt.Int.basis
      (Hex.GramSchmidt.Int.sizeReduce b j
        k r) =
    Hex.GramSchmidt.Int.basis b

Size-reducing row k against an earlier row j leaves the entire Gram-Schmidt basis unchanged. Subtracting an integer multiple of an earlier row from a later one is a unimodular operation that preserves the orthogonal profile, so LLL can size-reduce freely without disturbing the orthogonalised vectors, their norms, or the Gram determinants the swap step depends on.

An adjacent swap exchanges rows k - 1 and k, and the two basis rows at those positions change. The update formulas give the new vectors as explicit closed forms in the old data, so a caller can recompute the updated orthogonal vectors and their norms without rerunning Gram-Schmidt.

theorem

Hex.GramSchmidt.Int.basis_adjacentSwap_prev {n m : Nat}
  (b : Hex.Matrix Int n m) (k : Fin n) (hk : 0 < ↑k) :
  have km1 := Hex.GramSchmidt.prevRow k hk;
  (Hex.GramSchmidt.Int.basis
          (Hex.GramSchmidt.Int.adjacentSwap b k hk)).row
      km1 =
    (Hex.GramSchmidt.Int.basis b).row k +
      Hex.GramSchmidt.entry (Hex.GramSchmidt.Int.coeffs b) k km1 •
        (Hex.GramSchmidt.Int.basis b).row km1
Hex.GramSchmidt.Int.basis_adjacentSwap_prev
  {n m : Nat} (b : Hex.Matrix Int n m)
  (k : Fin n) (hk : 0 < ↑k) :
  have km1 :=
    Hex.GramSchmidt.prevRow k hk;
  (Hex.GramSchmidt.Int.basis
          (Hex.GramSchmidt.Int.adjacentSwap
            b k hk)).row
      km1 =
    (Hex.GramSchmidt.Int.basis b).row k +
      Hex.GramSchmidt.entry
          (Hex.GramSchmidt.Int.coeffs b) k
          km1 •
        (Hex.GramSchmidt.Int.basis b).row
          km1

The new Gram-Schmidt vector at row k - 1 after an adjacent swap: it is the old projection b_k + μ[k][k-1] • b_{k-1} of the swapped-in row against the rows below it. This is the orthogonal component that becomes the new shorter pivot, and whose norm LLL compares to the old one to decide whether the Lovász condition was violated.

theorem

Hex.GramSchmidt.Int.basis_adjacentSwap_curr {n m : Nat}
  (b : Hex.Matrix Int n m) (k : Fin n) (hk : 0 < ↑k)
  (hdenom :
    have km1 := Hex.GramSchmidt.prevRow k hk;
    have swappedPrev :=
      (Hex.GramSchmidt.Int.basis b).row k +
        Hex.GramSchmidt.entry (Hex.GramSchmidt.Int.coeffs b) k km1 •
          (Hex.GramSchmidt.Int.basis b).row km1;
    swappedPrev.dotProduct swappedPrev ≠ 0) :
  have km1 := Hex.GramSchmidt.prevRow k hk;
  have μ := Hex.GramSchmidt.entry (Hex.GramSchmidt.Int.coeffs b) k km1;
  have prev := (Hex.GramSchmidt.Int.basis b).row km1;
  have curr := (Hex.GramSchmidt.Int.basis b).row k;
  have swappedPrev := curr + μ • prev;
  (Hex.GramSchmidt.Int.basis
          (Hex.GramSchmidt.Int.adjacentSwap b k hk)).row
      k =
    (curr.dotProduct curr / swappedPrev.dotProduct swappedPrev) • prev -
      (μ * prev.dotProduct prev / swappedPrev.dotProduct swappedPrev) •
        curr
Hex.GramSchmidt.Int.basis_adjacentSwap_curr
  {n m : Nat} (b : Hex.Matrix Int n m)
  (k : Fin n) (hk : 0 < ↑k)
  (hdenom :
    have km1 :=
      Hex.GramSchmidt.prevRow k hk;
    have swappedPrev :=
      (Hex.GramSchmidt.Int.basis b).row
          k +
        Hex.GramSchmidt.entry
            (Hex.GramSchmidt.Int.coeffs b)
            k km1 •
          (Hex.GramSchmidt.Int.basis
                b).row
            km1;
    swappedPrev.dotProduct swappedPrev ≠
      0) :
  have km1 :=
    Hex.GramSchmidt.prevRow k hk;
  have μ :=
    Hex.GramSchmidt.entry
      (Hex.GramSchmidt.Int.coeffs b) k
      km1;
  have prev :=
    (Hex.GramSchmidt.Int.basis b).row km1;
  have curr :=
    (Hex.GramSchmidt.Int.basis b).row k;
  have swappedPrev := curr + μ • prev;
  (Hex.GramSchmidt.Int.basis
          (Hex.GramSchmidt.Int.adjacentSwap
            b k hk)).row
      k =
    (curr.dotProduct curr /
          swappedPrev.dotProduct
            swappedPrev) •
        prev -
      (μ * prev.dotProduct prev /
          swappedPrev.dotProduct
            swappedPrev) •
        curr

The new Gram-Schmidt vector at row k after an adjacent swap, given as an explicit linear combination of the old vectors b_{k-1} (prev) and b_k (curr). After the swap, row k carries the residual of the old prev against the new pivot swappedPrev; this closed form is what lets a caller recompute the updated orthogonal vector and its norm without rerunning Gram-Schmidt. The hypothesis hdenom records that the new pivot is nonzero, so the dividing inner products are well defined.