theorem Hex.GramSchmidt.Int.scaledCoeffMatrix_rowAdd_pivot_det {n m : ℕ} (b : Matrix ℤ n m) (j k : Fin n) (hjk : ↑j < ↑k) (c : ℤ) : (scaledCoeffMatrix (b.rowAdd j k c) k j hjk).det = (scaledCoeffMatrix b k j hjk).det + c * (leadingGramMatrixInt b (↑j + 1) ⋯).det

Determinant-level pivot identity for scaled Gram-Schmidt coefficients under an elementary row addition. In the Cramer matrix computing nu[k,j], replacing row k by row k + c * row j changes the replaced last column linearly: the new determinant is the old Cramer determinant plus c times the leading Gram determinant. This formulation does not require the rational coefficient denominator to be nonzero.

theorem Hex.GramSchmidt.Int.leadingGramMatrixInt_rowAdd_outside {n m : ℕ} (b : Matrix ℤ n m) (j k : Fin n) (c : ℤ) (t : ℕ) (ht : t ≤ n) (hkt : t ≤ ↑k) : leadingGramMatrixInt (b.rowAdd j k c) t ht = leadingGramMatrixInt b t ht

When the modified row index k lies outside the leading t-prefix (t ≤ k.val), the leading Gram matrix of Matrix.rowAdd b j k c agrees with that of b. Internal support lemma for the row-add determinant theorem in HexGramSchmidtMathlib.Int.

theorem Hex.GramSchmidt.Int.leadingGramMatrixInt_rowAdd_inside {n m : ℕ} (b : Matrix ℤ n m) (j k : Fin n) (c : ℤ) (t : ℕ) (ht : t ≤ n) (hjk : ↑j < ↑k) (hkt : ↑k < t) : leadingGramMatrixInt (b.rowAdd j k c) t ht = ((leadingGramMatrixInt b t ht).rowAdd ⟨↑j, ⋯⟩ ⟨↑k, hkt⟩ c).colAdd ⟨↑j, ⋯⟩ ⟨↑k, hkt⟩ c

When the modified row index k lies inside the leading t-prefix (k.val < t), the leading Gram matrix of Matrix.rowAdd b j k c agrees with the row-and-column-add of the original leading Gram matrix at the lifted Fin t indices jt, kt. Internal support lemma for the row-add determinant theorem in HexGramSchmidtMathlib.Int.

theorem Hex.GramSchmidt.Int.scaledCoeffs_rowAdd_pivot {n m : ℕ} (b : Matrix ℤ n m) (j k : Fin n) (hjk : ↑j < ↑k) (c : ℤ) : entry (scaledCoeffs (b.rowAdd j k c)) k j = entry (scaledCoeffs b) k j + c * Int.ofNat (gramDet b (↑j + 1) ⋯)

The executable scaled-coefficient pivot entry changes predictably under an earlier-row addition. This packages the Cramer/Bareiss pivot identity at the public scaledCoeffs level so update callers need not unfold the underlying determinant identity directly.

theorem Hex.GramSchmidt.Int.gramDet_rowAdd_earlier {n m : ℕ} (b : Matrix ℤ n m) (j k : Fin n) (c : ℤ) (t : ℕ) (ht : t ≤ n) (hjk : ↑j < ↑k) : gramDet (b.rowAdd j k c) t ht = gramDet b t ht

Adding a multiple of an earlier row to a later row leaves the leading Gram determinant unchanged. The hypothesis j.val < k.val makes the source row earlier than the destination row in the basis.

theorem Hex.GramSchmidt.Int.scaledCoeffs_rowAdd_lower {n m : ℕ} (b : Matrix ℤ n m) (l j k : Fin n) (hlj : ↑l < ↑j) (hjk : ↑j < ↑k) (c : ℤ) : entry (scaledCoeffs (b.rowAdd j k c)) k l = entry (scaledCoeffs b) k l + c * entry (scaledCoeffs b) j l

