Row-operation update formulas for hex-gram-schmidt.

This module packages the elementary row operations used by LLL and states the resulting update formulas for the Gram-Schmidt basis, coefficient, scaled coefficient, and Gram-determinant surfaces. The executable row operations live in HexMatrix; this file supplies the HexGramSchmidt-level API that later libraries use to reason about size reduction and adjacent swaps.

def Hex.GramSchmidt.prevRow {n : Nat} (k : Fin n) (hk : 0 < ↑k) : Fin n

The row immediately preceding k.

Equations

• Hex.GramSchmidt.prevRow k hk = ⟨↑k - 1, ⋯⟩

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

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

Equations

• Hex.GramSchmidt.Int.sizeReduce b j k r = b.rowAdd j k (-r)

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

Swap adjacent rows k - 1 and k.

Equations

• Hex.GramSchmidt.Int.adjacentSwap b k hk = b.rowSwap (Hex.GramSchmidt.prevRow k hk) k

def Hex.GramSchmidt.Int.adjacentSwapDenom {n m : Nat} (b : Matrix Int n m) (k : Fin n) : Int

The old d[k] denominator used by exact adjacent-swap updates.

Equations

• Hex.GramSchmidt.Int.adjacentSwapDenom b k = ↑(Hex.GramSchmidt.Int.gramDet b ↑k ⋯)

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

The old B = nu[k][k-1] pivot coefficient used by adjacent swaps.

Equations

• Hex.GramSchmidt.Int.adjacentSwapPivotCoeff b k hk = Hex.GramSchmidt.entry (Hex.GramSchmidt.Int.scaledCoeffs b) k (Hex.GramSchmidt.prevRow k hk)

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

Numerator of the adjacent-swap d[k]' update.

Equations

• One or more equations did not get rendered due to their size.

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

The integer quotient used as d[k]' in the adjacent-swap update formulas.

Equations

• Hex.GramSchmidt.Int.adjacentSwapGramDetQuotient b k hk = Hex.GramSchmidt.Int.adjacentSwapGramDetNumerator b k hk / Hex.GramSchmidt.Int.adjacentSwapDenom b k

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

Numerator of the adjacent-swap nu[i][k-1]' update for rows above k.

Equations

• One or more equations did not get rendered due to their size.

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

Numerator of the adjacent-swap nu[i][k]' update for rows above k.

Equations

• One or more equations did not get rendered due to their size.

theorem Hex.GramSchmidt.Int.basis_sizeReduce {n m : Nat} (b : Matrix Int n m) (j k : Fin n) (hjk : ↑j < ↑k) (r : Int) : basis (sizeReduce b j k r) = 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.

theorem Hex.GramSchmidt.Int.coeffs_sizeReduce_pivot {n m : Nat} (b : Matrix Int n m) (j k : Fin n) (hjk : ↑j < ↑k) (r : Int) (hnorm : ((basis b).row j).dotProduct ((basis b).row j) ≠ 0) : entry (coeffs (sizeReduce b j k r)) k j = entry (coeffs b) k j - ↑r

The defining effect of size reduction on the pivot coefficient: the (k, j) Gram-Schmidt coefficient drops by exactly r. Choosing r to be the nearest integer to μ[k][j] is precisely how LLL brings |μ[k][j]| ≤ 1/2, so this is the identity that certifies the size-reduction step achieves its bound. The nondegeneracy hypothesis hnorm records that row j of the basis is nonzero, so its coefficient is well defined.

theorem Hex.GramSchmidt.Int.coeffs_sizeReduce_lower {n m : Nat} (b : Matrix Int n m) (l j k : Fin n) (hlj : ↑l < ↑j) (hjk : ↑j < ↑k) (r : Int) : entry (coeffs (sizeReduce b j k r)) k l = entry (coeffs b) k l - ↑r * entry (coeffs b) j l

How size reduction propagates to coefficients below the pivot: for a column l earlier than j, the (k, l) coefficient decreases by r * μ[j][l]. A caller tracking the full coefficient row of k after a size reduction needs this to predict the side effect on already-reduced lower columns (and to see why size reduction is performed from the largest index downward).

theorem Hex.GramSchmidt.Int.coeffs_sizeReduce_other_row {n m : Nat} (b : Matrix Int n m) (j k : Fin n) (hjk : ↑j < ↑k) (r : Int) (i : Fin n) (hik : i ≠ k) : (coeffs (sizeReduce b j k r)).row i = (coeffs b).row i

Size reduction is local to the row being reduced: every coefficient row other than k is left untouched. This is the locality guarantee LLL relies on to argue that reducing row k cannot invalidate the size-reduced or Lovász-ordered state of any other row.

theorem Hex.GramSchmidt.Int.coeffs_sizeReduce_above_pivot {n m : Nat} (b : Matrix Int n m) (j k : Fin n) (hjk : ↑j < ↑k) (r : Int) (l : Fin n) (hjl : ↑j < ↑l) (hlk : ↑l < ↑k) : entry (coeffs (sizeReduce b j k r)) k l = entry (coeffs b) k l

