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.

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.

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.

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.

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.