16.2. Fundamental operations🔗

The two fundamental constructions are the orthogonal basis and the coefficient matrix. The basis rows are mutually orthogonal. The coefficient matrix is lower-unitriangular and reconstructs the input as coeffs · basis. Both come in a rational and an integer flavour; the integer flavour orthogonalizes over Rat, so like the rational one it is noncomputable and exists to state theorems, not to run.

def

Hex.GramSchmidt.Rat.basis {n m : ℕ} (b : Hex.Matrix ℚ n m) :
  Hex.Matrix ℚ n m
Hex.GramSchmidt.Rat.basis {n m : ℕ}
  (b : Hex.Matrix ℚ n m) :
  Hex.Matrix ℚ n m

The Gram-Schmidt orthogonal basis for a rational matrix.

def

Hex.GramSchmidt.Rat.coeffs {n m : ℕ} (b : Hex.Matrix ℚ n m) :
  Hex.Matrix ℚ n n
Hex.GramSchmidt.Rat.coeffs {n m : ℕ}
  (b : Hex.Matrix ℚ n m) :
  Hex.Matrix ℚ n n

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

def

Hex.GramSchmidt.Int.basis {n m : ℕ} (b : Hex.Matrix ℤ n m) :
  Hex.Matrix ℚ n m
Hex.GramSchmidt.Int.basis {n m : ℕ}
  (b : Hex.Matrix ℤ n m) :
  Hex.Matrix ℚ n m

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

def

Hex.GramSchmidt.Int.coeffs {n m : ℕ} (b : Hex.Matrix ℤ n m) :
  Hex.Matrix ℚ n n
Hex.GramSchmidt.Int.coeffs {n m : ℕ}
  (b : Hex.Matrix ℤ n m) :
  Hex.Matrix ℚ n n

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

Both matrices are noncomputable, because their entries involve division; they are stated by signature here, and their role is to be the subject of theorems rather than something you evaluate. What you actually compute with is the pair of exact-integer operations the integer namespace adds. The leading Gram determinants are the determinants of the leading principal Gram minors B Bᵀ (the squared volumes of the prefix sublattices). The scaled coefficient matrix clears the denominators of the rational coefficients against them, so every entry is again an integer.

def

Hex.GramSchmidt.Int.gramDet {n m : ℕ} (b : Hex.Matrix ℤ n m) (k : ℕ)
  (hk : k ≤ n := by omega) : ℕ
Hex.GramSchmidt.Int.gramDet {n m : ℕ}
  (b : Hex.Matrix ℤ n m) (k : ℕ)
  (hk : k ≤ n := by omega) : ℕ

The k-th Gram determinant: the determinant of the k × k leading principal Gram matrix of the integer input.

The bound hk : k ≤ n defaults to by omega, so callers with a concrete k and n (as in #guards and examples) can omit it.

def

Hex.GramSchmidt.Int.scaledCoeffs {n m : ℕ} (b : Hex.Matrix ℤ n m) :
  Hex.Matrix ℤ n n
Hex.GramSchmidt.Int.scaledCoeffs {n m : ℕ}
  (b : Hex.Matrix ℤ n m) :
  Hex.Matrix ℤ n n

Integral scaled Gram-Schmidt coefficients. For j < i, the entry is the determinant formula corresponding to d_{j+1} * μ_{i,j}; on the diagonal we store d_{j+1}, and entries above the diagonal are zero.

The scaled coefficients are packaged together with the Gram-determinant vector inside Hex.GramSchmidt.Int.Data. Hex.GramSchmidt.Int.scaledCoeffs projects out its coefficient matrix.

16.2.1. Worked example: Gram determinants and scaled coefficients🔗

The block below works over the integer matrix with rows (1,1,0), (1,0,1), (0,1,1). It reads off the leading Gram determinants, prints the whole scaled coefficient matrix, and applies a size-reduction row operation. The Hex.GramSchmidt.Int.gramDet bound is filled by its by omega autoparam, so the calls need no explicit proof.

open Hex Hex.GramSchmidt Hex.GramSchmidt.Int

namespace HexGramSchmidtChapter

-- A 3×3 integer matrix with rows
--   (1,1,0), (1,0,1), (0,1,1).
private def m : Hex.Matrix Int 3 3 :=
  #m[1, 1, 0; 1, 0, 1; 0, 1, 1]

-- Leading Gram determinants d_0 .. d_3. The empty
-- prefix is 1 by convention; d_k is the determinant
-- of the k×k leading Gram minor of the input.
#guard gramDet m 0 = 1
#guard gramDet m 1 = 2
#guard gramDet m 2 = 3
#guard gramDet m 3 = 4

-- scaledCoeffs stores d_{j+1} on the diagonal, the
-- integral coefficients d_{j+1}·μ_{i,j} strictly
-- below it, and zeros above.
#m[2, 0, 0;
   1, 3, 0;
   1, 1, 4]#eval scaledCoeffs m

-- Size-reducing row 2 against row 0 by 2 replaces
-- b[2] = (0,1,1) with b[2] - 2·b[0] = (-2,-1,1).
#guard (sizeReduce m 0 2 2).row 2 = #v[-2, -1, 1]

end HexGramSchmidtChapter

#m[2, 0, 0;
   1, 3, 0;
   1, 1, 4]