Permutation enumeration and inversion-parity arithmetic for the local Leibniz determinant.

This module defines permutationVectors, the recursive enumeration of the permutations of Fin n as length-n vectors, together with inversionCount, which counts the inversions of a permutation written as a list. The bulk of the file establishes how inversion count behaves under list concatenation and under swaps: inversionCount_append splits a concatenation into the inversions of each part plus the cross-inversions (crossInversionCount), and inversionCount_adjacent_swap_parity / inversionCount_swap_separated_parity show that swapping two distinct entries flips inversion parity. These parity facts underpin the sign computations used by the determinant.

It also proves that the enumeration is a faithful listing of the symmetric group: permutationVectors_complete (every duplicate-free length-n vector is enumerated) and permutationVectors_nodup / permutationVectors_nodup_list (no repeats), via the raiseFinAbove / peelLastVector last-position recursion and a handful of determinant-agnostic list and Fin helpers reused downstream.

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

Enumerate the permutations of Fin n as length-n vectors.

Equations

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

def Hex.Matrix.inversionCount {n : Nat} : List (Fin n) → Nat

Count inversions in a permutation written as a list.

Equations

• Hex.Matrix.inversionCount [] = 0
• Hex.Matrix.inversionCount (x_1 :: xs) = List.foldl (fun (acc : Nat) (y : Fin n) => acc + if y < x_1 then 1 else 0) 0 xs + Hex.Matrix.inversionCount xs

Generic list and Fin combinatorics

These determinant-agnostic helpers about folds, Nodup, and insertAt support the enumeration completeness and duplicate-freeness proofs below, and are reused by the Leibniz determinant layer downstream.

Completeness and duplicate-freeness of the enumeration

theorem Hex.Matrix.permutationVectors_complete {n : Nat} {perm : Vector (Fin n) n} (hnodup : perm.toList.Nodup) : perm ∈ permutationVectors n

Every duplicate-free length-n vector of Fin n appears in permutationVectors n. This gives the completeness half of the local permutation enumeration used by the Leibniz determinant.

theorem Hex.Matrix.permutationVectors_nodup {n : Nat} {perm : Vector (Fin n) n} (hmem : perm ∈ permutationVectors n) : perm.toList.Nodup

Every vector enumerated by permutationVectors n is duplicate-free, so each listed vector really represents a permutation of Fin n.

theorem Hex.Matrix.permutationVectors_nodup_list {n : Nat} : (permutationVectors n).Nodup

The permutation enumeration itself has no duplicate vectors. This lets determinant proofs compare sums over permutationVectors by list permutation rather than by quotienting repeated terms.