Rational Gram-Schmidt API for hex-gram-schmidt.

This module wraps the executable kernel into the rational-valued basis and coeffs of a Matrix Rat n m and proves their defining properties: the leading row is untouched (basis_zero), distinct basis rows are orthogonal (basis_orthogonal), the triangular factorization b = coeffs · basis (basis_decomposition), and the unit-diagonal / lower-triangular shape of coeffs (coeffs_diag, coeffs_upper, coeffs_lower_projection). It also tracks how basis and coeffs transform under Matrix.rowAdd and adjacent Matrix.rowSwap (the explicit re-orthogonalization formulas basis_rowSwap_adjacent_prev/_curr and the coefficient updates), and proves that orthogonalization preserves every row-prefix span (basis_span). These are the rational facts the integer-cast layer lifts.

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

The Gram-Schmidt orthogonal basis for a rational matrix.

Equations

• Hex.GramSchmidt.Rat.basis b = Hex.GramSchmidt.basisMatrix b

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

The Gram-Schmidt coefficient matrix for a rational input matrix.

Equations

• Hex.GramSchmidt.Rat.coeffs b = Hex.GramSchmidt.coeffMatrix b (Hex.GramSchmidt.Rat.basis b)

@[simp]

theorem Hex.GramSchmidt.Rat.basis_zero {n m : Nat} (b : Matrix Rat n m) (hn : 0 < n) : (basis b).row ⟨0, hn⟩ = b.row ⟨0, hn⟩

Gram-Schmidt leaves the first row untouched: the leading basis row of a rational matrix is its leading input row.

theorem Hex.GramSchmidt.Rat.basis_orthogonal {n m : Nat} (b : Matrix Rat 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

The defining guarantee of the construction: distinct rational Gram-Schmidt basis rows are mutually orthogonal (their dot product is zero).

theorem Hex.GramSchmidt.Rat.basis_decomposition {n m : Nat} (b : Matrix Rat n m) (i : Nat) (hi : i < n) : b.row ⟨i, hi⟩ = (basis b).row ⟨i, hi⟩ + prefixCombination (coeffs b) (basis b) i hi

The triangular factorization b = coeffs · basis, stated row by row: each rational input row equals its orthogonalized basis row plus the coefficient-weighted combination of the earlier basis rows.

@[simp]

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

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

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

The rational coefficient matrix is lower triangular: entries strictly above the diagonal vanish, since a row only combines basis rows with smaller index.

theorem Hex.GramSchmidt.Rat.coeffs_lower_projection {n m : Nat} (b : Matrix Rat n m) {i j : Fin n} (hji : ↑j < ↑i) : entry (coeffs b) i j = if ((basis b).row j).dotProduct ((basis b).row j) = 0 then 0 else (b.row i).dotProduct ((basis b).row j) / ((basis b).row j).dotProduct ((basis b).row j)

Strictly lower-triangular coefficient entries are the rational projection coefficient of the input row onto the earlier generated basis row.

theorem Hex.GramSchmidt.Rat.coeffs_lower_projection_comm {n m : Nat} (b : Matrix Rat n m) {i j : Fin n} (hji : ↑j < ↑i) : entry (coeffs b) i j = if ((basis b).row j).dotProduct ((basis b).row j) = 0 then 0 else ((basis b).row j).dotProduct (b.row i) / ((basis b).row j).dotProduct ((basis b).row j)

Lower coefficient entries, with the dot product oriented to match Mathlib's projection coefficient numerator.

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

The Gram-Schmidt basis is invariant under adding a scalar multiple of an earlier row to a later row. This is the rational size-reduction update used by the integer wrappers.

theorem Hex.GramSchmidt.Rat.basis_rowSwap_of_before {n m : Nat} (b : Matrix Rat 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 leaves every basis row before the pair unchanged, since each Gram-Schmidt output row depends only on the input prefix up to its own index.

theorem Hex.GramSchmidt.Rat.basis_rowSwap_adjacent_prev {n m : Nat} (b : Matrix Rat 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 the adjacent rows km1, k, the basis row at the lower index km1 becomes the old basis row k plus its projection coefficient times the old basis row km1. The explicit re-orthogonalization formula for the first vector of the swapped pair.

theorem Hex.GramSchmidt.Rat.basis_rowSwap_adjacent_curr {n m : Nat} (b : Matrix Rat 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 the adjacent rows km1, k (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. The companion of basis_rowSwap_adjacent_prev tracking how a swap rewrites the second vector of the pair.

theorem Hex.GramSchmidt.Rat.coeffs_rowSwap_adjacent_lower_prev {n m : Nat} (b : Matrix Rat 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, the coefficient at the lower row km1 against an earlier column j equals the old coefficient at row k against j: the swapped rows carry their lower coefficients with them.

theorem Hex.GramSchmidt.Rat.coeffs_rowSwap_adjacent_lower_curr {n m : Nat} (b : Matrix Rat 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: 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.Rat.coeffs_rowSwap_adjacent_pivot {n m : Nat} (b : Matrix Rat 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, in terms of the old projection coefficient and basis-row norms.

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

Under rowAdd b src dst c with src < dst, lower coefficients in the destination row update linearly below the pivot source column.

theorem Hex.GramSchmidt.Rat.coeffs_rowAdd_pivot {n m : Nat} (b : Matrix Rat n m) (src dst : Fin n) (hsrcdst : ↑src < ↑dst) (c : Rat) (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 rowAdd b src dst c with src < dst, the pivot coefficient in the destination row increases by c when the source basis row has nonzero norm.

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

Under rowAdd b src dst c with src < col < dst, destination-row coefficients above the pivot source column are preserved.

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

A row add only changes the destination row of the coefficient matrix.

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

Orthogonalization preserves the row space of each prefix: the first i + 1 rational basis rows span exactly the vectors spanned by the first i + 1 input rows.

theorem Hex.GramSchmidt.Rat.basis_rowSwap_of_after {n m : Nat} (b : Matrix Rat 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 leaves every basis row after the pair unchanged: the orthogonalized prefix beyond index k is recomputed from the same set of input rows.

theorem Hex.GramSchmidt.Rat.coeffs_rowSwap_adjacent_before {n m : Nat} (b : Matrix Rat 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.

theorem Hex.GramSchmidt.Rat.coeffs_rowSwap_adjacent_after_low {n m : Nat} (b : Matrix Rat 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.

theorem Hex.GramSchmidt.Rat.coeffs_rowSwap_adjacent_after_high {n m : Nat} (b : Matrix Rat 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.