Executable Gram-Schmidt orthogonalization kernel for hex-gram-schmidt.

This module is the rational core that the rest of the library builds on. It defines the projection primitives (projectionCoeff, subtractProjection), the per-row reduction reduceAgainstBasis, the left-to-right orthogonalization basisRows/basisMatrix, the coefficient matrix coeffMatrix, and the supporting entry/prefix helpers (entry, castIntMatrix, prefixCombination, prefixRows, prefixSpan). It also proves the foundational facts the correspondence proofs consume: pairwise orthogonality of basisRows, the residual/projection reconstruction identity, the leading-row equation, and the zero-norm degeneracy lemmas (a Rat vector with zero self-dot-product is the zero vector).

def Hex.GramSchmidt.projectionCoeff {m : Nat} (row basisRow : Vector Rat m) : Rat

Coefficient of the orthogonal projection of row onto basisRow. When the basis row has zero norm we use 0, which matches the degenerate case of Gram-Schmidt where the corresponding projection term vanishes.

Equations

• Hex.GramSchmidt.projectionCoeff row basisRow = if basisRow.dotProduct basisRow = 0 then 0 else row.dotProduct basisRow / basisRow.dotProduct basisRow

def Hex.GramSchmidt.subtractProjection {m : Nat} (row basisRow : Vector Rat m) : Vector Rat m

Subtract the projection of row onto basisRow.

Equations

• Hex.GramSchmidt.subtractProjection row basisRow = row - Hex.GramSchmidt.projectionCoeff row basisRow • basisRow

theorem Hex.GramSchmidt.dot_zero_of_dot_self_zero {m : Nat} (row v : Vector Rat m) (hzero : v.dotProduct v = 0) : row.dotProduct v = 0

Over Rat, a vector whose self-dot-product is zero is the zero vector, so its dot product with any other row also vanishes. Used to discharge the degenerate zero-norm basis row case when reasoning about orthogonality.

def Hex.GramSchmidt.reduceAgainstBasis {m : Nat} (basisRev : List (Vector Rat m)) (row : Vector Rat m) : Vector Rat m

Reduce a row against the previously constructed orthogonal basis rows.

Equations

• Hex.GramSchmidt.reduceAgainstBasis basisRev row = List.foldl Hex.GramSchmidt.subtractProjection row basisRev

def Hex.GramSchmidt.basisRowsAux {m : Nat} (basisRev pending : List (Vector Rat m)) : List (Vector Rat m)

Left-to-right Gram-Schmidt orthogonalization on a list of rows.

Equations

• Hex.GramSchmidt.basisRowsAux basisRev [] = basisRev.reverse
• Hex.GramSchmidt.basisRowsAux basisRev (row :: rows) = Hex.GramSchmidt.basisRowsAux (Hex.GramSchmidt.reduceAgainstBasis basisRev row :: basisRev) rows

def Hex.GramSchmidt.basisRows {m : Nat} (rows : List (Vector Rat m)) : List (Vector Rat m)

Left-to-right Gram-Schmidt orthogonalization on a matrix's rows.

Equations

• Hex.GramSchmidt.basisRows rows = Hex.GramSchmidt.basisRowsAux [] rows

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

Rebuild a matrix from its row list after Gram-Schmidt orthogonalization.

Equations

• Hex.GramSchmidt.basisMatrix b = { data := Vector.ofFn fun (i : Fin n) => (Hex.GramSchmidt.basisRows b.rows.toList)[↑i]! }

def Hex.GramSchmidt.coeffMatrix {n m : Nat} (rows basis : Matrix Rat n m) : Matrix Rat n n

Gram-Schmidt coefficient matrix for an already-cast rational input.

Equations

• Hex.GramSchmidt.coeffMatrix rows basis = Hex.Matrix.ofFn fun (i j : Fin n) => if _hlt : ↑j < ↑i then Hex.GramSchmidt.projectionCoeff (rows.getRow i) (basis.getRow j) else if i = j then 1 else 0

def Hex.GramSchmidt.entry {R : Type u_1} {n m : Nat} (M : Matrix R n m) (i : Fin n) (j : Fin m) : R

Access a dense matrix entry by row and column indices.

Equations

• Hex.GramSchmidt.entry M i j = (M.row i)[j]

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

Cast an integer matrix into the rational matrix space used by Gram-Schmidt.

Equations

• Hex.GramSchmidt.castIntMatrix b = { data := Vector.map (fun (row : Vector Int m) => Vector.map (fun (x : Int) => ↑x) row) b.rows }

def Hex.GramSchmidt.prefixCombination {n m : Nat} (coeffs : Matrix Rat n n) (basis : Matrix Rat n m) (i : Nat) (hi : i < n) : Vector Rat m

The prefix combination term used in the decomposition theorem shape.

Equations

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

def Hex.GramSchmidt.prefixRows {R : Type u_1} {n m : Nat} (M : Matrix R n m) (i : Nat) (hi : i < n) : Matrix R (i + 1) m

The row-prefix matrix containing rows 0 through i.

Equations

• Hex.GramSchmidt.prefixRows M i hi = { data := Vector.ofFn fun (j : Fin (i + 1)) => M.row ⟨↑j, ⋯⟩ }

def Hex.GramSchmidt.prefixSpan {n m : Nat} (M : Matrix Rat n m) (i : Nat) (hi : i < n) (v : Vector Rat m) : Prop

Executable row-span membership in the first i + 1 rows of a matrix.

Equations

• Hex.GramSchmidt.prefixSpan M i hi v = ∃ (c : Vector Rat (i + 1)), Hex.Matrix.vecMul c (Hex.GramSchmidt.prefixRows M i hi) = v