Strictly-increasing column-tuple enumeration

The Cauchy-Binet sum-of-squares formula needs a Mathlib-free enumeration of the "essentially distinct" column choices: each strictly increasing length-n selection from Fin m represents one orbit of injective ordered tuples under the action of permutations of Fin n. The enumeration below builds these tuples by appending the new largest element, recursing on a bound parameter that constrains the next entry to be strictly less than bound.

def Hex.Matrix.selectedColumnTuplesUpTo (m n bound : Nat) : List (Vector (Fin m) n)

All strictly increasing length-n column tuples in Fin m whose entries are all < bound. The recursion appends a new largest element c < bound and recurses on the remaining prefix with the smaller bound c.val.

Equations

• One or more equations did not get rendered due to their size.
• Hex.Matrix.selectedColumnTuplesUpTo m 0 x✝ = [#v[]]

def Hex.Matrix.selectedColumnTuples (n m : Nat) : List (Vector (Fin m) n)

Enumerate all strictly increasing length-n column selections from Fin m. This list of orbit representatives drives the Cauchy-Binet grouping argument that re-folds the ordered-tuple Gram expansion as a sum of squared minors.

Equations

• Hex.Matrix.selectedColumnTuples n m = Hex.Matrix.selectedColumnTuplesUpTo m n m

def Hex.Matrix.IsStrictlyIncreasingColumnTuple {m n : Nat} (cols : Vector (Fin m) n) : Prop

A column tuple is strictly increasing as a function Fin n → Fin m.

Equations

• Hex.Matrix.IsStrictlyIncreasingColumnTuple cols = ∀ (i j : Fin n), ↑i < ↑j → ↑cols[i] < ↑cols[j]

theorem Hex.Matrix.mem_selectedColumnTuples_iff {n m : Nat} (cols : Vector (Fin m) n) : cols ∈ selectedColumnTuples n m ↔ IsStrictlyIncreasingColumnTuple cols

Public membership characterization: a column tuple lies in selectedColumnTuples n m iff it is strictly increasing.

theorem Hex.Matrix.isStrictlyIncreasingColumnTuple_injective {n m : Nat} {cols : Vector (Fin m) n} (hsi : IsStrictlyIncreasingColumnTuple cols) : Function.Injective (columnTupleVectorFn cols)

Strictly increasing column tuples induce injective Fin n → Fin m selection functions, so each enumerated tuple yields an injective columnTupleVectorFn.

theorem Hex.Matrix.mem_selectedColumnTuples_injective {n m : Nat} {cols : Vector (Fin m) n} (hmem : cols ∈ selectedColumnTuples n m) : Function.Injective (columnTupleVectorFn cols)

Convenience corollary: every column tuple enumerated by selectedColumnTuples yields an injective column-selection function.

theorem Hex.Matrix.selectedColumnTuples_nodup {n m : Nat} : (selectedColumnTuples n m).Nodup

The strictly-increasing column-tuple enumeration has no duplicates.

Canonical sort and orbit factorization for injective column tuples

For the Cauchy-Binet orbit-grouping argument we need, for every injective ordered column tuple cols : Vector (Fin m) n, a canonical factorization

cols[i] = (sortInjTuple cols)[(sortInjPerm cols)[i]]

where sortInjTuple cols is strictly increasing (i.e. lives in selectedColumnTuples n m) and sortInjPerm cols is a permutation of Fin n (i.e. lives in permutationVectors n). This gives a bijection between injective columnTupleVectors n m entries and the product selectedColumnTuples n m × permutationVectors n, which lets the orbit sum group ordered minors by their canonical sorted column choice.

The implementation is rank-based: sortInjPerm cols i is the number of columns in cols strictly smaller in value than cols[i]. For any cols, this is < n because cols[i] is never strictly less than itself; for injective cols, the rank is moreover a bijection on Fin n.

def Hex.Matrix.columnRankNat {m n : Nat} (cols : Vector (Fin m) n) (i : Fin n) : Nat

Count of indices whose cols-image has strictly smaller Fin.val than that at i. This is the natural-number form of the rank.

Equations

• Hex.Matrix.columnRankNat cols i = (List.filter (fun (j : Fin n) => decide (↑cols[j] < ↑cols[i])) (List.finRange n)).length

theorem Hex.Matrix.columnRankNat_lt {m n : Nat} (cols : Vector (Fin m) n) (i : Fin n) : columnRankNat cols i < n

The rank is always strictly less than n: index i itself is never in the filter, so the filter is a strict sublist of finRange n.

def Hex.Matrix.sortInjPerm {m n : Nat} (cols : Vector (Fin m) n) : Vector (Fin n) n

Canonical sorting permutation: for each index i, output the rank of cols[i] (number of strictly smaller positions). For an injective cols this is genuinely a permutation of Fin n; for a non-injective cols it is still well-defined but may have repeated values.

Equations

• Hex.Matrix.sortInjPerm cols = Vector.ofFn fun (i : Fin n) => ⟨Hex.Matrix.columnRankNat cols i, ⋯⟩

theorem Hex.Matrix.sortInjPerm_getElem_val {m n : Nat} (cols : Vector (Fin m) n) (i : Fin n) : ↑(sortInjPerm cols)[i] = columnRankNat cols i

The i-th value of the sorting permutation is the rank columnRankNat cols i of cols[i] (the number of strictly smaller positions).

def Hex.Matrix.sortInjTuple {m n : Nat} (cols : Vector (Fin m) n) : Vector (Fin m) n

The canonical sorted version of cols: read cols through the inverse of sortInjPerm. For an injective cols this is strictly increasing; for a non-injective cols the value is well-defined but not meaningful.

Equations

• Hex.Matrix.sortInjTuple cols = Vector.ofFn fun (r : Fin n) => cols[(Hex.Matrix.inversePermutationVector (Hex.Matrix.sortInjPerm cols))[r]]

theorem Hex.Matrix.sortInjPerm_mem_permutationVectors {m n : Nat} (cols : Vector (Fin m) n) (hinj : Function.Injective (columnTupleVectorFn cols)) : sortInjPerm cols ∈ permutationVectors n

For an injective cols, sortInjPerm cols ∈ permutationVectors n.

theorem Hex.Matrix.mem_columnTupleVectors {n m : Nat} (cols : Vector (Fin m) n) : cols ∈ columnTupleVectors n m

Every length-n tuple of column indices appears in columnTupleVectors n m.

theorem Hex.Matrix.cols_getElem_eq_sortInjTuple_sortInjPerm {m n : Nat} (cols : Vector (Fin m) n) (hinj : Function.Injective (columnTupleVectorFn cols)) (i : Fin n) : cols[i] = (sortInjTuple cols)[(sortInjPerm cols)[i]]

Factorization equation: each entry of cols is recovered through the canonical sort/permutation pair. Requires injectivity of cols.

theorem Hex.Matrix.isStrictlyIncreasingColumnTuple_sortInjTuple {m n : Nat} (cols : Vector (Fin m) n) (hinj : Function.Injective (columnTupleVectorFn cols)) : IsStrictlyIncreasingColumnTuple (sortInjTuple cols)

For an injective cols, the canonical sorted tuple is strictly increasing.

theorem Hex.Matrix.sortInjTuple_mem_selectedColumnTuples {m n : Nat} (cols : Vector (Fin m) n) (hinj : Function.Injective (columnTupleVectorFn cols)) : sortInjTuple cols ∈ selectedColumnTuples n m

For an injective cols, the canonical sorted tuple is enumerated by selectedColumnTuples n m.

Forward injectivity of the sort/permutation pair

theorem Hex.Matrix.sortInj_pair_injective {m n : Nat} {cols cols' : Vector (Fin m) n} (hinj : Function.Injective (columnTupleVectorFn cols)) (hinj' : Function.Injective (columnTupleVectorFn cols')) (hsort : sortInjTuple cols = sortInjTuple cols') (hperm : sortInjPerm cols = sortInjPerm cols') : cols = cols'

Pairwise distinctness: two injective column tuples that map to the same (sortInjTuple, sortInjPerm) pair must be equal.

Reconstruction from selectedColumnTuples × permutationVectors

For a strictly-increasing sel and a permutation perm, the "reconstruction" Vector.ofFn (fun i => sel[perm[i]]) is itself injective, and its canonical sort/permutation pair recovers (sel, perm). This is the inverse map of sortInjTuple/sortInjPerm.

def Hex.Matrix.reconstructInjTuple {m n : Nat} (sel : Vector (Fin m) n) (perm : Vector (Fin n) n) : Vector (Fin m) n

Reconstruction map: given a sorted choice and a permutation, build an ordered column tuple.

Equations

• Hex.Matrix.reconstructInjTuple sel perm = Vector.ofFn fun (i : Fin n) => sel[perm[i]]

theorem Hex.Matrix.getElem_reconstructInjTuple {m n : Nat} (sel : Vector (Fin m) n) (perm : Vector (Fin n) n) (i : Fin n) : (reconstructInjTuple sel perm)[i] = sel[perm[i]]

The i-th entry of the reconstructed tuple is sel[perm[i]]: read the sorted choice sel through the permutation perm.

theorem Hex.Matrix.getElem_columnTupleMatrix_reconstructInjTuple {R : Type u} {n m : Nat} (A : Matrix R n m) (sel : Vector (Fin m) n) (perm : Vector (Fin n) n) (r c : Fin n) : (A.columnTupleMatrix (columnTupleVectorFn (reconstructInjTuple sel perm)))[r][c] = (A.columnTupleMatrix (columnTupleVectorFn sel))[r][perm[c]]

Selecting columns via the reconstructed tuple equals selecting via sel with the column index permuted by perm: entry (r, c) agrees with entry (r, perm[c]) of the sel-selected minor.

theorem Hex.Matrix.columnTupleCoeff_reconstructInjTuple {R : Type u} [Lean.Grind.CommRing R] {n m : Nat} (A : Matrix R n m) (sel : Vector (Fin m) n) (perm : Vector (Fin n) n) : A.columnTupleCoeff (reconstructInjTuple sel perm) = (A.columnTupleMatrix (columnTupleVectorFn sel)).detProduct perm

Reconstructing an injective tuple from a selected tuple and a permutation turns the coefficient product into the corresponding determinant product.

theorem Hex.Matrix.reconstructInjTuple_injective {m n : Nat} {sel : Vector (Fin m) n} {perm : Vector (Fin n) n} (hsel : IsStrictlyIncreasingColumnTuple sel) (hperm : perm ∈ permutationVectors n) : Function.Injective (columnTupleVectorFn (reconstructInjTuple sel perm))

The reconstructed column tuple is itself injective when sel is strictly increasing and perm is a permutation.

theorem Hex.Matrix.sortInjPerm_reconstructInjTuple {m n : Nat} {sel : Vector (Fin m) n} {perm : Vector (Fin n) n} (hsel : IsStrictlyIncreasingColumnTuple sel) (hperm : perm ∈ permutationVectors n) : sortInjPerm (reconstructInjTuple sel perm) = perm

sortInjPerm of a reconstructed tuple recovers the original permutation.

theorem Hex.Matrix.sortInjTuple_reconstructInjTuple {m n : Nat} {sel : Vector (Fin m) n} {perm : Vector (Fin n) n} (hsel : IsStrictlyIncreasingColumnTuple sel) (hperm : perm ∈ permutationVectors n) : sortInjTuple (reconstructInjTuple sel perm) = sel

sortInjTuple of a reconstructed tuple recovers the original selection.

Bijection wrappers

theorem Hex.Matrix.reconstructInjTuple_sortInj {m n : Nat} (cols : Vector (Fin m) n) (hinj : Function.Injective (columnTupleVectorFn cols)) : reconstructInjTuple (sortInjTuple cols) (sortInjPerm cols) = cols

Forward-then-backward identity: reconstruction inverts the canonical sort/permutation pair on injective column tuples.

theorem Hex.Matrix.selPerm_reconstructed_list_nodup {m n : Nat} : (List.flatMap (fun (sel : Vector (Fin m) n) => List.map (reconstructInjTuple sel) (permutationVectors n)) (selectedColumnTuples n m)).Nodup

The flat list of reconstructed column tuples, indexed by selectedColumnTuples × permutationVectors, has no duplicates.

theorem Hex.Matrix.mem_selPerm_reconstructed_iff {m n : Nat} (cols : Vector (Fin m) n) : cols ∈ List.flatMap (fun (sel : Vector (Fin m) n) => List.map (reconstructInjTuple sel) (permutationVectors n)) (selectedColumnTuples n m) ↔ Function.Injective (columnTupleVectorFn cols)

A column tuple is injective iff it is enumerated by the selectedColumnTuples × permutationVectors reconstruction. This is the bijection statement in membership form.

theorem Hex.Matrix.columnTupleExpansion_refold_selectedPerm {R : Type u} [Lean.Grind.CommRing R] {n m : Nat} (A : Matrix R n m) : List.foldl (fun (acc : R) (cols : Vector (Fin m) n) => acc + A.columnTupleExpansionTerm cols) 0 (columnTupleVectors n m) = List.foldl (fun (acc : R) (cols : Vector (Fin m) n) => acc + A.columnTupleExpansionTerm cols) 0 (List.flatMap (fun (sel : Vector (Fin m) n) => List.map (reconstructInjTuple sel) (permutationVectors n)) (selectedColumnTuples n m))

Refold the ordered column-tuple Gram expansion over the canonical selectedColumnTuples × permutationVectors reconstruction list. Non-injective ordered tuples contribute zero determinants, and the remaining injective tuples are exactly the reconstructed selected/permutation tuples.

theorem Hex.Matrix.det_gramMatrix_eq_sum_minors_sq {R : Type u} [Lean.Grind.CommRing R] {n m : Nat} (A : Matrix R n m) : A.gramMatrix.det = List.foldl (fun (acc : R) (cols : Vector (Fin m) n) => acc + (A.columnTupleMatrix (columnTupleVectorFn cols)).det ^ 2) 0 (selectedColumnTuples n m)

Cauchy-Binet for the row Gram matrix: the Gram determinant is the finite sum of squares of the selected column minors.

theorem Hex.Matrix.det_gramMatrix_nonneg {n m : Nat} (A : Matrix Int n m) : 0 ≤ A.gramMatrix.det

Integer row Gram determinants are nonnegative, by Cauchy-Binet as a finite sum of integer squares.

def Hex.Matrix.firstColumns (k n : Nat) (hk : k ≤ n) : Vector (Fin n) k

The identity selection of the first k columns of an n-column matrix.

Equations

• Hex.Matrix.firstColumns k n hk = Vector.ofFn fun (i : Fin k) => ⟨↑i, ⋯⟩

theorem Hex.Matrix.getElem_firstColumns (k n : Nat) (hk : k ≤ n) (i : Fin k) : (firstColumns k n hk)[i] = ⟨↑i, ⋯⟩

The i-th entry of the first-k-columns selection is the index i itself, embedded into Fin n.

theorem Hex.Matrix.firstColumns_mem_selectedColumnTuples (k n : Nat) (hk : k ≤ n) : firstColumns k n hk ∈ selectedColumnTuples k n

The first k columns form a strictly increasing selected column tuple.

theorem Hex.Matrix.columnTupleMatrix_takeRows_firstColumns_eq_principalSubmatrix {R : Type u} {n : Nat} (M : Matrix R n n) (k : Nat) (hk : k ≤ n) : (M.takeRows k hk).columnTupleMatrix (columnTupleVectorFn (firstColumns k n hk)) = M.principalSubmatrix k hk

Selecting the first k columns from the leading k rows of a square matrix gives exactly its leading k × k prefix.

theorem Hex.Matrix.det_gramMatrix_takeRows_pos_of_upperTriangular_pos_diag {n : Nat} (M : Matrix Int n n) (hzero : ∀ (i j : Fin n), ↑j < ↑i → M[i][j] = 0) (hdiag : ∀ (i : Fin n), 0 < M[i][i]) (k : Nat) (hk : k ≤ n) : 0 < (M.takeRows k hk).gramMatrix.det

The Gram determinant of the first k rows of a positive-diagonal integer upper-triangular matrix is strictly positive. The leading-principal minor provides a positive square term in the Cauchy-Binet expansion.