Mathlib-side row-operation update theorems for hex-gram-schmidt.

The theorems in this module relate gramDet / scaledCoeffs under the size-reduce (earlier-row-add) and adjacent-swap row operations. Their statements are Hex-local, but their proofs cross the Mathlib boundary by composing HexMatrixMathlib.bareiss_eq_mathlib_det with HexMatrixMathlib.det_eq.symm through gramDet_rowAdd_earlier and the matrix-side gramDet_adjacentSwap_of_ne equation respectively, so they live in the Mathlib-side layer per [SPEC/Libraries/hex-gram-schmidt.md "Proof path governs placement, not just statement"]. The size-reduce theorems are thin wrappers around scaledCoeffs_rowAdd_pivot/lower/other_row/above_pivot and gramDet_rowAdd_earlier, which live in HexGramSchmidtMathlib/Int.lean.

Size-reduce updates

GramSchmidt.Int.sizeReduce b j k r is Matrix.rowAdd b j k (-r) (definitional), so the theorems below specialise the earlier-row-add updates in HexGramSchmidt/Int.lean to the LLL size-reduce row operation. They are kept in this Mathlib-side module because their proof path composes HexMatrixMathlib.bareiss_eq_mathlib_det with HexMatrixMathlib.det_eq.symm.

theorem Hex.GramSchmidt.Int.gramDet_sizeReduce {n m : ℕ} (b : Matrix ℤ n m) (j k : Fin n) (hjk : ↑j < ↑k) (r : ℤ) (t : ℕ) (ht : t ≤ n) : gramDet (sizeReduce b j k r) t ht = gramDet b t ht

The size-reduce row operation leaves every leading Gram determinant unchanged: sizeReduce b j k r adds -r times the earlier row j to the later row k (j < k), a unimodular operation. Specialises gramDet_rowAdd_earlier.

theorem Hex.GramSchmidt.Int.scaledCoeffs_sizeReduce_pivot {n m : ℕ} (b : Matrix ℤ n m) (j k : Fin n) (hjk : ↑j < ↑k) (r : ℤ) : entry (scaledCoeffs (sizeReduce b j k r)) k j = entry (scaledCoeffs b) k j - r * Int.ofNat (gramDet b (↑j + 1) ⋯)

Size-reduce update at the pivot column j: the scaled coefficient at (k, j) decreases by r * gramDet b (j+1), reflecting that subtracting r times row j cancels exactly that multiple of the j-leading Gram determinant from the (k, j) Cramer numerator.

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

Size-reduce update at a column l below the pivot (l < j < k): the scaled coefficient at (k, l) decreases by r times the (j, l) coefficient, since row k inherits -r times row j's contribution in that column.

theorem Hex.GramSchmidt.Int.scaledCoeffs_sizeReduce_other_row {n m : ℕ} (b : Matrix ℤ n m) (j k : Fin n) (hjk : ↑j < ↑k) (r : ℤ) (i : Fin n) (hik : i ≠ k) : (scaledCoeffs (sizeReduce b j k r)).row i = (scaledCoeffs b).row i

Size-reduce touches only row k: every other row i ≠ k of the scaled-coefficient matrix is left unchanged.

theorem Hex.GramSchmidt.Int.scaledCoeffs_sizeReduce_above_pivot {n m : ℕ} (b : Matrix ℤ n m) (j k : Fin n) (hjk : ↑j < ↑k) (r : ℤ) (l : Fin n) (hjl : ↑j < ↑l) (hlk : ↑l < ↑k) : entry (scaledCoeffs (sizeReduce b j k r)) k l = entry (scaledCoeffs b) k l

Size-reduce leaves the scaled coefficient at (k, l) unchanged for any column l strictly between the pivot j and k (j < l < k): row j's contribution there is already orthogonalised away, so adding a multiple of it has no effect.

Adjacent-swap updates

theorem Hex.GramSchmidt.Int.gramDet_adjacentSwap_of_ne {n m : ℕ} (b : Matrix ℤ n m) (k : Fin n) (hk : 0 < ↑k) (t : ℕ) (ht : t ≤ n) (htk : t ≠ ↑k) : gramDet (adjacentSwap b k hk) t ht = gramDet b t ht

