Row-add determinant helper lemmas

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.

scaledCoeffs row-by-row updates under earlier-row addition

The three theorems below package the scaled-coefficient update under Matrix.rowAdd b j k c with j.val < k.val at each below-diagonal column position (left of the pivot, the row that is unchanged when not the destination, and strictly between the source and the pivot column). They mirror the pattern of scaledCoeffs_rowAdd_pivot and let the LLLState.sizeReduceColumn proof-field discharges in HexLLL/Basic.lean work against rowAdd directly, without reaching for the Mathlib-side scaledCoeffs_sizeReduce_* wrappers in HexGramSchmidt/Update.lean.

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.

Determinant-backed independence

These determinant-positivity lemmas for gramDet live in HexGramSchmidtMathlib because their proofs identify gramDet with the Leibniz determinant of the leading Gram matrix via the composition of HexMatrixMathlib.bareiss_eq_mathlib_det and HexMatrixMathlib.det_eq.symm (packaged here as leadingGramMatrixInt_det_eq_gramDet_int). Callers that already have a determinant lemma for a special matrix family can produce the public independent predicate stated over Mathlib-free computed data.

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.

Singular-prefix zero propagation for the Gram-Bareiss surface

When the no-pivot Bareiss loop on a Gram matrix records a singular step at index s, the (s+1)-leading Gram prefix has zero determinant. By the multiplicative succession gramSchmidtNormProduct_succ, the same vanishing propagates to every larger prefix. This is the singular branch of the gramDetVecEntry_eq_principalSubmatrix_bareiss placeholder.

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

Capstone for the Gram determinant vector: 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.