Scaled-coefficient and Gram-determinant surface for hex-gram-schmidt.

This module packages the executable scaled Gram-Schmidt output: the Data record bundling the leading Gram determinant vector d with the scaled coefficient matrix ν, produced by data from a single scaledCoeffRowsSchur pass, and exposed as the public gramDetVec and scaledCoeffs. It proves the per-row Schur kernel agrees with the reference scaledCoeffRows formulation (schurSigma_congr and the column/boundary frame lemmas), and develops the Bareiss commutation infrastructure the determinant correspondence rests on: a Matrix.stepMatrix step commutes with taking a principalSubmatrix and with taking a trailing borderedMinor (principalSubmatrix_stepMatrix_eq, borderedMinor_stepMatrix_eq), the no-pivot loop stays synchronized across a matrix and its bordered minor (noPivotLoop_full_eq_borderedMinor_at_trailing), it preserves trailing-block symmetry, and its step/singularStep bookkeeping is monotone and stable under prefixing.

structure Hex.GramSchmidt.Int.Data (n : Nat) : Type

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.

• d : Vector Nat (n + 1)
• ν : Matrix Int n n

def Hex.GramSchmidt.Int.gramDetVecFromScaledCoeffRows {n : Nat} (rows : Array (Array Int)) : Vector Nat (n + 1)

Equations

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

def Hex.GramSchmidt.Int.data {n m : Nat} (b : Matrix Int n m) : Data n

Run the per-row Schur scaled-coefficient kernel once and package both the leading Gram determinant vector and the scaled Gram-Schmidt coefficient matrix.

Equations

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

def Hex.GramSchmidt.Int.gramDetVec {n m : Nat} (b : Matrix Int n m) : Vector Nat (n + 1)

All leading Gram determinants, starting with the empty-prefix value d₀ = 1.

Equations

• Hex.GramSchmidt.Int.gramDetVec b = (Hex.GramSchmidt.Int.data b).d

def Hex.GramSchmidt.Int.scaledCoeffs {n m : Nat} (b : Matrix Int n m) : 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.

Equations

• Hex.GramSchmidt.Int.scaledCoeffs b = (Hex.GramSchmidt.Int.data b).ν

theorem Hex.GramSchmidt.Int.scaledCoeffs_entry_eq_getArrayEntry {n m : Nat} (b : Matrix Int n m) (i j : Fin n) : entry (scaledCoeffs b) i j = getArrayEntry (scaledCoeffRowsSchur b) ↑i ↑j

Entry-level packaging equation from the public scaled-coefficient matrix back to the shared array pass that computes it.

theorem Hex.GramSchmidt.Int.noPivotLoop_full_eq_borderedMinor_at_trailing {n : Nat} (M : Matrix Int n n) (k : Nat) (hk : k < n) (row col : Fin n) (hrow : k ≤ ↑row) (hcol : k ≤ ↑col) : have BM := M.borderedMinor k hk row col; have s_full := Matrix.noPivotLoop k M.noPivotInitialState; have s_bm := Matrix.noPivotLoop k BM.noPivotInitialState; s_full.matrix[row][col] = s_bm.matrix[Fin.last k][Fin.last k] ∧ s_full.singularStep = s_bm.singularStep

The (row, col) entry of the noPivot Bareiss state after k iterations on the full n × n matrix agrees with the (Fin.last k, Fin.last k) entry of the noPivot Bareiss state after k iterations on the (k + 1) × (k + 1) bordered minor at row, col. The singularStep bookkeeping also agrees, mirroring the leading-prefix sync corollary. Requires row, col to lie in the trailing block.

theorem Hex.GramSchmidt.Int.noPivotLoop_id_at_singular_fixedpoint {n : Nat} (fuel : Nat) (state : Matrix.BareissState n) (hDone : state.step + 1 < n) (hp : state.matrix[⟨state.step, ⋯⟩][⟨state.step, ⋯⟩] = 0) (hsing : state.singularStep = some state.step) : Matrix.noPivotLoop fuel state = state

Once the no-pivot Bareiss loop has marked the current step singular (state.singularStep = some state.step with a zero pivot at that step), any further fuel is a no-op.

theorem Hex.GramSchmidt.Int.noPivotLoop_add {n : Nat} (a b : Nat) (state : Matrix.BareissState n) : Matrix.noPivotLoop (a + b) state = Matrix.noPivotLoop b (Matrix.noPivotLoop a state)

Fuel composition for the no-pivot Bareiss loop: running a + b units of fuel from state equals running b more units after a initial units.

theorem Hex.GramSchmidt.Int.noPivotLoop_singular_inv {n : Nat} (fuel : Nat) (state : Matrix.BareissState n) (h_init : state.singularStep = none) : (Matrix.noPivotLoop fuel state).singularStep = none ∨ ∃ (k : Fin n), (Matrix.noPivotLoop fuel state).singularStep = some ↑k ∧ (Matrix.noPivotLoop fuel state).step = ↑k ∧ (Matrix.noPivotLoop fuel state).matrix[k][k] = 0 ∧ ↑k + 1 < n

After running noPivotLoop from a state without a recorded singular step, the result has either no singular step, or it has a singular step that matches the current step field together with a zero pivot at that position.

theorem Hex.GramSchmidt.Int.noPivotLoop_singularStep_lt {n : Nat} (fuel : Nat) (state : Matrix.BareissState n) (h_init : state.singularStep = none) (s : Nat) (h_sing : (Matrix.noPivotLoop fuel state).singularStep = some s) : s < state.step + fuel

When the no-pivot Bareiss loop starts from a non-singular state and records a singular step within fuel iterations, the recorded singular index is strictly bounded by the initial step plus the fuel. The singular branch sets singularStep := some state.step at the trigger iteration, and state.step advances by at most one per regular iteration; with fuel iterations available and at least one used for the singular trigger, the recorded index is `< start

• fuel`.

theorem Hex.GramSchmidt.Int.noPivotLoop_step_monotone {n : Nat} (fuel : Nat) (state : Matrix.BareissState n) : state.step ≤ (Matrix.noPivotLoop fuel state).step

The step field of a no-pivot Bareiss state never decreases under further loop iterations.

theorem Hex.GramSchmidt.Int.bareissNoPivotData_diag_eq_principalSubmatrix_bareiss_of_prefix_nonsingular {n m : Nat} (b : Matrix Int n m) (r : Nat) (hr : r < n) (h_nonsing : (Matrix.noPivotLoop r b.gramMatrix.noPivotInitialState).singularStep = none) : b.gramMatrix.bareissNoPivotData.matrix[⟨r, hr⟩][⟨r, hr⟩] = (b.gramMatrix.principalSubmatrix (r + 1) ⋯).bareiss

Signed diagonal projection for a non-singular target prefix: the final no-pivot full-Gram diagonal at r is the public Bareiss determinant of the (r + 1) leading prefix.