Under Matrix.rowAdd b j k c with l.val < j.val < k.val, the destination-row scaled coefficient at column l updates by the linear combination (scaledCoeffs b)[k][l] + c * (scaledCoeffs b)[j][l].

theorem Hex.GramSchmidt.Int.scaledCoeffs_rowAdd_other_row {n m : ℕ} (b : Matrix ℤ n m) (j k : Fin n) (hjk : ↑j < ↑k) (c : ℤ) (i : Fin n) (hik : i ≠ k) : (scaledCoeffs (b.rowAdd j k c)).row i = (scaledCoeffs b).row i

Under Matrix.rowAdd b j k c with j.val < k.val, every row of scaledCoeffs other than the destination row k is preserved.

theorem Hex.GramSchmidt.Int.scaledCoeffs_rowAdd_above_pivot {n m : ℕ} (b : Matrix ℤ n m) (j k : Fin n) (hjk : ↑j < ↑k) (c : ℤ) (l : Fin n) (hjl : ↑j < ↑l) (hlk : ↑l < ↑k) : entry (scaledCoeffs (b.rowAdd j k c)) k l = entry (scaledCoeffs b) k l

Under Matrix.rowAdd b j k c with j.val < l.val < k.val, the destination-row scaled coefficient at column l between the source column and the pivot is preserved.

theorem Hex.GramSchmidt.Int.independent_of_det_positive {n m : ℕ} (b : Matrix ℤ n m) (hdet : ∀ (k : ℕ) (hk : k ≤ n), 0 < k → 0 < (b.gramMatrix.principalSubmatrix k hk).det) : independent b

A determinant-positive leading-Gram-prefix proof induces the executable gramDet independence predicate. This is useful for callers that already have determinant lemmas for special matrix families, while keeping the public predicate stated over Mathlib-free computed data.

theorem Hex.GramSchmidt.Int.independent_identity {n : ℕ} : independent (Matrix.identity n)

The identity matrix is independent: its Gram matrix is the identity, so every leading principal minor has determinant 1 > 0.

theorem Hex.GramSchmidt.Int.principalSubmatrix_gram_bareiss_eq_zero_of_singularStep_lt {n m : ℕ} (b : Matrix ℤ n m) (r : ℕ) (hr : r < n) (s : ℕ) (h_sing : (Matrix.noPivotLoop r b.gramMatrix.noPivotInitialState).singularStep = some s) : (b.gramMatrix.principalSubmatrix (r + 1) ⋯).bareiss = 0

Singular-branch zero propagation: if the partial-pass no-pivot Bareiss loop on the full Gram matrix records a singular step at index s strictly before slot r + 1, the public row-pivoted Bareiss determinant of the (r + 1) leading Gram prefix is zero.

This is the supporting lemma needed by the singular branch of the gramDetVecEntry_eq_principalSubmatrix_bareiss placeholder: both sides vanish in this case, and this lemma supplies the right-hand side. The proof composes the new lemma HexMatrixMathlib.noPivotLoop_invariant_of_singularStep_eq_none (to identify det(principalSubmatrix _ (s+1)) = 0 at the moment of singularity) with the unconditional gramDet_eq_prod_normSq_uncond and the multiplicative succession gramSchmidtNormProduct_succ to propagate zero from s + 1 to r + 1.

theorem Hex.GramSchmidt.Int.gramDetVecEntry_eq_principalSubmatrix_bareiss {n m : ℕ} (b : Matrix ℤ n m) (r : ℕ) (hr : r < n) : gramDetVecEntry b.gramMatrix.bareissNoPivotData ⟨r + 1, ⋯⟩ = (b.gramMatrix.principalSubmatrix (r + 1) ⋯).bareiss.toNat

The no-pivot Bareiss pass over the full Gram matrix records, at slot r + 1, the same leading-prefix determinant as the public row-pivoted Bareiss surface on that prefix.

This theorem lives in HexGramSchmidtMathlib because the proof path for the singular branch identifies the executable determinant with Mathlib's Leibniz determinant. Mathlib-free callers should use the executable gramDet API instead of depending on this Bareiss-facing statement.