Swapping the adjacent rows k-1 and k leaves the t-leading Gram determinant unchanged for every t ≠ k. For t > k both swapped rows lie inside the leading block, so the Gram matrix is conjugated by a row-and-column swap (determinant invariant); for t < k neither row is involved. Only the t = k prefix, which separates the two swapped rows, can change.

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

Adjacent-swap update for a column j strictly below the swapped block (j + 1 < k): the new scaled coefficient at row k-1 equals the old one at row k, because the swap moves the original row k into position k-1 while leaving the j-leading Gram determinant fixed.

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

Adjacent-swap companion to scaledCoeffs_adjacentSwap_lower_prev: for a column j strictly below the swapped block (j + 1 < k), the new scaled coefficient at row k equals the old one at row k-1, since the swap moves the original row k-1 into position k.

theorem Hex.GramSchmidt.Int.scaledCoeffs_adjacentSwap_pivot {n m : ℕ} (b : Matrix ℤ n m) (k : Fin n) (hk : 0 < ↑k) : have km1 := prevRow k hk; entry (scaledCoeffs (adjacentSwap b k hk)) k km1 = entry (scaledCoeffs b) k km1

The pivot scaled coefficient (k, k-1) is invariant under the adjacent swap of rows k-1 and k: the swap transposes the Cramer minor scaledCoeffMatrix, and a transpose preserves its determinant.

theorem Hex.GramSchmidt.Int.scaledCoeffs_adjacentSwap_before {n m : ℕ} (b : Matrix ℤ n m) (k : Fin n) (hk : 0 < ↑k) (i j : Fin n) (hi : ↑i + 1 < ↑k) (hji : ↑j < ↑i) : entry (scaledCoeffs (adjacentSwap b k hk)) i j = entry (scaledCoeffs b) i j

The adjacent swap of rows k-1, k leaves the scaled coefficient at (i, j) unchanged whenever the whole entry lies strictly below the swapped block (i + 1 < k, so both row i and its columns j < i are untouched).

theorem Hex.GramSchmidt.Int.scaledCoeffs_adjacentSwap_above_low {n m : ℕ} (b : Matrix ℤ n m) (k : Fin n) (hk : 0 < ↑k) (i j : Fin n) (hki : ↑k < ↑i) (hj : ↑j + 1 < ↑k) : entry (scaledCoeffs (adjacentSwap b k hk)) i j = entry (scaledCoeffs b) i j

For a row i above the swapped block (i > k) and a column j strictly below it (j + 1 < k), the adjacent swap of rows k-1, k leaves the scaled coefficient at (i, j) unchanged: the j-leading Gram determinant and the relevant Cramer numerator are both unaffected.

theorem Hex.GramSchmidt.Int.scaledCoeffs_adjacentSwap_above_high {n m : ℕ} (b : Matrix ℤ n m) (k : Fin n) (hk : 0 < ↑k) (i j : Fin n) (hki : ↑k < ↑i) (hkj : ↑k < ↑j) (hji : ↑j < ↑i) : entry (scaledCoeffs (adjacentSwap b k hk)) i j = entry (scaledCoeffs b) i j

For a row i and column j both strictly above the swapped block (k < j < i), the adjacent swap of rows k-1, k leaves the scaled coefficient at (i, j) unchanged.

theorem Hex.GramSchmidt.Int.gramDet_adjacentSwap_pivot {n m : ℕ} (b : Matrix ℤ n m) (k : Fin n) (hk : 0 < ↑k) (hdet : gramDet b ↑k ⋯ ≠ 0) : have km1 := prevRow k hk; have B := entry (scaledCoeffs b) k km1; ↑(gramDet (adjacentSwap b k hk) ↑k ⋯) = (↑(gramDet b (↑k + 1) ⋯) * ↑(gramDet b ↑km1 ⋯) + B ^ 2) / ↑(gramDet b ↑k ⋯)

The single k-leading Gram determinant that the adjacent swap of rows k-1, k can change, expressed as an exact integer quotient: writing B = scaledCoeffs b k (k-1), the new value is (d_{k+1} · d_{k-1} + B²) / d_k, where d_t = gramDet b t. Exactness of the division is supplied by adjacentSwap_gramDetNumerator_dvd; the hypothesis d_k ≠ 0 makes the quotient well-defined.

