5.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 one casting its input into Rat first.

def

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

The Gram-Schmidt orthogonal basis for a rational matrix.

def

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

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

def

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

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

def

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

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

The basis and coefficient matrices are noncomputable (their entries involve division), so they are documented here by signature. The integer namespace adds two computable operations that stay in exact arithmetic. 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.

def

Hex.GramSchmidt.Int.gramDet {n m : Nat} (b : Hex.Matrix Int n m)
  (k : Nat) (hk : k ≤ n) : Nat
Hex.GramSchmidt.Int.gramDet {n m : Nat}
  (b : Hex.Matrix Int n m) (k : Nat)
  (hk : k ≤ n) : Nat

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

def

Hex.GramSchmidt.Int.scaledCoeffs {n m : Nat} (b : Hex.Matrix Int n m) :
  Hex.Matrix Int n n
Hex.GramSchmidt.Int.scaledCoeffs
  {n m : Nat} (b : Hex.Matrix Int n m) :
  Hex.Matrix Int 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. scaledCoeffs projects out its coefficient matrix.

5.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 and the scaled coefficient matrix, then applies a size-reduction row operation.

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 : Matrix Int 3 3 :=
  Matrix.ofFn fun i j =>
    match i.val, j.val with
    | 0, 0 => 1
    | 0, 1 => 1
    | 1, 0 => 1
    | 1, 2 => 1
    | 2, 1 => 1
    | 2, 2 => 1
    | _, _ => 0

private abbrev i0 : Fin 3 := ⟨0, by⊢ 0 < 3 decideAll goals completed! 🐙⟩
private abbrev i1 : Fin 3 := ⟨1, by⊢ 1 < 3 decideAll goals completed! 🐙⟩
private abbrev i2 : Fin 3 := ⟨2, by⊢ 2 < 3 decideAll goals completed! 🐙⟩

-- 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 (by⊢ 0 ≤ 3 decideAll goals completed! 🐙) = 1
#guard gramDet m 1 (by⊢ 1 ≤ 3 decideAll goals completed! 🐙) = 2
#guard gramDet m 2 (by⊢ 2 ≤ 3 decideAll goals completed! 🐙) = 3
#guard gramDet m 3 (by⊢ 3 ≤ 3 decideAll goals completed! 🐙) = 4

-- scaledCoeffs stores d_{j+1} on the diagonal ...
#guard entry (scaledCoeffs m) i0 i0 = 2
#guard entry (scaledCoeffs m) i1 i1 = 3
#guard entry (scaledCoeffs m) i2 i2 = 4
-- ... the integral coefficients d_{j+1} * μ_{i,j}
-- strictly below it ...
#guard entry (scaledCoeffs m) i1 i0 = 1
#guard entry (scaledCoeffs m) i2 i0 = 1
#guard entry (scaledCoeffs m) i2 i1 = 1
-- ... and zeros above the diagonal.
#guard entry (scaledCoeffs m) i0 i1 = 0
#guard entry (scaledCoeffs m) i1 i2 = 0

-- Size-reducing row 2 against row 0 by 2 replaces
-- b[2] with b[2] - 2·b[0]; here entry (2,0) drops
-- to -2 and the diagonal entry (2,2) is untouched.
#guard entry (sizeReduce m i0 i2 2) i2 i0 = -2
#guard entry (sizeReduce m i0 i2 2) i2 i2 = 1

end HexGramSchmidtChapter