Executable array/loop machinery for the integer scaled Gram-Schmidt pass in hex-gram-schmidt.

This module defines the integer-determinant surface (gramDet and independent, the leading Gram matrices (leadingGramMatrixInt/Rat), scaledCoeffMatrix, lattice membership memLattice, and the no-pivot Bareiss determinant reader gramDetVecEntry) together with the mutable row-major array kernel that computes the scaled coefficients fraction-free. The kernel includes the nested-array storage (gramRows, zeroRows, getArrayEntry/setArrayEntry, rowsToMatrix), the Bareiss-style elimination sweep stepScaledRows and column-writer writeScaledColumn, the driver scaledCoeffArrayLoop, the two formulations scaledCoeffRows (reference) and scaledCoeffRowsSchur (live per-row Schur recurrence, with schurSigma/schurScaledCoeffEntry), and a large body of frame/size bookkeeping lemmas plus the per-step correspondence rowsToMatrix_stepScaledRows_eq between the array update and Matrix.stepMatrix.

def Hex.GramSchmidt.liftFinLE {k n : Nat} (i : Fin k) (hk : k ≤ n) : Fin n

Promote an index into a shorter prefix to the ambient matrix height.

Equations

• Hex.GramSchmidt.liftFinLE i hk = ⟨↑i, ⋯⟩

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

Leading principal Gram matrix of the first k rows of an integer basis.

Equations

• Hex.GramSchmidt.leadingGramMatrixInt b k hk = Hex.Matrix.ofFn fun (i j : Fin k) => (b.row (Hex.GramSchmidt.liftFinLE i hk)).dotProduct (b.row (Hex.GramSchmidt.liftFinLE j hk))

theorem Hex.GramSchmidt.leadingGramMatrixInt_eq_principalSubmatrix_gram {n m : Nat} (b : Matrix Int n m) (k : Nat) (hk : k ≤ n) : leadingGramMatrixInt b k hk = b.gramMatrix.principalSubmatrix k hk

The Gram-Schmidt leading Gram matrix is the leading prefix of the full Gram matrix. This is the shape equation between the public gramDet API and the one-pass gramDetVec implementation.

def Hex.GramSchmidt.leadingGramMatrixRat {n m : Nat} (b : Matrix Rat n m) (k : Nat) (hk : k ≤ n) : Matrix Rat k k

Leading principal Gram matrix of the first k rows of a rational basis.

Equations

• Hex.GramSchmidt.leadingGramMatrixRat b k hk = Hex.Matrix.ofFn fun (i j : Fin k) => (b.row (Hex.GramSchmidt.liftFinLE i hk)).dotProduct (b.row (Hex.GramSchmidt.liftFinLE j hk))

def Hex.GramSchmidt.scaledCoeffMatrix {n m : Nat} (b : Matrix Int n m) (i j : Fin n) (hji : ↑j < ↑i) : Matrix Int (↑j + 1) (↑j + 1)

Determinant matrix used by the integral scaledCoeffs entry formula: take the leading j + 1 Gram matrix and replace its last column by the inner products with row i.

Equations

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

def Hex.GramSchmidt.Int.memLattice {n m : Nat} (b : Matrix Int n m) (v : Vector Int m) : Prop

Integer lattice membership in the row span of b. This mirrors the LLL predicate without making hex-gram-schmidt depend on the downstream LLL library.

Equations

• Hex.GramSchmidt.Int.memLattice b v = ∃ (c : Vector Int n), Hex.Matrix.vecMul c b = v

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

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.

Equations

• Hex.GramSchmidt.Int.gramDet b k hk = (Hex.GramSchmidt.leadingGramMatrixInt b k hk).bareiss.toNat

def Hex.GramSchmidt.Int.independent {n m : Nat} (b : Matrix Int n m) : Prop

Linear independence of the row prefix determinants used by the Gram-Schmidt theorem surface, stated over the Mathlib-free executable gramDet data.

Equations

• Hex.GramSchmidt.Int.independent b = ∀ (k : Fin n), 0 < Hex.GramSchmidt.Int.gramDet b (↑k + 1) ⋯

noncomputable def Hex.GramSchmidt.Int.gramSchmidtNormProduct {n m : Nat} (b : Matrix Int n m) (k : Nat) (hk : k ≤ n) : Rat

Product of the squared Gram-Schmidt basis norms along the first k rows.

Equations

• Hex.GramSchmidt.Int.gramSchmidtNormProduct b k hk = Fin.foldl k (fun (acc : Rat) (j : Fin k) => have jn := ⟨↑j, ⋯⟩; acc * ((Hex.GramSchmidt.Int.basis b).row jn).normSq) 1

def Hex.GramSchmidt.Int.bareissDiagNat {n : Nat} (data : Matrix.BareissData n) (r : Nat) (hr : r < n) : Nat

Read a diagonal entry from a Bareiss elimination matrix as a natural determinant value.

Equations

• Hex.GramSchmidt.Int.bareissDiagNat data r hr = data.matrix[(⟨r, hr⟩, ⟨r, hr⟩)].toNat

def Hex.GramSchmidt.Int.gramDetVecEntry {n : Nat} (data : Matrix.BareissData n) (k : Fin (n + 1)) : Nat

Read the k-th leading-principal determinant from one no-pivot Bareiss elimination pass over the full Gram matrix. This helper is only used for Gram matrices: once a leading row prefix is singular, every larger leading prefix is also singular, so all later leading determinants are zero.