theorem Hex.GramSchmidt.Int.adjacentSwap_gramDetNumerator_dvd {n m : ℕ} (b : Matrix ℤ n m) (k : Fin n) (hk : 0 < ↑k) (_hdet : gramDet b ↑k ⋯ ≠ 0) : adjacentSwapDenom b k ∣ adjacentSwapGramDetNumerator b k hk

Exactness witness for gramDet_adjacentSwap_pivot: the pre-swap pivot adjacentSwapDenom b k = d_k divides the numerator adjacentSwapGramDetNumerator b k = d_{k+1} · d_{k-1} + B², because that numerator equals d_k times the post-swap k-leading Gram determinant.

Adjacent-swap scaled-coefficient identity for rows above the pivot

For i > k, after swapping adjacent rows km1, k (with km1.val + 1 = k.val), the executable Bareiss determinant of the scaled-coefficient Cramer minor scaledCoeffMatrix (rowSwap b km1 k) i km1 times the pivot Gram determinant d_k = gramDet b k.val equals the integer numerator

d_{km1} * nu[i][k] + B * nu[i][km1]

where B = nu[k][km1]. The proof linearises nu'[i][km1] (as a Rat) through the basis identity basis (rowSwap b km1 k) [km1] = basis b [k] + μ * basis b [km1] (via basis_rowSwap_adjacent_prev), identifies bareiss = nu' via scaledCoeffs_eq_scaledCoeffMatrix_bareiss, and discharges with ring.

theorem Hex.GramSchmidt.Int.bareiss_scaledCoeffMatrix_rowSwap_above_prev {n m : ℕ} (b : Matrix ℤ n m) (k : Fin n) (hk : 0 < ↑k) (i : Fin n) (hki : ↑k < ↑i) (_hdet : gramDet b ↑k ⋯ ≠ 0) : let km1 := prevRow k hk; have hkm1i := ⋯; (scaledCoeffMatrix (b.rowSwap km1 k) i km1 hkm1i).bareiss * ↑(gramDet b ↑k ⋯) = adjacentSwapScaledCoeffAbovePrevNumerator b k hk i

Bordered-minor identity for the swapped prev (km1) column at a row i > k: the executable Bareiss determinant of the Cramer minor times the pre-swap pivot d_k equals the integer numerator adjacentSwapScaledCoeffAbovePrevNumerator. Feeds the exact division in scaledCoeffs_adjacentSwap_above_prev.

Adjacent-swap scaled-coefficient identity for the swapped curr column

For i > k, after swapping adjacent rows km1, k, the executable Bareiss determinant of the scaled-coefficient Cramer minor scaledCoeffMatrix (rowSwap b km1 k) i k times the pivot Gram determinant d_k = gramDet b k.val equals the integer numerator

d_{k+1} * nu[i][km1] - B * nu[i][k]

where B = nu[k][km1]. The proof identifies bareiss with scaledCoeffs via scaledCoeffs_eq_scaledCoeffMatrix_bareiss and reduces the resulting Int equation to a rational identity. The rational identity uses the two new helpers dot_basis_rowSwap_curr_castRow_eq (the Cramer-style dot product expansion) and dot_basis_rowSwap_curr_prev_eq_normSq (D = Nk'), combined with gramDet_adjacentSwap_of_ne for t = k + 1 ≠ k (giving d_{k+1}(b') = d_{k+1}(b)), and the standard rationalisation lemmas for gramDet.

theorem Hex.GramSchmidt.Int.bareiss_scaledCoeffMatrix_rowSwap_above_curr {n m : ℕ} (b : Matrix ℤ n m) (k : Fin n) (hk : 0 < ↑k) (i : Fin n) (hki : ↑k < ↑i) (_hdet : gramDet b ↑k ⋯ ≠ 0) : (scaledCoeffMatrix (b.rowSwap (prevRow k hk) k) i k hki).bareiss * ↑(gramDet b ↑k ⋯) = adjacentSwapScaledCoeffAboveCurrNumerator b k hk i

