Integer-cast layer of the Gram-Schmidt surface for hex-gram-schmidt.

This module defines the rational-valued basis and coeffs of an integer input matrix (via GramSchmidt.castIntMatrix) and lifts the rational results of HexGramSchmidt/Basic/Rat.lean to the integer setting: the leading-row, orthogonality, triangular-decomposition, and prefix-span facts (basis_zero, basis_orthogonal, basis_decomposition, coeffs_diag, coeffs_upper, basis_span), together with the behaviour of basis/coeffs under the integer row operations Matrix.rowAdd and adjacent Matrix.rowSwap used by the LLL size-reduction and swap steps.

noncomputable def Hex.GramSchmidt.Int.basis {n m : Nat} (b : Matrix Int n m) : Matrix Rat n m

The Gram-Schmidt orthogonal basis for an integer matrix, viewed in Rat after coefficient divisions.

Equations

• Hex.GramSchmidt.Int.basis b = Hex.GramSchmidt.basisMatrix (Hex.GramSchmidt.castIntMatrix b)

noncomputable def Hex.GramSchmidt.Int.coeffs {n m : Nat} (b : Matrix Int n m) : Matrix Rat n n

The Gram-Schmidt coefficient matrix for an integer input matrix.

Equations

• Hex.GramSchmidt.Int.coeffs b = Hex.GramSchmidt.coeffMatrix (Hex.GramSchmidt.castIntMatrix b) (Hex.GramSchmidt.Int.basis b)

@[simp]

theorem Hex.GramSchmidt.Int.basis_zero {n m : Nat} (b : Matrix Int n m) (hn : 0 < n) : (basis b).row ⟨0, hn⟩ = Vector.map (fun (x : Int) => ↑x) (b.row ⟨0, hn⟩)

Gram-Schmidt leaves the first row untouched: the leading basis row of an integer matrix is its leading input row cast into Rat.

theorem Hex.GramSchmidt.Int.basis_orthogonal {n m : Nat} (b : Matrix Int n m) (i j : Nat) (hi : i < n) (hj : j < n) (hij : i ≠ j) : ((basis b).row ⟨i, hi⟩).dotProduct ((basis b).row ⟨j, hj⟩) = 0

Distinct Gram-Schmidt basis rows of an integer matrix (taken in Rat) are mutually orthogonal.

theorem Hex.GramSchmidt.Int.basis_decomposition {n m : Nat} (b : Matrix Int n m) (i : Nat) (hi : i < n) : Vector.map (fun (x : Int) => ↑x) (b.row ⟨i, hi⟩) = (basis b).row ⟨i, hi⟩ + prefixCombination (coeffs b) (basis b) i hi

The triangular factorization for an integer matrix: each input row, cast into Rat, equals its orthogonalized basis row plus the coefficient-weighted combination of the earlier basis rows.

@[simp]

theorem Hex.GramSchmidt.Int.coeffs_diag {n m : Nat} (b : Matrix Int n m) (i : Nat) (hi : i < n) : entry (coeffs b) ⟨i, hi⟩ ⟨i, hi⟩ = 1

The coefficient matrix of an integer input has unit diagonal: each row enters its own decomposition with weight 1.

theorem Hex.GramSchmidt.Int.coeffs_upper {n m : Nat} (b : Matrix Int n m) (i j : Nat) (hi : i < n) (hj : j < n) (hij : i < j) : entry (coeffs b) ⟨i, hi⟩ ⟨j, hj⟩ = 0

The coefficient matrix of an integer input is lower triangular: entries strictly above the diagonal vanish.

theorem Hex.GramSchmidt.Int.basis_rowAdd {n m : Nat} (b : Matrix Int n m) (src dst : Fin n) (c : Int) (hsrcdst : ↑src < ↑dst) : basis (b.rowAdd src dst c) = basis b

The integer Gram-Schmidt basis is invariant under adding an integer multiple of an earlier row to a later row.

