Prefix coefficient vector for integer row combinations

theorem Hex.GramSchmidt.Int.prefixSpan_basis_of_vecMul {n m : Nat} (b : Matrix Int n m) (c : Vector Int n) (k : Fin n) (hzero : ∀ (j : Fin n), ↑k < ↑j → c[j] = 0) : prefixSpan (basis b) ↑k ⋯ (Vector.map (fun (x : Int) => ↑x) (Matrix.vecMul c b))

Transport of prefixSpan_castIntMatrix through basis_span: the cast integer row combination also lies in the prefix span of the first k.val + 1 Gram-Schmidt basis rows.

theorem Hex.GramSchmidt.Int.prefixSpan_basis_and_coeffs_apply_eq_of_vecMul {n m : Nat} (b : Matrix Int n m) (c : Vector Int n) (k : Fin n) (hzero : ∀ (j : Fin n), ↑k < ↑j → c[j] = 0) : prefixSpan (basis b) ↑k ⋯ (Vector.map (fun (x : Int) => ↑x) (Matrix.vecMul c b)) ∧ (Matrix.vecMul (Vector.map (fun (x : Int) => ↑x) c) (coeffs b))[k] = ↑c[k]

Package the prefix-span witness together with the recovered top Gram-Schmidt coordinate for a lattice row combination whose integer coefficients vanish above k.

@[simp]

theorem Hex.GramSchmidt.Int.coeffs_mul_basis_eq_castIntMatrix {n m : Nat} (b : Matrix Int n m) : coeffs b * basis b = castIntMatrix b

The coefficient matrix reconstructs the cast integer input rows from the Gram-Schmidt basis rows: coeffs b * basis b collapses to the cast input castIntMatrix b.

theorem Hex.GramSchmidt.Int.vecMul_basis_coeffs_reconstruction {n m : Nat} (b : Matrix Int n m) (c : Vector Int n) : Vector.map (fun (x : Int) => ↑x) (Matrix.vecMul c b) = Matrix.vecMul (Matrix.vecMul (Vector.map (fun (x : Int) => ↑x) c) (coeffs b)) (basis b)

Integer row combinations reconstruct through the Gram-Schmidt basis after first combining the Gram-Schmidt coefficient rows.

@[simp]

theorem Hex.GramSchmidt.Int.normSq_map_intCast {m : Nat} (v : Vector Int m) : (Vector.map (fun (x : Int) => ↑x) v).normSq = ↑v.normSq

Casting commutes with the squared norm: the rational squared norm of an integer vector mapped into ℚ equals its integer squared norm cast to ℚ. This transfers norm facts proved over ℤ into the rational Gram-Schmidt setting. As a simp rule it pushes the cast outward, putting the rational squared norm in the normal form ((normSq v : Int) : Rat).

