Mathlib-side determinantal identification of the canonical Bareiss Gram-Schmidt coefficients for hex-gram-schmidt.

This module finishes the Cramer identity scaledCoeffMatrix_det_eq_gramDet_mul_coeffs, expressing the scaled coefficient determinant as gramDet (j+1) * coeffs[i][j]. Its second half introduces the augmented (n+1) × (n+1) matrix augmentedGram, whose upper block is gramMatrix b and whose trailing column carries a standard basis vector, and proves noPivotLoop_augmentedGram_invariant: the no-pivot Bareiss pass on the augmented matrix mirrors the pass on gramMatrix b while its trailing column tracks bareissGramCanonicalCoeff. This yields bareissGramCanonicalCoeff_eq_augmentedGram_entry and its bordered-minor form, identifying the canonical row coefficients with a Bareiss minor determinant.

Augmented Gram matrix for determinantal identification of

bareissGramCanonicalCoeff

The canonical row-coefficient vector of the initial no-pivot Bareiss trajectory on gramMatrix b is identified with a trailing-column entry of the no-pivot Bareiss pass on an (n + 1) × (n + 1) augmented matrix. The upper n × n block of the augmented matrix is gramMatrix b; the trailing column at upper rows carries the standard basis vector δ_a at the chosen coefficient slot a; the trailing row is structurally zero.

Because the trailing row is zero and the no-pivot Bareiss update at slot (i, j) with i, j < n only consults the upper block, the upper-block trajectory on the augmented matrix exactly mirrors the trajectory on gramMatrix b. Because the trailing-column update at row i < n and step k < i.val mirrors the canonical-coefficient Bareiss step, the trailing column at upper rows tracks bareissGramCanonicalCoeff b fuel i at slot a.

def Hex.GramSchmidt.Int.augmentedGram {n m : ℕ} (b : Matrix ℤ n m) (a : Fin n) : Matrix ℤ (n + 1) (n + 1)

Augmented (n + 1) × (n + 1) matrix used to identify bareissGramCanonicalCoeff b fuel i [a] with a trailing-column entry of the no-pivot Bareiss pass. Upper block is gramMatrix b; trailing column at upper rows is the standard basis vector δ_a; trailing row is zero.

Equations

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

theorem Hex.GramSchmidt.Int.augmentedGram_upper_block {n m : ℕ} (b : Matrix ℤ n m) (a i j : Fin n) : (augmentedGram b a)[⟨↑i, ⋯⟩][⟨↑j, ⋯⟩] = b.gramMatrix[i][j]

Upper-block entry of augmentedGram b a agrees with gramMatrix b.

theorem Hex.GramSchmidt.Int.augmentedGram_trailing_col {n m : ℕ} (b : Matrix ℤ n m) (a i : Fin n) : (augmentedGram b a)[⟨↑i, ⋯⟩][Fin.last n] = if i = a then 1 else 0

Trailing-column entry of augmentedGram b a at an upper row i : Fin n is 1 when i = a and 0 otherwise.

theorem Hex.GramSchmidt.Int.augmentedGram_trailing_row {n m : ℕ} (b : Matrix ℤ n m) (a : Fin n) (j : Fin (n + 1)) : (augmentedGram b a)[Fin.last n][j] = 0

Trailing-row entries of augmentedGram b a are all zero.

theorem Hex.GramSchmidt.Int.trailing_eq_at_step_local {n' : ℕ} {M : Matrix ℤ n' n'} {state : Matrix.BareissState n'} (hinv : HexMatrixMathlib.BareissNoPivotInvariant M state) (s : ℕ) (hs : s < n') (hstep : s = state.step) (a c : Fin n') (hsa : s ≤ ↑a) (hsc : s ≤ ↑c) : state.matrix[a][c] = (M.borderedMinor s hs a c).det

Local copy of HexMatrixMathlib.trailing_eq_at_step (private there): re-state BareissNoPivotInvariant.trailing_eq with the step value supplied externally so the dependent bordered-minor type matches the desired s = state.step substitution cleanly.