theorem Hex.GramSchmidt.Int.basis_rowSwap_of_before {n m : Nat} (b : Matrix Int n m) (km1 k i : Fin n) (hkm1k : ↑km1 < ↑k) (hi : ↑i < ↑km1) : (basis (b.rowSwap km1 k)).row i = (basis b).row i

Swapping rows km1 and k of an integer matrix leaves every basis row before the pair unchanged.

theorem Hex.GramSchmidt.Int.basis_rowSwap_adjacent_prev {n m : Nat} (b : Matrix Int n m) (km1 k : Fin n) (hkm1 : ↑km1 + 1 = ↑k) : (basis (b.rowSwap km1 k)).row km1 = (basis b).row k + entry (coeffs b) k km1 • (basis b).row km1

After swapping adjacent rows km1, k of an integer matrix, the basis row at the lower index km1 becomes the old basis row k plus its projection coefficient times the old basis row km1.

theorem Hex.GramSchmidt.Int.basis_rowSwap_of_after {n m : Nat} (b : Matrix Int n m) (km1 k i : Fin n) (hkm1 : ↑km1 + 1 = ↑k) (hi : ↑k < ↑i) : (basis (b.rowSwap km1 k)).row i = (basis b).row i

Swapping the adjacent rows km1, k of an integer matrix leaves every basis row after the pair unchanged.

theorem Hex.GramSchmidt.Int.basis_rowSwap_adjacent_curr {n m : Nat} (b : Matrix Int n m) (km1 k : Fin n) (hkm1 : ↑km1 + 1 = ↑k) (hnorm : ((basis b).row k + entry (coeffs b) k km1 • (basis b).row km1).dotProduct ((basis b).row k + entry (coeffs b) k km1 • (basis b).row km1) ≠ 0) : have prev := (basis b).row km1; have curr := (basis b).row k; have mu := entry (coeffs b) k km1; have swappedPrev := curr + mu • prev; (basis (b.rowSwap km1 k)).row k = (curr.dotProduct curr / swappedPrev.dotProduct swappedPrev) • prev - (mu * prev.dotProduct prev / swappedPrev.dotProduct swappedPrev) • curr

After swapping adjacent rows km1, k of an integer matrix (assuming the swapped pivot is nonzero), the basis row at index k is the explicit two-term combination of the old basis rows km1, k.

theorem Hex.GramSchmidt.Int.coeffs_rowSwap_adjacent_lower_prev {n m : Nat} (b : Matrix Int n m) (km1 k j : Fin n) (hkm1 : ↑km1 + 1 = ↑k) (hj : ↑j < ↑km1) : entry (coeffs (b.rowSwap km1 k)) km1 j = entry (coeffs b) k j

After an adjacent swap of an integer matrix, the coefficient at the lower row km1 against an earlier column j equals the old coefficient at row k against j.

theorem Hex.GramSchmidt.Int.coeffs_rowSwap_adjacent_lower_curr {n m : Nat} (b : Matrix Int n m) (km1 k j : Fin n) (hkm1 : ↑km1 + 1 = ↑k) (hj : ↑j < ↑km1) : entry (coeffs (b.rowSwap km1 k)) k j = entry (coeffs b) km1 j

Dual of coeffs_rowSwap_adjacent_lower_prev for an integer matrix: after an adjacent swap, the coefficient at row k against an earlier column j equals the old coefficient at row km1 against j.

theorem Hex.GramSchmidt.Int.coeffs_rowSwap_adjacent_pivot {n m : Nat} (b : Matrix Int n m) (km1 k : Fin n) (hkm1 : ↑km1 + 1 = ↑k) (hnorm : ((basis b).row k + entry (coeffs b) k km1 • (basis b).row km1).dotProduct ((basis b).row k + entry (coeffs b) k km1 • (basis b).row km1) ≠ 0) : have mu := entry (coeffs b) k km1; have prev := (basis b).row km1; have curr := (basis b).row k; have swappedPrev := curr + mu • prev; entry (coeffs (b.rowSwap km1 k)) k km1 = mu * prev.dotProduct prev / swappedPrev.dotProduct swappedPrev