theorem Hex.GramSchmidt.Int.normSq_latticeVec_ge_min_basis_normSq {n m : Nat} (b : Matrix Int n m) (_hli : independent b) (v : Vector Int m) (hv : memLattice b v) (hv' : v ≠ 0) : ∃ (i : Fin n), ((basis b).row i).normSq ≤ ↑v.normSq

Every nonzero lattice vector is at least as long as some basis row: there is an index i with normSq ((basis b).row i) ≤ normSq v (compared in ℚ). This lower-bounds an arbitrary lattice vector by an explicit basis quantity, the starting point for relating short lattice vectors to the input basis.

theorem Hex.GramSchmidt.Int.exists_top_index_normSq_le_of_memLattice {n m : Nat} (b : Matrix Int n m) (_hli : independent b) (v : Vector Int m) (hv : memLattice b v) (hv' : v ≠ 0) : ∃ (k : Fin n), ∃ (c : Vector Int n), Matrix.vecMul c b = v ∧ c[k] ≠ 0 ∧ (∀ (j : Fin n), ↑k < ↑j → c[j] = 0) ∧ ((basis b).row k).normSq ≤ ↑v.normSq

Strengthening of normSq_latticeVec_ge_min_basis_normSq that exposes the highest nonzero coefficient index k of a nonzero lattice vector together with the integer coefficients that witness it, the fact that those coefficients vanish above k, and the matching basis-row length bound ‖b*_k‖² ≤ ‖v‖².

This is the survivor-span entry point: the vanishing-above-k data localizes v to the prefix b_0 … b_k, and the length bound feeds a Gram-Schmidt cut test on the top index k.

Dot-product symmetry support

theorem Hex.GramSchmidt.Int.scaledCoeffMatrix_eq_borderedMinor {n m : Nat} (b : Matrix Int n m) (i j : Fin n) (hji : ↑j < ↑i) : scaledCoeffMatrix b i j hji = b.gramMatrix.borderedMinor ↑j ⋯ ⟨↑j, ⋯⟩ i

The Cramer determinant matrix for the scaled Gram-Schmidt coefficient (i, j) (with j < i) is the bordered minor of gramMatrix b at level j with the border row index taken to be j and the border column index taken to be i. This is the definitional equation between GramSchmidt.scaledCoeffMatrix and the bordered-minor machinery in HexBareiss.Bareiss.

theorem Hex.GramSchmidt.Int.scaledCoeffRows_lower_eq_noPivotLoop_scaledCoeffMatrix {n m : Nat} (b : Matrix Int n m) (i j : Fin n) (hji : ↑j < ↑i) (h_nonsing : (Matrix.noPivotLoop (↑j) b.gramMatrix.noPivotInitialState).singularStep = none) : getArrayEntry (scaledCoeffRows b) ↑i ↑j = (Matrix.noPivotLoop (↑j) (scaledCoeffMatrix b i j hji).noPivotInitialState).matrix[Fin.last ↑j][Fin.last ↑j]

Non-singular top-level composite: when the no-pivot Bareiss pass over the full Gram matrix has not recorded a singular step before reaching column j, the executable scaled-coefficient array entry below the diagonal at (i, j) matches the trailing entry of the no-pivot Bareiss-style loop on the corresponding Cramer determinant matrix scaledCoeffMatrix b i j hji. This composes scaledCoeffArrayLoop_lower_matches_target_column (from #4103), noPivotLoop_full_eq_borderedMinor_at_trailing (from #4028), and the symmetry/transpose equation noPivotLoop_scaledCoeffMatrix_eq.

theorem Hex.GramSchmidt.Int.getArrayEntry_scaledCoeffRowsSchur_eq_noPivotLoop_of_nonsing {n m : Nat} (b : Matrix Int n m) (hquot : StepWitness b) (q : Nat) (hqn : q < n) (h_nonsing : (Matrix.noPivotLoop q b.gramMatrix.noPivotInitialState).singularStep = none) : getArrayEntry (scaledCoeffRowsSchur b) q q = (Matrix.noPivotLoop q b.gramMatrix.noPivotInitialState).matrix[⟨q, hqn⟩][⟨q, hqn⟩] ∧ ∀ (c : Nat), q < c → ∀ (hcn : c < n), getArrayEntry (scaledCoeffRowsSchur b) c q = (Matrix.noPivotLoop q b.gramMatrix.noPivotInitialState).matrix[⟨c, hcn⟩][⟨q, hqn⟩]

Mathlib-free non-singular Schur ≡ Bareiss correspondence at a single column. When the no-pivot Bareiss pass over the full Gram matrix reaches column q without recording a singular step, the diagonal slot and every below-column entry of the integral Schur kernel match the corresponding noPivotLoop/Bareiss matrix at fuel q.

Proved by strong induction on q. The base case q = 0 reduces to the column-zero boundary of the Schur kernel together with noPivotLoop at zero fuel returning the initial Gram state. The step case q' + 1 rewrites the Schur recurrence rows[c][q' + 1] = rows[q'][q'] · gram[c][q' + 1] - schurSigma rows c (q' + 1) and discharges the σ-chain via schurSigma_foldl_eq at p_out = q' + 1, fed with the σ-fold correspondence assembled from the strong inductive hypothesis.

theorem Hex.GramSchmidt.Int.getArrayEntry_scaledCoeffRowsSchur_eq_zero_of_singularStep_lt {n m : Nat} (b : Matrix Int n m) (hquot : StepWitness b) (i j : Nat) (hi : i < n) (hji : j ≤ i) (s : Nat) (hsj : s < j) (h_sing : (Matrix.noPivotLoop j b.gramMatrix.noPivotInitialState).singularStep = some s) : getArrayEntry (scaledCoeffRowsSchur b) i j = 0

Singular cascade at the Schur kernel. If the no-pivot Bareiss pass over the full Gram matrix records an early singular step at column s < j, every Schur-kernel entry in the column-j, weak-lower triangle (j ≤ i) vanishes.

The row-s column is cleared by combining the non-singular Schur≡Bareiss correspondence at fuel s (getArrayEntry_scaledCoeffRowsSchur_eq_noPivotLoop_of_nonsing) with the column-zero structural lemma at the singular step (principalSubmatrix_gram_zero_pivot_column_zero). Strong induction on j' ∈ (s, j] then propagates the zeros via the Schur recurrence rows[i'][j'] = rows[j'-1][j'-1] · gram[i'][j'] - schurSigma i' j'. The diagonal factor rows[j'-1][j'-1] is zero by the row-s lemma when j' = s + 1 and by the cascade IH otherwise. The σ-fold collapses to zero by sub-induction on the iteration count: the killing iteration p = s makes all three relevant Schur entries zero (rows[s][s] = 0 and rows[c][s] = 0 for c ≥ s + 1), so the σ-body exactDiv of zero by the prev-pivot returns zero; subsequent iterations preserve zero via the outer IH at columns (s, j'). The proof does not transitively cite getArrayEntry_scaledCoeffRowsSchur_eq (the residual gap at line 6463).

theorem Hex.GramSchmidt.Int.getArrayEntry_scaledCoeffRowsSchur_eq {n m : Nat} (b : Matrix Int n m) (hquot : StepWitness b) (i j : Nat) : getArrayEntry (scaledCoeffRowsSchur b) i j = getArrayEntry (scaledCoeffRows b) i j

The per-row Schur scaled-coefficient kernel and the column-major Bareiss array path produce identical integer values at every cell. Both arrays contain the leading Gram determinant d_{j+1} on the diagonal and d_{j+1} · μ_{i,j} below the diagonal, with zeros above; the recurrences differ only in evaluation order. This equivalence is the bridge from the Schur implementation to the existing invariant infrastructure proven about scaledCoeffRows.

Closure routes the in-bounds j ≤ i, j ≠ 0 case through Sub-D (getArrayEntry_scaledCoeffRowsSchur_eq_noPivotLoop_of_nonsing) and Sub-C′ (getArrayEntry_scaledCoeffRowsSchur_eq_zero_of_singularStep_lt); the out-of-bounds branch (n ≤ i) follows from both arrays having size n, so the row entry is default on both sides.

theorem Hex.GramSchmidt.Int.gramDetVec_eq_gramDet {n m : Nat} (b : Matrix Int n m) (hquot : StepWitness b) (k : Nat) (hk : k ≤ n) : (gramDetVec b).get ⟨k, ⋯⟩ = gramDet b k hk

The packed Gram determinant vector agrees entrywise with gramDet: under a step witness, its k-th component is the determinant of the leading k × k Gram minor for every k ≤ n. This identifies the executable gramDetVec array pass with its specification gramDet.

theorem Hex.GramSchmidt.Int.scaledCoeffs_diag_toNat {n m : Nat} (b : Matrix Int n m) (hquot : StepWitness b) (i : Nat) (hi : i < n) : (entry (scaledCoeffs b) ⟨i, hi⟩ ⟨i, hi⟩).toNat = gramDet b (i + 1) ⋯

Nat-level diagonal synchronization for the public scaled-coefficient matrix. This is the Mathlib-free diagonal fact exposed by the shared array pass; the stronger Int-valued diagonal statement additionally needs a nonnegativity proof for the Bareiss/Gram determinant slot.

theorem Hex.GramSchmidt.Int.scaledCoeffs_diag_eq_zero_or_eq_principalSubmatrix_bareiss {n m : Nat} (b : Matrix Int n m) (hquot : StepWitness b) (i : Nat) (hi : i < n) : entry (scaledCoeffs b) ⟨i, hi⟩ ⟨i, hi⟩ = 0 ∨ entry (scaledCoeffs b) ⟨i, hi⟩ ⟨i, hi⟩ = (b.gramMatrix.principalSubmatrix (i + 1) ⋯).bareiss

Signed diagonal information for the public scaled-coefficient matrix. The diagonal slot is either the zero tail recorded after an earlier singular no-pivot step, or the Bareiss determinant of the corresponding leading Gram prefix.

theorem Hex.GramSchmidt.Int.scaledCoeffs_diag_of_nonneg {n m : Nat} (b : Matrix Int n m) (hquot : StepWitness b) (i : Nat) (hi : i < n) (hnonneg : 0 ≤ entry (scaledCoeffs b) ⟨i, hi⟩ ⟨i, hi⟩) : entry (scaledCoeffs b) ⟨i, hi⟩ ⟨i, hi⟩ = Int.ofNat (gramDet b (i + 1) ⋯)

Int-valued diagonal identity for the scaled Gram-Schmidt coefficients: once the (i, i) slot is known nonnegative, it equals the Gram determinant gramDet b (i + 1). The toNat form (scaledCoeffs_diag_toNat) is unconditional; the signed Int form needs the determinant slot to be nonnegative.

theorem Hex.GramSchmidt.Int.scaledCoeffs_eq_zero_of_singularStep_lt {n m : Nat} (b : Matrix Int n m) (hquot : StepWitness b) (i j : Fin n) (hji : ↑j < ↑i) (s : Nat) (h_sing : (Matrix.noPivotLoop (↑j) b.gramMatrix.noPivotInitialState).singularStep = some s) (_hsj : s < ↑j) : entry (scaledCoeffs b) i j = 0

Singular dual of scaledCoeffRows_lower_eq_noPivotLoop_scaledCoeffMatrix. When the no-pivot Bareiss pass over the full Gram matrix records an early singular step before reaching column j, the integral scaled Gram-Schmidt coefficient below the diagonal at (i, j) is zero. The array loop halts at the recorded singular column and the target column is never written.

theorem Hex.GramSchmidt.Int.scaledCoeffs_lower_eq_noPivotLoop_scaledCoeffMatrix {n m : Nat} (b : Matrix Int n m) (hquot : StepWitness b) (i j : Fin n) (hji : ↑j < ↑i) (h_nonsing : (Matrix.noPivotLoop (↑j) b.gramMatrix.noPivotInitialState).singularStep = none) : entry (scaledCoeffs b) i j = (Matrix.noPivotLoop (↑j) (scaledCoeffMatrix b i j hji).noPivotInitialState).matrix[Fin.last ↑j][Fin.last ↑j]

Non-singular companion of scaledCoeffs_eq_zero_of_singularStep_lt: when the no-pivot Bareiss pass over the full Gram matrix reaches column j without recording a singular step, the integral scaled Gram-Schmidt coefficient below the diagonal at (i, j) matches the trailing entry of the no-pivot Bareiss-style loop on the corresponding Cramer minor scaledCoeffMatrix b i j hji.

theorem Hex.GramSchmidt.Int.rowSwap_row_left_int {n' m' : Nat} (M : Matrix Int n' m') (i j : Fin n') : (M.rowSwap i j)[i] = M[j]

For a Matrix Int, the Fin-indexed left swap row i becomes the old row j. This is the direct row-access form of Matrix.rowSwap for the first swapped row.

theorem Hex.GramSchmidt.Int.rowSwap_row_right_int {n' m' : Nat} (M : Matrix Int n' m') (i j : Fin n') : (M.rowSwap i j)[j] = M[i]

For a Matrix Int, the Fin-indexed right swap row j becomes the old row i. This is the companion row-access form of Matrix.rowSwap for the second swapped row.

theorem Hex.GramSchmidt.Int.scaledCoeffMatrix_rowSwap_adjacent_pivot_transpose {n m : Nat} (b : Matrix Int n m) (km1 k : Fin n) (hkm1 : ↑km1 + 1 = ↑k) (hkm1k : ↑km1 < ↑k) : scaledCoeffMatrix (b.rowSwap km1 k) k km1 hkm1k = (scaledCoeffMatrix b k km1 hkm1k).transpose

Swapping the adjacent rows km1 and k of the basis transposes the scaled-coefficient Cramer minor for that pivot pair: scaledCoeffMatrix (rowSwap b km1 k) k km1 = (scaledCoeffMatrix b k km1)ᵀ. This is the matrix identity behind an LLL adjacent row swap, relating the coefficient minor before and after the exchange.

Coefficient bordered minor and multilinearity entry equation

The coeffBM matrix shares its first k columns with borderedMinor G k hk i j (those columns do not depend on j) and replaces the last column with the indicator vector picking out row index a. The multilinearity entry equation expands Matrix.det (borderedMinor G k hk i j) as a sum over a of Matrix.det (coeffBM G k hk i a) * G[a][j], applying det_colReplace_sum_finRange to the indicator expansion of the last column.

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

The k-th Gram determinant for a rational input matrix.

This remains Mathlib-free API: it is the direct Hex determinant definition used by rational Gram-Schmidt callers, not a theorem identifying an executable Hex output with a Leibniz determinant.

Equations

• Hex.GramSchmidt.Rat.gramDet b k hk = (Hex.GramSchmidt.leadingGramMatrixRat b k hk).det