Adjacent-swap pivot Gram-determinant product

Swapping adjacent rows km1, k (with km1 + 1 = k) of b changes only the leading k × k Gram determinant within 0 ≤ t ≤ k + 1. The new pivot Gram determinant gramDet (rowSwap b km1 k) k satisfies the integer product identity

gramDet b' k · gramDet b k = gramDet b (k+1) · gramDet b km1 + B²

where B = (scaledCoeffs b)[k][km1]. This is the fraction-free form of the standard rational adjacent-swap update used by integer LLL.

theorem Hex.GramSchmidt.Int.dot_add_left_rat {m' : ℕ} (u v w : Vector ℚ m') : (u + v).dotProduct w = u.dotProduct w + v.dotProduct w

The rational dot product is additive in its left argument.

theorem Hex.GramSchmidt.Int.dot_smul_left_rat {m' : ℕ} (s : ℚ) (u v : Vector ℚ m') : (s • u).dotProduct v = s * u.dotProduct v

The rational dot product is homogeneous in its left argument: a scalar factors out.

theorem Hex.GramSchmidt.Int.normSq_add_smul_orthogonal_rat {m' : ℕ} (curr prev : Vector ℚ m') (μ : ℚ) (horth : curr.dotProduct prev = 0) : (curr + μ • prev).normSq = curr.normSq + μ ^ 2 * prev.normSq

Pythagoras: if curr ⊥ prev, then the squared norm of curr + μ • prev splits as ‖curr‖² + μ² · ‖prev‖².

theorem Hex.GramSchmidt.Int.gramSchmidtNormProduct_rowSwap_below {n m : ℕ} (b : Matrix ℤ n m) (km1 k : Fin n) (hkm1k : ↑km1 < ↑k) : gramSchmidtNormProduct (b.rowSwap km1 k) ↑km1 ⋯ = gramSchmidtNormProduct b ↑km1 ⋯

For j < km1.val, the Gram-Schmidt basis row is unchanged by the swap of rows km1, k. The norm-square product over indices < km1.val therefore agrees on b and Matrix.rowSwap b km1 k.

theorem Hex.GramSchmidt.Int.gramDet_eq_prod_normSq_uncond {n m : ℕ} (b : Matrix ℤ n m) (k : ℕ) (hk : k ≤ n) : ↑(gramDet b k hk) = gramSchmidtNormProduct b k hk

Unconditional version of gramDet_eq_prod_normSq: the leading Gram determinant casts to the rational gramSchmidtNormProduct without requiring linear independence. The independent hypothesis in the public theorem is not actually used by the proof.

theorem Hex.GramSchmidt.Int.gramDet_subst_val {n m : ℕ} (b : Matrix ℤ n m) (j₁ j₂ : ℕ) (h₁ : j₁ ≤ n) (h₂ : j₂ ≤ n) (he : j₁ = j₂) : gramDet b j₁ h₁ = gramDet b j₂ h₂

gramDet is independent of the propositional ≤ n proof, and depends only on the Nat value k. Two gramDet calls with equal Nat arguments produce equal values.

theorem Hex.GramSchmidt.Int.gramSchmidtNormProduct_subst_val {n m : ℕ} (b : Matrix ℤ n m) (j₁ j₂ : ℕ) (h₁ : j₁ ≤ n) (h₂ : j₂ ≤ n) (he : j₁ = j₂) : gramSchmidtNormProduct b j₁ h₁ = gramSchmidtNormProduct b j₂ h₂

Same as gramDet_subst_val for gramSchmidtNormProduct.

theorem Hex.GramSchmidt.Int.gramDet_rowSwap_adjacent_pivot_product {n m : ℕ} (b : Matrix ℤ n m) (km1 k : Fin n) (hkm1 : ↑km1 + 1 = ↑k) : have B := entry (scaledCoeffs b) k km1; ↑(gramDet (b.rowSwap km1 k) ↑k ⋯) * ↑(gramDet b ↑k ⋯) = ↑(gramDet b (↑k + 1) ⋯) * ↑(gramDet b ↑km1 ⋯) + B ^ 2

Integer fraction-free identity for the leading pivot Gram determinant after swapping adjacent rows km1, k with km1.val + 1 = k.val:

gramDet b' k · gramDet b k = gramDet b (k+1) · gramDet b km1 + B²

where B = (scaledCoeffs b)[k][km1]. This is the algebraic heart of the integer LLL adjacent-swap update.

theorem Hex.GramSchmidt.Int.dot_basis_castRow_eq_coeffs_mul_normSq {n m : ℕ} (b : Matrix ℤ n m) (i j : ℕ) (hi : i < n) (hj : j < i) : ((basis b).row ⟨j, ⋯⟩).dotProduct (Vector.map (fun (x : ℤ) => ↑x) (b.row ⟨i, hi⟩)) = entry (coeffs b) ⟨i, hi⟩ ⟨j, ⋯⟩ * ((basis b).row ⟨j, ⋯⟩).normSq

Dotting the j-th Gram-Schmidt basis row with the integer-cast i-th input row picks out the (i, j) Gram-Schmidt coefficient weighted by the squared norm of the basis row. Holds unconditionally: when the basis row is zero, both sides vanish (orthogonality + the if-branch in coeffs_lower_projection).