The explicit value of the new pivot coefficient (row k, column km1) after an adjacent swap of an integer matrix.

theorem Hex.GramSchmidt.Int.coeffs_rowSwap_adjacent_before {n m : Nat} (b : Matrix Int n m) (km1 k i j : Fin n) (hkm1 : ↑km1 + 1 = ↑k) (hi : ↑i < ↑km1) (hji : ↑j < ↑i) : entry (coeffs (b.rowSwap km1 k)) i j = entry (coeffs b) i j

Coefficient entries for a row and column both lying before the swapped pair are unaffected by an adjacent swap of an integer matrix.

theorem Hex.GramSchmidt.Int.coeffs_rowSwap_adjacent_after_low {n m : Nat} (b : Matrix Int n m) (km1 k i j : Fin n) (hkm1 : ↑km1 + 1 = ↑k) (hi : ↑k < ↑i) (hj : ↑j < ↑km1) : entry (coeffs (b.rowSwap km1 k)) i j = entry (coeffs b) i j

Coefficient entries for a row after the swapped pair against a column before it are unaffected by an adjacent swap of an integer matrix.

theorem Hex.GramSchmidt.Int.coeffs_rowSwap_adjacent_after_high {n m : Nat} (b : Matrix Int n m) (km1 k i j : Fin n) (hkm1 : ↑km1 + 1 = ↑k) (hi : ↑k < ↑i) (hj : ↑k < ↑j) (hji : ↑j < ↑i) : entry (coeffs (b.rowSwap km1 k)) i j = entry (coeffs b) i j

Coefficient entries for a row and column both lying after the swapped pair are unaffected by an adjacent swap of an integer matrix.

theorem Hex.GramSchmidt.Int.coeffs_rowAdd_lower {n m : Nat} (b : Matrix Int n m) (col src dst : Fin n) (hcolsrc : ↑col < ↑src) (hsrcdst : ↑src < ↑dst) (c : Int) : entry (coeffs (b.rowAdd src dst c)) dst col = entry (coeffs b) dst col + ↑c * entry (coeffs b) src col

Under integer row-add with src < dst, lower coefficients in the destination row update linearly below the pivot source column.

theorem Hex.GramSchmidt.Int.coeffs_rowAdd_pivot {n m : Nat} (b : Matrix Int n m) (src dst : Fin n) (hsrcdst : ↑src < ↑dst) (c : Int) (hnorm : ((basis b).row src).dotProduct ((basis b).row src) ≠ 0) : entry (coeffs (b.rowAdd src dst c)) dst src = entry (coeffs b) dst src + ↑c

Under integer row-add with src < dst, the pivot coefficient in the destination row increases by the added integer multiple.

theorem Hex.GramSchmidt.Int.coeffs_rowAdd_above_pivot {n m : Nat} (b : Matrix Int n m) (src col dst : Fin n) (hsrccol : ↑src < ↑col) (hcoldst : ↑col < ↑dst) (c : Int) : entry (coeffs (b.rowAdd src dst c)) dst col = entry (coeffs b) dst col

Under integer row-add with src < col < dst, destination-row coefficients above the pivot source column are preserved.

theorem Hex.GramSchmidt.Int.coeffs_rowAdd_other_row {n m : Nat} (b : Matrix Int n m) (src dst : Fin n) (c : Int) (hsrcdst : ↑src < ↑dst) (row : Fin n) (hrow : row ≠ dst) : (coeffs (b.rowAdd src dst c)).row row = (coeffs b).row row

An integer row-add only changes the destination row of the coefficient matrix.

theorem Hex.GramSchmidt.Int.basis_span {n m : Nat} (b : Matrix Int n m) (i : Nat) (hi : i < n) (v : Vector Rat m) : prefixSpan (basis b) i hi v ↔ prefixSpan (castIntMatrix b) i hi v

Orthogonalization preserves the row space of each prefix for an integer matrix: the first i + 1 basis rows span exactly the vectors spanned by the first i + 1 input rows cast into Rat.