theorem Hex.GramSchmidt.Int.noPivotLoop_augmentedGram_invariant {n m : ℕ} (b : Matrix ℤ n m) (a : Fin n) (fuel : ℕ) : fuel + 1 ≤ n → (Matrix.noPivotLoop fuel b.gramMatrix.noPivotInitialState).singularStep = none → (Matrix.noPivotLoop fuel (augmentedGram b a).noPivotInitialState).step = (Matrix.noPivotLoop fuel b.gramMatrix.noPivotInitialState).step ∧ (Matrix.noPivotLoop fuel (augmentedGram b a).noPivotInitialState).prevPivot = (Matrix.noPivotLoop fuel b.gramMatrix.noPivotInitialState).prevPivot ∧ (Matrix.noPivotLoop fuel (augmentedGram b a).noPivotInitialState).singularStep = none ∧ (∀ (i j : Fin n), (Matrix.noPivotLoop fuel (augmentedGram b a).noPivotInitialState).matrix[⟨↑i, ⋯⟩][⟨↑j, ⋯⟩] = (Matrix.noPivotLoop fuel b.gramMatrix.noPivotInitialState).matrix[i][j]) ∧ ∀ (i : Fin n), (Matrix.noPivotLoop fuel (augmentedGram b a).noPivotInitialState).matrix[⟨↑i, ⋯⟩][Fin.last n] = (bareissGramCanonicalCoeff b fuel i)[a]

Combined invariant relating the no-pivot Bareiss trajectory on the augmented matrix to the trajectory on gramMatrix b. Under fuel + 1 ≤ n and a non-singular prefix on the Gram side, the augmented loop tracks the Gram loop on (i) step, (ii) prevPivot, (iii) the upper n × n block, and (iv) carries the canonical row coefficient in its trailing column.

theorem Hex.GramSchmidt.Int.bareissGramCanonicalCoeff_eq_augmentedGram_entry {n m : ℕ} (b : Matrix ℤ n m) (fuel : ℕ) (i a : Fin n) (hfuel : fuel ≤ ↑i) (h_no_sing : (Matrix.noPivotLoop fuel b.gramMatrix.noPivotInitialState).singularStep = none) : (bareissGramCanonicalCoeff b fuel i)[a] = (Matrix.noPivotLoop fuel (augmentedGram b a).noPivotInitialState).matrix[⟨↑i, ⋯⟩][Fin.last n]

Determinantal identification of the canonical row-coefficient vector bareissGramCanonicalCoeff b fuel i at slot a as the trailing-column entry of the no-pivot Bareiss pass on the augmented (n + 1) × (n + 1) matrix augmentedGram b a. The hypothesis fuel ≤ i.val ensures the comparison covers both the active-row and processed-row branches of the canonical recursion.

theorem Hex.GramSchmidt.Int.bareissGramCanonicalCoeff_eq_borderedMinor_aug {n m : ℕ} (b : Matrix ℤ n m) (fuel : ℕ) (i a : Fin n) (hfuel : fuel ≤ ↑i) (h_no_sing : (Matrix.noPivotLoop fuel b.gramMatrix.noPivotInitialState).singularStep = none) : (bareissGramCanonicalCoeff b fuel i)[a] = ((augmentedGram b a).borderedMinor fuel ⋯ ⟨↑i, ⋯⟩ (Fin.last n)).det

Direct bordered-minor form: the canonical row-coefficient vector at slot a equals the determinant of the (fuel + 1) × (fuel + 1) bordered minor of the augmented Gram matrix. Composes bareissGramCanonicalCoeff_eq_augmentedGram_entry with the Bareiss no-pivot invariant trailing_eq.

theorem Hex.GramSchmidt.Int.noPivotLoop_initial_step_eq_and_fuel_succ_le {n' : ℕ} (M : Matrix ℤ n' n') (fuel : ℕ) (h_no_sing : (Matrix.noPivotLoop fuel M.noPivotInitialState).singularStep = none) (hnext : (Matrix.noPivotLoop fuel M.noPivotInitialState).step + 1 < n') : (Matrix.noPivotLoop fuel M.noPivotInitialState).step = fuel ∧ fuel + 1 ≤ n'

Under a non-singular no-pivot Bareiss prefix that has not yet reached the terminal step, the loop on the initial state of M consumed exactly fuel regular iterations: the resulting step equals fuel, and fuel + 1 ≤ n'.