Size-reducing row k against j does not touch coefficients at columns strictly between j and k: for j < l < k the (k, l) coefficient is unchanged. Together with coeffs_sizeReduce_lower and coeffs_sizeReduce_pivot, this pins down exactly which coefficients move, which is what lets LLL reduce columns one at a time without re-disturbing the columns above the current pivot.

theorem Hex.GramSchmidt.Int.basis_adjacentSwap_of_lt {n m : Nat} (b : Matrix Int n m) (k : Fin n) (hk : 0 < ↑k) (i : Fin n) (hi : ↑i + 1 < ↑k) : (basis (adjacentSwap b k hk)).row i = (basis b).row i

An adjacent swap at k leaves the Gram-Schmidt basis vector of every row strictly before the swapped pair unchanged (i + 1 < k, i.e. i < k - 1). Only the orthogonalisation of the two swapped rows and the rows above them can change, so a caller need only recompute the basis from index k - 1 onward after a Lovász swap.

theorem Hex.GramSchmidt.Int.basis_adjacentSwap_of_gt {n m : Nat} (b : Matrix Int n m) (k : Fin n) (hk : 0 < ↑k) (i : Fin n) (hi : ↑k < ↑i) : (basis (adjacentSwap b k hk)).row i = (basis b).row i

An adjacent swap at k leaves the Gram-Schmidt basis vector of every row strictly after the swapped pair unchanged. The span of the first k + 1 rows is invariant under swapping rows k - 1 and k, so the orthogonalisation of any later row, which projects against that span, is unaffected; only rows k - 1 and k move.

theorem Hex.GramSchmidt.Int.basis_adjacentSwap_prev {n m : Nat} (b : Matrix Int n m) (k : Fin n) (hk : 0 < ↑k) : have km1 := prevRow k hk; (basis (adjacentSwap b k hk)).row km1 = (basis b).row k + entry (coeffs b) k km1 • (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 : Matrix Int n m) (k : Fin n) (hk : 0 < ↑k) (hdenom : have km1 := prevRow k hk; have swappedPrev := (basis b).row k + entry (coeffs b) k km1 • (basis b).row km1; swappedPrev.dotProduct swappedPrev ≠ 0) : have km1 := prevRow k hk; have μ := entry (coeffs b) k km1; have prev := (basis b).row km1; have curr := (basis b).row k; have swappedPrev := curr + μ • prev; (basis (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.

theorem Hex.GramSchmidt.Int.coeffs_adjacentSwap_lower_prev {n m : Nat} (b : Matrix Int n m) (k : Fin n) (hk : 0 < ↑k) (j : Fin n) (hj : ↑j + 1 < ↑k) : have km1 := prevRow k hk; entry (coeffs (adjacentSwap b k hk)) km1 j = entry (coeffs b) k j

Effect of an adjacent swap on the lower coefficients of the new row k - 1: for a column j below the swapped pair (j + 1 < k), the new (k-1, j) coefficient equals the old (k, j) coefficient. Because the swap moves the old row k into position k - 1, its coefficients against the unchanged lower rows come along unchanged: the bookkeeping a caller needs to update the μ table in place rather than recomputing it.

theorem Hex.GramSchmidt.Int.coeffs_adjacentSwap_lower_curr {n m : Nat} (b : Matrix Int n m) (k : Fin n) (hk : 0 < ↑k) (j : Fin n) (hj : ↑j + 1 < ↑k) : have km1 := prevRow k hk; entry (coeffs (adjacentSwap b k hk)) k j = entry (coeffs b) km1 j

Companion to coeffs_adjacentSwap_lower_prev for the other swapped row: for a column j below the swapped pair (j + 1 < k), the new (k, j) coefficient equals the old (k-1, j) coefficient. The two rows exchange their lower coefficient vectors wholesale, so a caller can swap the corresponding μ-rows in the columns below k - 1 instead of recomputing them.

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

The updated pivot coefficient after an adjacent swap: the new μ[k][k-1] equals μ * ⟨prev, prev⟩ / ⟨swappedPrev, swappedPrev⟩, where μ is the old pivot coefficient and swappedPrev the new shorter pivot. This is the μ' entry of the standard LLL swap update; a caller uses it to refresh the pivot coefficient in place. The hypothesis hdenom records that the new pivot is nonzero, so the quotient is well defined.

The four adjacentSwap scaled-coefficient identities for rows above the pivot (scaledCoeffs_adjacentSwap_above_prev, _above_curr, and the two _dvd companions) live in HexGramSchmidtMathlib/Update.lean. Their proof path goes through bareiss_scaledCoeffMatrix_rowSwap_above_prev / _above_curr (the bordered-minor identities), which cross the Bareiss / det correspondence and so cannot be proved in the Mathlib-free core per [SPEC/Libraries/hex-gram-schmidt.md "Proof path governs placement, not just statement"].