Equations

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

theorem Hex.GramSchmidt.Int.gramDetVecEntry_noPivot_eq_zero_of_singularStep_lt {n m : Nat} (b : Matrix Int n m) (s r : Nat) (hr : r < n) (hsing : b.gramMatrix.bareissNoPivotData.singularStep = some s) (hs : s < r + 1) : gramDetVecEntry b.gramMatrix.bareissNoPivotData ⟨r + 1, ⋯⟩ = 0

Specialization of the encoded zero-tail fact to the no-pivot executable data used by the Gram determinant vector pass.

structure Hex.GramSchmidt.Int.ScaledCoeffArrayState : Type

Mutable loop state for the integer scaled Gram-Schmidt pass: the current step, the working matrix and coefficient arrays, and the previous Bareiss pivot.

• step : Nat
• matrix : Array (Array Int)
• coeffs : Array (Array Int)
• prevPivot : Int

@[inline]

def Hex.GramSchmidt.Int.getArrayEntry (rows : Array (Array Int)) (row col : Nat) : Int

Read entry (row, col) from a row-major nested array as rows[row]![col]!.

Equations

• Hex.GramSchmidt.Int.getArrayEntry rows row col = rows[row]![col]!

def Hex.GramSchmidt.Int.zeroRows (n : Nat) : Array (Array Int)

An n × n row-major nested array initialised to all zeros.

Equations

• Hex.GramSchmidt.Int.zeroRows n = Array.replicate n (Array.replicate n 0)

def Hex.GramSchmidt.Int.gramRows {n m : Nat} (b : Matrix Int n m) : Array (Array Int)

The Gram matrix of b packaged as a row-major nested integer array.

Equations

• Hex.GramSchmidt.Int.gramRows b = Array.ofFn fun (i : Fin n) => Array.ofFn fun (j : Fin n) => (b.row i).dotProduct (b.row j)

def Hex.GramSchmidt.Int.rowsToMatrix (rows : Array (Array Int)) (n : Nat) : Matrix Int n n

Reconstruct an n × n integer matrix from a row-major nested array, reading entry (i, j) as rows[i]![j]! (getArrayEntry). This converts the executable array passes back to the Matrix API; for the Gram rows it inverts gramRows, so rowsToMatrix (gramRows b) n = gramMatrix b.

Equations

• Hex.GramSchmidt.Int.rowsToMatrix rows n = Hex.Matrix.ofFn fun (i j : Fin n) => Hex.GramSchmidt.Int.getArrayEntry rows ↑i ↑j

def Hex.GramSchmidt.Int.setArrayEntry (rows : Array (Array Int)) (row col : Nat) (value : Int) : Array (Array Int)

Write value into entry (row, col) of a row-major nested array.

Equations

• Hex.GramSchmidt.Int.setArrayEntry rows row col value = rows.set! row (rows[row]!.set! col value)

def Hex.GramSchmidt.Int.writeScaledColumn (coeffs rows : Array (Array Int)) (n k : Nat) : Array (Array Int)

Write column k of the coefficient array, copying the matrix-column values from row k downward.

Equations

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

def Hex.GramSchmidt.Int.stepScaledRows (rows : Array (Array Int)) (n k : Nat) (pivot prevPivot : Int) : Array (Array Int)

Equations

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

def Hex.GramSchmidt.Int.scaledCoeffArrayLoop (n fuel : Nat) (state : ScaledCoeffArrayState) : ScaledCoeffArrayState

Equations

• One or more equations did not get rendered due to their size.
• Hex.GramSchmidt.Int.scaledCoeffArrayLoop n 0 state = state

def Hex.GramSchmidt.Int.scaledCoeffRows {n m : Nat} (b : Matrix Int n m) : Array (Array Int)

Run one no-pivot fraction-free Gram elimination and record each scaled coefficient column immediately before the elimination step zeroes it.

This is the reference formulation of the scaled-coefficient matrix, kept for proofs rather than execution. The live algorithm runs scaledCoeffRowsSchur (the per-row Schur recurrence below); getArrayEntry_scaledCoeffRowsSchur_eq proves the two agree entry-for-entry, and that bridge is what connects scaledCoeffRowsSchur to gramDet / scaledCoeffs. Do not remove this formulation as "unused": deleting it breaks the correctness proof of the live path.

Equations

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

def Hex.GramSchmidt.Int.schurSigma (rows : Array (Array Int)) (i j : Nat) : Int

Schur-complement σ-chain for the fraction-free scaled Gram-Schmidt recurrence. Each step divides by the previous diagonal pivot rows[p-1][p-1] via Matrix.exactDiv; that division is exact — the fraction-free Bareiss invariant guarantees the numerator is divisible by the pivot, so sigma stays an integer bounded by a minor determinant rather than growing as an unreduced fraction.

Equations

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

def Hex.GramSchmidt.Int.schurScaledCoeffEntry (rows gram : Array (Array Int)) (i j : Nat) : Int

Equations

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

def Hex.GramSchmidt.Int.scaledCoeffRowsSchur {n m : Nat} (b : Matrix Int n m) : Array (Array Int)

Per-row Schur-complement scaled Gram-Schmidt coefficient kernel.

Rows are filled from top to bottom; within row i, entries 0..i are written left to right. For j < i this writes the scaled coefficient ν[i][j]; for j = i the same recurrence writes the diagonal Gram determinant d_{i+1}.

Equations

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