theorem Hex.GramSchmidt.Int.prevPivot_eq_at_step_local {n' : ℕ} {M : Matrix ℤ n' n'} {state : Matrix.BareissState n'} (hinv : HexMatrixMathlib.BareissNoPivotInvariant M state) (s : ℕ) (hs : s ≤ n') (hstep : s = state.step) : state.prevPivot = (M.principalSubmatrix s hs).det

Companion to trailing_eq_at_step_local: rewrite BareissNoPivotInvariant.prevPivot_eq with the step value supplied externally so the dependent principalSubmatrix type matches the desired s = state.step substitution cleanly.

def Hex.GramSchmidt.Int.StepWitness.ofGram {n m : ℕ} (b : Matrix ℤ n m) : StepWitness b

Concrete bridge-side instance of StepWitness for any integer basis.

The witness quotient at slot a is the next iteration's canonical row coefficient (bareissGramCanonicalCoeff b (fuel + 1) i)[a]. Integrality of this quotient comes from the Bareiss-Desnanot identity applied to the augmented (n + 1) × (n + 1) matrix augmentedGram b a: the canonical coefficients identify with trailing-column entries of the augmented no-pivot Bareiss pass (bareissGramCanonicalCoeff_eq_borderedMinor_aug), and the Bareiss step recurrence on the augmented matrix supplies the exact-division multiplicative identity.

Equations

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

theorem Hex.GramSchmidt.Int.scaledCoeffMatrix_det_eq_zero_of_singularStep_lt {n m : ℕ} (b : Matrix ℤ n m) (i j : Fin n) (hji : ↑j < ↑i) (s : ℕ) (h_sing : (Matrix.noPivotLoop (↑j) b.gramMatrix.noPivotInitialState).singularStep = some s) : (scaledCoeffMatrix b i j hji).det = 0

Cramer's rule identity under singularity. When the no-pivot Bareiss pass over the Gram matrix records an early singular step before reaching column j, the Leibniz determinant of the Cramer minor scaledCoeffMatrix b i j hji is zero. Internally lifts the partial-pass singularity to the full bareissNoPivotData pass, traverses gramDetVecEntry to conclude gramDet b (j+1) = 0, and finishes via the Cramer determinant identity scaledCoeffMatrix_det_eq_gramDet_mul_coeffs.

theorem Hex.GramSchmidt.Int.scaledCoeffs_lower_eq_det_scaledCoeffMatrix {n m : ℕ} (b : Matrix ℤ n m) (i j : Fin n) (hji : ↑j < ↑i) : ↑(entry (scaledCoeffs b) i j) = ↑(scaledCoeffMatrix b i j hji).det

Unconditional rational closed form for the strictly lower entries of scaledCoeffs: the executable integer scaled coefficient agrees with the Leibniz determinant of the Cramer minor scaledCoeffMatrix b i j hji, regardless of whether the no-pivot Bareiss pass over gramMatrix b reaches column j without recording a singular step. The non-singular branch composes the Mathlib-free correspondence scaledCoeffs_lower_eq_noPivotLoop_scaledCoeffMatrix (via noPivotLoop_full_eq_borderedMinor_at_trailing + scaledCoeffMatrix_eq_borderedMinor) with bareiss_eq_noPivotLoop_last_of_no_singular and the bareiss_eq_mathlib_det / det_eq cross-bridge; the singular branch sends both sides to 0 via the singular cascade. All Mathlib-side bridge theorems for strictly lower entries route through this unconditional identity.

theorem Hex.GramSchmidt.Int.scaledCoeffs_eq_scaledCoeffMatrix_bareiss {n m : ℕ} (b : Matrix ℤ n m) (i j : Fin n) (hji : ↑j < ↑i) : entry (scaledCoeffs b) i j = (scaledCoeffMatrix b i j hji).bareiss

Cramer/Bareiss identity: below the diagonal, the integral scaled Gram-Schmidt coefficient is exactly the public Bareiss determinant of the Cramer minor scaledCoeffMatrix. Derived from the unconditional scaledCoeffs_lower_eq_det_scaledCoeffMatrix by casting back to Int and translating Matrix.det to Matrix.bareiss via det_eq / bareiss_eq_mathlib_det.

theorem Hex.GramSchmidt.Int.scaledCoeffs_eq {n m : ℕ} (b : Matrix ℤ n m) (i j : ℕ) (hi : i < n) (hj : j < i) : ↑(entry (scaledCoeffs b) ⟨i, hi⟩ ⟨j, ⋯⟩) = ↑(gramDet b (j + 1) ⋯) * entry (coeffs b) ⟨i, hi⟩ ⟨j, ⋯⟩

Below the diagonal, the rational image of the integer scaled Gram-Schmidt coefficient factors as gramDet b (j+1) * coeffs[i,j]. Derived from the unconditional scaledCoeffs_lower_eq_det_scaledCoeffMatrix and scaledCoeffMatrix_det_eq_gramDet_mul_coeffs.