theorem Hex.GramSchmidt.Int.dot_basis_rowSwap_curr_prev_eq_normSq {n m : ℕ} (b : Matrix ℤ n m) (km1 k : Fin n) (hkm1 : ↑km1 + 1 = ↑k) : ((basis (b.rowSwap km1 k)).row k).dotProduct ((basis b).row km1) = ((basis (b.rowSwap km1 k)).row k).normSq

For an adjacent row swap b' = rowSwap b km1 k with km1.val + 1 = k.val, the dot product of the swapped k-th basis row with the original km1-th basis row equals the squared norm of the swapped k-th basis row. Equivalently, dot u_k prev = ||u_k||², where u_k = (basis b').row k and prev = (basis b).row km1.

The proof routes both sides through dot u_k (cast b.row km1) = dot u_k (cast b'.row k) (the cast vectors agree because b'.row k = b.row km1 from the row swap), expanding each side via basis_decomposition. The prefix combinations vanish on both sides because u_k = (basis b').row k is orthogonal to every (basis b').row q with q < k, and the relevant (basis b).row q agrees with (basis b').row q for q < km1.

theorem Hex.GramSchmidt.Int.dot_basis_rowSwap_curr_castRow_eq {n m : ℕ} (b : Matrix ℤ n m) (km1 k : Fin n) (hkm1 : ↑km1 + 1 = ↑k) (i : Fin n) (hki : ↑k < ↑i) : ((basis (b.rowSwap km1 k)).row k).dotProduct (Vector.map (fun (x : ℤ) => ↑x) (b.row i)) = ((basis (b.rowSwap km1 k)).row k).dotProduct ((basis b).row km1) * (entry (coeffs b) i ⟨↑km1, ⋯⟩ - entry (coeffs b) k ⟨↑km1, ⋯⟩ * entry (coeffs b) i k)

For an adjacent row swap b' = rowSwap b km1 k with km1.val + 1 = k.val, the dot product of the swapped k-th basis row with the integer-cast i-th input row (for i > k) decomposes as the dot product of u_k with the original km1-th basis row times a linear combination of the original km1-th and k-th coefficients of row i.

Concretely, with μ = c[k][km1]: dot u_k (cast b.row i) = (dot u_k prev) * (c[i][km1] - μ * c[i][k])

This is the "Cramer-style" dot product expansion that, combined with dot_basis_rowSwap_curr_prev_eq_normSq, lets us extract c'[i][k] from the b'-side Cramer formula c'[i][k] * ||u_k||² = dot u_k (cast b.row i).

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

Below the diagonal, the executable integral scaled coefficient is exactly the Cramer determinant encoded by scaledCoeffMatrix.

theorem Hex.GramSchmidt.Int.leadingGramMatrixInt_det_eq_gramDet_int_of_nonneg {n m : ℕ} (b : Matrix ℤ n m) (t : ℕ) (ht : t ≤ n) (hdet : 0 ≤ (leadingGramMatrixInt b t ht).det) : (leadingGramMatrixInt b t ht).det = Int.ofNat (gramDet b t ht)

Conditional form of the leading Gram determinant identity. The remaining unconditional fact is exactly the nonnegativity of leading Gram determinants: once 0 ≤ det is available, the public Nat-valued gramDet casts back to the signed determinant.

theorem Hex.GramSchmidt.Int.leadingGramMatrixInt_det_eq_gramDet_int {n m : ℕ} (b : Matrix ℤ n m) (t : ℕ) (ht : t ≤ n) : (leadingGramMatrixInt b t ht).det = Int.ofNat (gramDet b t ht)

The public Nat Gram determinant casts back to the signed determinant of the leading integer Gram matrix.

theorem Hex.GramSchmidt.Int.scaledCoeffs_diag {n m : ℕ} (b : Matrix ℤ n m) (i : ℕ) (hi : i < n) : entry (scaledCoeffs b) ⟨i, hi⟩ ⟨i, hi⟩ = Int.ofNat (gramDet b (i + 1) ⋯)

Mathlib-side unconditional diagonal synchronization for the public scaled-coefficient matrix. The Mathlib-free core exposes the Nat-level version and the conditional Int lift; the required nonnegativity of the Gram/Bareiss diagonal slot is supplied here.

theorem Hex.GramSchmidt.Int.gramDet_pos_of_upperTriangular_pos_diag {n : ℕ} (M : Matrix ℤ n n) (hzero : ∀ (i j : Fin n), ↑j < ↑i → M[i][j] = 0) (hdiag : ∀ (i : Fin n), 0 < M[i][i]) (k : ℕ) (hk : k ≤ n) (hk' : 0 < k) : 0 < gramDet M k hk

The leading executable Gram determinants of a square upper-triangular integer matrix with strictly positive diagonal are positive.

This theorem lives in HexGramSchmidtMathlib: its proof identifies the executable gramDet with the Leibniz determinant of the leading Gram matrix via the composition of HexMatrixMathlib.bareiss_eq_mathlib_det and HexMatrixMathlib.det_eq.symm.