Bordered-minor identity for the swapped curr (k) column at a row i > k: the executable Bareiss determinant of the Cramer minor times the pre-swap pivot d_k equals the integer numerator adjacentSwapScaledCoeffAboveCurrNumerator. Feeds the exact division in scaledCoeffs_adjacentSwap_above_curr.

Adjacent-swap scaled-coefficient quotient formulas for rows above the pivot

For i > k, after the adjacent swap of rows km1, k, the new scaled coefficients at the km1 and k columns are integer quotients of the corresponding adjacentSwapScaledCoeff*Numerator definitions by the pre-swap pivot adjacentSwapDenom b k = gramDet b k.val. Both pairs follow from the bordered-minor identities bareiss_scaledCoeffMatrix_rowSwap_above_prev and _above_curr once we rewrite bareiss → scaledCoeffs via scaledCoeffs_eq_scaledCoeffMatrix_bareiss.

theorem Hex.GramSchmidt.Int.adjacentSwap_scaledCoeffAbovePrevNumerator_dvd {n m : ℕ} (b : Matrix ℤ n m) (k : Fin n) (hk : 0 < ↑k) (i : Fin n) (hki : ↑k < ↑i) (hdet : gramDet b ↑k ⋯ ≠ 0) : adjacentSwapDenom b k ∣ adjacentSwapScaledCoeffAbovePrevNumerator b k hk i

Exactness witness for scaledCoeffs_adjacentSwap_above_prev: the pre-swap pivot adjacentSwapDenom b k = d_k divides adjacentSwapScaledCoeffAbovePrevNumerator, immediate from the bordered-minor identity bareiss_scaledCoeffMatrix_rowSwap_above_prev.

theorem Hex.GramSchmidt.Int.adjacentSwap_scaledCoeffAboveCurrNumerator_dvd {n m : ℕ} (b : Matrix ℤ n m) (k : Fin n) (hk : 0 < ↑k) (i : Fin n) (hki : ↑k < ↑i) (hdet : gramDet b ↑k ⋯ ≠ 0) : adjacentSwapDenom b k ∣ adjacentSwapScaledCoeffAboveCurrNumerator b k hk i

Exactness witness for scaledCoeffs_adjacentSwap_above_curr: the pre-swap pivot adjacentSwapDenom b k = d_k divides adjacentSwapScaledCoeffAboveCurrNumerator, immediate from the bordered-minor identity bareiss_scaledCoeffMatrix_rowSwap_above_curr.

theorem Hex.GramSchmidt.Int.scaledCoeffs_adjacentSwap_above_prev {n m : ℕ} (b : Matrix ℤ n m) (k : Fin n) (hk : 0 < ↑k) (i : Fin n) (hki : ↑k < ↑i) (hdet : gramDet b ↑k ⋯ ≠ 0) : entry (scaledCoeffs (adjacentSwap b k hk)) i (prevRow k hk) = adjacentSwapScaledCoeffAbovePrevNumerator b k hk i / adjacentSwapDenom b k

Adjacent-swap quotient formula at the prev (km1) column for a row i > k: the new scaled coefficient equals adjacentSwapScaledCoeffAbovePrevNumerator / adjacentSwapDenom, an exact integer division by the divisibility witness adjacentSwap_scaledCoeffAbovePrevNumerator_dvd.

theorem Hex.GramSchmidt.Int.scaledCoeffs_adjacentSwap_above_curr {n m : ℕ} (b : Matrix ℤ n m) (k : Fin n) (hk : 0 < ↑k) (i : Fin n) (hki : ↑k < ↑i) (hdet : gramDet b ↑k ⋯ ≠ 0) : entry (scaledCoeffs (adjacentSwap b k hk)) i k = adjacentSwapScaledCoeffAboveCurrNumerator b k hk i / adjacentSwapDenom b k

Adjacent-swap quotient formula at the curr (k) column for a row i > k: the new scaled coefficient equals adjacentSwapScaledCoeffAboveCurrNumerator / adjacentSwapDenom, an exact integer division by the divisibility witness adjacentSwap_scaledCoeffAboveCurrNumerator_dvd.