The Lindström-Gessel-Viennot Lemma: Weighted and Generalized Versions

This file formalizes the weighted version of the LGV lemma and related results, following Section "The weighted version ... The nonpermutable case" (sec.det.comb.lgv) of the Algebraic Combinatorics notes.

Main definitions

• LGV.SimpleDigraph: A digraph structure with no self-loops (irreflexive adjacency)
• LGV.SimpleDigraph.toDigraph: Conversion to Mathlib's Digraph type
• LGV.ArcWeight: A weight function on arcs of a digraph
• LGV.pathWeight: The weight of a path (product of arc weights)
• LGV.pathTupleWeight: The weight of a path tuple (product of path weights)
• LGV.pathWeightMatrix: The matrix of sums of path weights between source/target vertices
• LGV.catalanHankelMatrix: The Hankel matrix of Catalan numbers

Main results

• LGV.lgv_weighted_lattice: LGV lemma, lattice weight version (Theorem thm.lgv.kpaths.wt)
• LGV.lgv_weighted_digraph: LGV lemma, digraph weight version (Theorem thm.lgv.kpaths.wt-dg)
• LGV.lgv_nonpermutable: LGV lemma, nonpermutable lattice weight version (Corollary cor.lgv.kpaths.wt-np)
• LGV.binom_det_nonneg: Determinant of binomial coefficient matrix is nonnegative (Corollary cor.lgv.binom-det-nonneg)
• LGV.catalan_hankel_det: Hankel determinant of Catalan numbers equals 1 (Corollary cor.lgv.catalan-hankel-det-0)
• LGV.catalan_hankel_det_zero through LGV.catalan_hankel_det_seven: Base cases proved by computation

References

• Source: AlgebraicCombinatorics/tex/Determinants/LGV2.tex
• [Lindström, On the vector representations of induced matroids][Lindstrom73]
• [Gessel-Viennot, Binomial determinants, paths, and hook length formulae][GesVie85]

Implementation notes

We formalize the LGV lemma for general path-finite acyclic digraphs, with the integer lattice ℤ² as a special case. The key construction is a sign-reversing involution on intersecting path tuples that exchanges tails at the first intersection point.

The nonpermutable case applies when the source and target vertices are "sorted" in a way that prevents non-identity permutations from having non-intersecting path tuples.

For the Catalan Hankel determinant, we use Mathlib's catalan function and prove the base cases (k = 0, 1, ..., 7) by direct computation using native_decide. The general theorem uses the LGV lemma with Dyck paths.

Relationship with LGV1.lean

This file (LGV2.lean) and LGV1.lean both work with the integer lattice digraph, but use different representations:

• LGV1.lean: Uses Mathlib's Digraph type and LatticePath (list of steps: east/north)
• LGV2.lean: Uses LGV.SimpleDigraph (custom structure with irreflexivity) and SimpleDigraph.Path (list of vertices)

The integer lattice definitions have equivalent adjacency relations, proven by integerLattice_arc_iff and integerLattice_toDigraph_adj_iff. The conversion SimpleDigraph.toDigraph allows transferring results between the two representations.

This file contains the complete weighted LGV lemma proof. LGV1.lean contains the counting case infrastructure with lattice-specific path counting results.

Digraph Definitions

We work with simple digraphs that are path-finite and acyclic.

structure LGV.SimpleDigraph (V : Type u_1) : Type u_1

A simple digraph with vertex set V. Convention conv.lgv.digraph(d): A simple digraph has arcs as pairs of distinct vertices.

• arc : V → V → Prop

  The arc relation: arc u v means there is an arc from u to v

• arc_irrefl (v : V) : ¬self.arc v v

  No self-loops

structure LGV.SimpleDigraph.Path {V : Type u_1} (D : SimpleDigraph V) : Type u_1

A path in a digraph is a list of vertices where consecutive vertices are connected by arcs. A path may contain 0 arcs (in which case start and end are identical).

• vertices : List V

  The vertices of the path, in order

• nonempty : self.vertices ≠ []

  The path is nonempty

• arcs_valid (i : ℕ) (hi : i + 1 < self.vertices.length) : D.arc (self.vertices.get ⟨i, ⋯⟩) (self.vertices.get ⟨i + 1, hi⟩)

  Consecutive vertices are connected by arcs

def LGV.SimpleDigraph.Path.start {V : Type u_1} {D : SimpleDigraph V} (p : D.Path) : V

The starting vertex of a path

Equations

• p.start = p.vertices.head ⋯

def LGV.SimpleDigraph.Path.finish {V : Type u_1} {D : SimpleDigraph V} (p : D.Path) : V

The ending vertex of a path

Equations

• p.finish = p.vertices.getLast ⋯

@[simp]

theorem LGV.SimpleDigraph.Path.start_mk {V : Type u_1} {D : SimpleDigraph V} (vs : List V) (hne : vs ≠ []) (harcs : ∀ (i : ℕ) (hi : i + 1 < vs.length), D.arc (vs.get ⟨i, ⋯⟩) (vs.get ⟨i + 1, hi⟩)) : { vertices := vs, nonempty := hne, arcs_valid := harcs }.start = vs.head hne

Simp lemma for Path.start on a constructed path

@[simp]

theorem LGV.SimpleDigraph.Path.finish_mk {V : Type u_1} {D : SimpleDigraph V} (vs : List V) (hne : vs ≠ []) (harcs : ∀ (i : ℕ) (hi : i + 1 < vs.length), D.arc (vs.get ⟨i, ⋯⟩) (vs.get ⟨i + 1, hi⟩)) : { vertices := vs, nonempty := hne, arcs_valid := harcs }.finish = vs.getLast hne

Simp lemma for Path.finish on a constructed path

def LGV.SimpleDigraph.IsPathFinite {V : Type u_1} (D : SimpleDigraph V) : Prop

A digraph is path-finite if there are only finitely many paths between any two vertices. Convention conv.lgv.digraph(b)

Equations

• D.IsPathFinite = ∀ (u v : V), {p : D.Path | p.start = u ∧ p.finish = v}.Finite

def LGV.SimpleDigraph.IsAcyclic {V : Type u_1} (D : SimpleDigraph V) : Prop

A digraph is acyclic if it has no directed cycles. Convention conv.lgv.digraph(c)

Equations

• D.IsAcyclic = ∀ (p : D.Path), p.start = p.finish → p.vertices.length = 1

def LGV.SimpleDigraph.Path.subpath {V : Type u_1} {D : SimpleDigraph V} (p : D.Path) (i j : ℕ) (hij : i ≤ j) (hj : j < p.vertices.length) : D.Path

Extract a subpath from index i to index j (inclusive). The resulting path has j - i + 1 vertices.

Equations

• p.subpath i j hij hj = { vertices := List.take (j - i + 1) (List.drop i p.vertices), nonempty := ⋯, arcs_valid := ⋯ }

theorem LGV.SimpleDigraph.Path.subpath_start {V : Type u_1} {D : SimpleDigraph V} (p : D.Path) (i j : ℕ) (hij : i ≤ j) (hj : j < p.vertices.length) : (p.subpath i j hij hj).start = p.vertices.get ⟨i, ⋯⟩

The start of a subpath is the vertex at index i.

theorem LGV.SimpleDigraph.Path.subpath_finish {V : Type u_1} {D : SimpleDigraph V} (p : D.Path) (i j : ℕ) (hij : i ≤ j) (hj : j < p.vertices.length) : (p.subpath i j hij hj).finish = p.vertices.get ⟨j, hj⟩

The finish of a subpath is the vertex at index j.

theorem LGV.SimpleDigraph.Path.subpath_length {V : Type u_1} {D : SimpleDigraph V} (p : D.Path) (i j : ℕ) (hij : i ≤ j) (hj : j < p.vertices.length) : (p.subpath i j hij hj).vertices.length = j - i + 1

The length of a subpath from i to j is j - i + 1.

theorem LGV.SimpleDigraph.Path.vertices_nodup_of_acyclic {V : Type u_1} {D : SimpleDigraph V} (hac : D.IsAcyclic) (p : D.Path) : p.vertices.Nodup

In an acyclic digraph, all vertices on a path are distinct. This follows from the fact that if a vertex appears twice, we could extract a cycle (a path from that vertex back to itself).

Conversion to Mathlib's Digraph

LGV.SimpleDigraph is a specialized digraph structure that enforces irreflexivity (no self-loops). Mathlib's Digraph is more general and allows self-loops.

We provide a conversion that forgets the irreflexivity proof, allowing use of Mathlib's digraph infrastructure when needed.

def LGV.SimpleDigraph.toDigraph {V : Type u_2} (D : SimpleDigraph V) : Digraph V

Convert a SimpleDigraph to Mathlib's Digraph. This forgets the irreflexivity proof but preserves the adjacency relation.

Note: LGV1.lean uses Mathlib's Digraph directly, while LGV2.lean uses this SimpleDigraph structure. This conversion enables interoperability.

Equations

• D.toDigraph = { Adj := D.arc }

@[simp]

theorem LGV.SimpleDigraph.toDigraph_adj {V : Type u_2} (D : SimpleDigraph V) (u v : V) : D.toDigraph.Adj u v ↔ D.arc u v

The adjacency relation is preserved by toDigraph.

The Integer Lattice ℤ²

Definition def.lgv.lattice: The integer lattice has vertex set ℤ² with arcs (i,j) → (i+1,j) (east-steps) and (i,j) → (i,j+1) (north-steps).

Relationship with LGV1.lean

LGV1.lean defines LGV.integerLattice : Digraph LatticePoint using Mathlib's Digraph. This file defines LGV.integerLattice : SimpleDigraph (ℤ × ℤ) using our custom structure.

The two definitions have semantically identical adjacency relations:

• LGV1: IntegerLatticeAdj p q ↔ q = (p.1 + 1, p.2) ∨ q = (p.1, p.2 + 1)
• LGV2: integerLattice.arc u v ↔ (v.1 = u.1 + 1 ∧ v.2 = u.2) ∨ (v.1 = u.1 ∧ v.2 = u.2 + 1)

The lemma integerLattice_arc_iff proves these are equivalent, enabling results from either file to be transferred to the other.

def LGV.integerLattice : SimpleDigraph (ℤ × ℤ)

The integer lattice digraph ℤ².

This is the same lattice as in LGV1.lean, but using SimpleDigraph instead of Mathlib's Digraph. See integerLattice_arc_iff for the characterization and integerLattice_toDigraph_adj_iff for the equivalence with LGV1's definition.

Equations

• LGV.integerLattice = { arc := fun (u v : ℤ × ℤ) => v.1 = u.1 + 1 ∧ v.2 = u.2 ∨ v.1 = u.1 ∧ v.2 = u.2 + 1, arc_irrefl := LGV.integerLattice._proof_1 }

theorem LGV.integerLattice_arc_iff (u v : ℤ × ℤ) : integerLattice.arc u v ↔ v = (u.1 + 1, u.2) ∨ v = (u.1, u.2 + 1)

Characterization of adjacency in the integer lattice. An arc exists from u to v iff v is one step east or north of u.

This matches the form of integerLattice_adj_iff in LGV1.lean.

theorem LGV.integerLattice_toDigraph_adj_iff (u v : ℤ × ℤ) : integerLattice.toDigraph.Adj u v ↔ v = (u.1 + 1, u.2) ∨ v = (u.1, u.2 + 1)

The integer lattice adjacency relation in LGV2 matches the one in LGV1.

This bridges the two definitions:

• LGV1.lean: integerLattice.Adj p q where integerLattice : Digraph LatticePoint
• LGV2.lean: integerLattice.arc u v where integerLattice : SimpleDigraph (ℤ × ℤ)

Both are equivalent to: v = (u.1 + 1, u.2) ∨ v = (u.1, u.2 + 1)

theorem LGV.integerLattice_path_length_eq (p : integerLattice.Path) : ↑p.vertices.length = p.finish.1 + p.finish.2 - p.start.1 - p.start.2 + 1

Path length is determined by start and finish coordinates

theorem LGV.integerLattice_path_vertex_sum (p : integerLattice.Path) (i : ℕ) (hi : i < p.vertices.length) : (p.vertices.get ⟨i, hi⟩).1 + (p.vertices.get ⟨i, hi⟩).2 = p.start.1 + p.start.2 + ↑i

Sum at vertex i equals start sum + i

theorem LGV.integerLattice_path_x_step (p : integerLattice.Path) (i : ℕ) (hi : i + 1 < p.vertices.length) : (p.vertices.get ⟨i + 1, hi⟩).1 - (p.vertices.get ⟨i, ⋯⟩).1 = 0 ∨ (p.vertices.get ⟨i + 1, hi⟩).1 - (p.vertices.get ⟨i, ⋯⟩).1 = 1

x-coordinate change at each step is 0 or 1

theorem LGV.integerLattice_path_vertices_bounded (p : integerLattice.Path) (i : ℕ) (hi : i < p.vertices.length) : p.start.1 ≤ (p.vertices.get ⟨i, hi⟩).1 ∧ (p.vertices.get ⟨i, hi⟩).1 ≤ p.finish.1 ∧ p.start.2 ≤ (p.vertices.get ⟨i, hi⟩).2 ∧ (p.vertices.get ⟨i, hi⟩).2 ≤ p.finish.2

Vertices of a lattice path are bounded by start and finish coordinates

theorem LGV.integerLattice_acyclic : integerLattice.IsAcyclic

The integer lattice is acyclic

theorem LGV.integerLattice_pathFinite : integerLattice.IsPathFinite

The integer lattice is path-finite

Path Weights

For each arc, we assign a weight from a commutative ring K. The weight of a path is the product of its arc weights.

def LGV.ArcWeight {V : Type u_1} (D : SimpleDigraph V) (K : Type u_3) : Type (max u_1 u_3)

An arc weight function assigns a ring element to each arc. Definition in Theorem thm.lgv.kpaths.wt

Equations

• LGV.ArcWeight D K = ((u v : V) → D.arc u v → K)

noncomputable def LGV.pathWeightAux {V : Type u_1} {K : Type u_2} [CommRing K] {D : SimpleDigraph V} (w : ArcWeight D K) (vertices : List V) (arcs_valid : ∀ (i : ℕ) (hi : i + 1 < vertices.length), D.arc (vertices.get ⟨i, ⋯⟩) (vertices.get ⟨i + 1, hi⟩)) : K

Helper function to compute the product of arc weights along a vertex list. Uses recursion on the structure of the list.

• For an empty list or single vertex, the weight is 1 (no arcs).
• For a list [v₀, v₁, ...], the weight is w(v₀, v₁) * (weight of [v₁, ...]).

Equations

• LGV.pathWeightAux w [] arcs_valid_2 = 1
• LGV.pathWeightAux w [head] arcs_valid_2 = 1
• LGV.pathWeightAux w (v₀ :: v₁ :: rest) arcs_valid_2 = w v₀ v₁ ⋯ * LGV.pathWeightAux w (v₁ :: rest) ⋯

noncomputable def LGV.pathWeight {V : Type u_1} {K : Type u_2} [CommRing K] {D : SimpleDigraph V} (w : ArcWeight D K) (p : D.Path) : K

The weight of a path is the product of weights of its arcs. w(p) := ∏_{a is an arc of p} w(a)

Equations

• LGV.pathWeight w p = LGV.pathWeightAux w p.vertices ⋯

theorem LGV.pathWeightAux_proof_irrel {V : Type u_1} {K : Type u_2} [CommRing K] {D : SimpleDigraph V} (w : ArcWeight D K) (l : List V) (arcs1 arcs2 : ∀ (i : ℕ) (hi : i + 1 < l.length), D.arc (l.get ⟨i, ⋯⟩) (l.get ⟨i + 1, hi⟩)) : pathWeightAux w l arcs1 = pathWeightAux w l arcs2

pathWeightAux is independent of the proof of arcs_valid (proof irrelevance).

theorem LGV.pathWeightAux_eq_of_eq {V : Type u_1} {K : Type u_2} [CommRing K] {D : SimpleDigraph V} (w : ArcWeight D K) {l1 l2 : List V} (h : l1 = l2) (arcs1 : ∀ (i : ℕ) (hi : i + 1 < l1.length), D.arc (l1.get ⟨i, ⋯⟩) (l1.get ⟨i + 1, hi⟩)) (arcs2 : ∀ (i : ℕ) (hi : i + 1 < l2.length), D.arc (l2.get ⟨i, ⋯⟩) (l2.get ⟨i + 1, hi⟩)) : pathWeightAux w l1 arcs1 = pathWeightAux w l2 arcs2

pathWeightAux equality when lists are equal (combines substitution with proof irrelevance).

@[simp]

theorem LGV.pathWeightAux_singleton {V : Type u_1} {K : Type u_2} [CommRing K] {D : SimpleDigraph V} (w : ArcWeight D K) (v : V) (arcs_valid : ∀ (i : ℕ) (hi : i + 1 < [v].length), D.arc ([v].get ⟨i, ⋯⟩) ([v].get ⟨i + 1, hi⟩)) : pathWeightAux w [v] arcs_valid = 1

pathWeightAux of a singleton list is 1.

theorem LGV.pathWeightAux_pair {V : Type u_1} {K : Type u_2} [CommRing K] {D : SimpleDigraph V} (w : ArcWeight D K) (u v : V) (arcs_valid : ∀ (i : ℕ) (hi : i + 1 < [u, v].length), D.arc ([u, v].get ⟨i, ⋯⟩) ([u, v].get ⟨i + 1, hi⟩)) : pathWeightAux w [u, v] arcs_valid = w u v ⋯

pathWeightAux of a two-element list is just the arc weight.

theorem LGV.pathWeightAux_cons_cons {V : Type u_1} {K : Type u_2} [CommRing K] {D : SimpleDigraph V} (w : ArcWeight D K) (u v : V) (rest : List V) (arcs_valid : ∀ (i : ℕ) (hi : i + 1 < (u :: v :: rest).length), D.arc ((u :: v :: rest).get ⟨i, ⋯⟩) ((u :: v :: rest).get ⟨i + 1, hi⟩)) (rest_arcs : ∀ (i : ℕ) (hi : i + 1 < (v :: rest).length), D.arc ((v :: rest).get ⟨i, ⋯⟩) ((v :: rest).get ⟨i + 1, hi⟩)) (arc_uv : D.arc u v) : pathWeightAux w (u :: v :: rest) arcs_valid = w u v arc_uv * pathWeightAux w (v :: rest) rest_arcs

pathWeightAux of a cons-cons list factors into an arc weight times the tail.

theorem LGV.pathWeightAux_append {V : Type u_1} {K : Type u_2} [CommRing K] {D : SimpleDigraph V} (w : ArcWeight D K) (l1 l2 : List V) (h1_ne : l1 ≠ []) (h2_ne : l2 ≠ []) (h_join : l1.getLast h1_ne = l2.head h2_ne) (arcs1 : ∀ (i : ℕ) (hi : i + 1 < l1.length), D.arc (l1.get ⟨i, ⋯⟩) (l1.get ⟨i + 1, hi⟩)) (arcs2 : ∀ (i : ℕ) (hi : i + 1 < l2.length), D.arc (l2.get ⟨i, ⋯⟩) (l2.get ⟨i + 1, hi⟩)) (arcs_concat : ∀ (i : ℕ) (hi : i + 1 < (l1 ++ l2.tail).length), D.arc ((l1 ++ l2.tail).get ⟨i, ⋯⟩) ((l1 ++ l2.tail).get ⟨i + 1, hi⟩)) : pathWeightAux w (l1 ++ l2.tail) arcs_concat = pathWeightAux w l1 arcs1 * pathWeightAux w l2 arcs2

pathWeightAux is multiplicative over list append when the lists share a common vertex. If l1 = [..., v] and l2 = [v, ...], then pathWeightAux (l1 ++ l2.tail) = pathWeightAux l1 * pathWeightAux l2.

noncomputable def LGV.pathTupleWeight {V : Type u_1} {K : Type u_2} [CommRing K] {D : SimpleDigraph V} {k : ℕ} (w : ArcWeight D K) (ps : Fin k → D.Path) : K

The weight of a path tuple is the product of weights of its component paths. w(𝐩) := w(p₁) w(p₂) ⋯ w(pₖ)

Equations

• LGV.pathTupleWeight w ps = ∏ i : Fin k, LGV.pathWeight w (ps i)

k-Vertices and Path Tuples

Definition def.lgv.path-tups: A k-vertex is a k-tuple of vertices. A path tuple from 𝐀 to 𝐁 is a k-tuple of paths where pᵢ goes from Aᵢ to Bᵢ.

@[reducible, inline]

abbrev LGV.kVertex (V : Type u_3) (k : ℕ) : Type u_3

A k-vertex is a k-tuple of vertices of D. Definition def.lgv.path-tups(a)

Equations

• LGV.kVertex V k = (Fin k → V)

def LGV.permuteKVertex {V : Type u_3} {k : ℕ} (σ : Equiv.Perm (Fin k)) (A : kVertex V k) : kVertex V k

Permute a k-vertex by a permutation σ: σ(𝐀) = (A_{σ(1)}, A_{σ(2)}, ..., A_{σ(k)}). Definition def.lgv.path-tups(b)

Equations

• LGV.permuteKVertex σ A i = A (σ i)

structure LGV.PathTuple {V : Type u_3} [DecidableEq V] (D : SimpleDigraph V) (k : ℕ) (A B : kVertex V k) : Type u_3

A path tuple from 𝐀 to 𝐁 is a k-tuple (p₁, ..., pₖ) where pᵢ is a path from Aᵢ to Bᵢ. Definition def.lgv.path-tups(c)

• paths : Fin k → D.Path

  The paths in the tuple

• starts (i : Fin k) : (self.paths i).start = A i

  Each path starts at the corresponding source vertex

• finishes (i : Fin k) : (self.paths i).finish = B i

  Each path ends at the corresponding target vertex

theorem LGV.PathTuple.ext {V : Type u_3} [DecidableEq V] {D : SimpleDigraph V} {k : ℕ} {A B : kVertex V k} (pt1 pt2 : PathTuple D k A B) (h : ∀ (i : Fin k), pt1.paths i = pt2.paths i) : pt1 = pt2

theorem LGV.PathTuple.ext_iff {V : Type u_3} [DecidableEq V] {D : SimpleDigraph V} {k : ℕ} {A B : kVertex V k} {pt1 pt2 : PathTuple D k A B} : pt1 = pt2 ↔ ∀ (i : Fin k), pt1.paths i = pt2.paths i

def LGV.pathsIntersect {V : Type u_3} [DecidableEq V] {D : SimpleDigraph V} (p q : D.Path) : Prop

Two paths have a vertex in common

Equations

• LGV.pathsIntersect p q = ∃ v ∈ p.vertices, v ∈ q.vertices

def LGV.PathTuple.isNonIntersecting {V : Type u_3} [DecidableEq V] {D : SimpleDigraph V} {k : ℕ} {A B : kVertex V k} (pt : PathTuple D k A B) : Prop

A path tuple is non-intersecting (nipat) if no two paths share a vertex. Definition def.lgv.path-tups(d)

Equations

• pt.isNonIntersecting = ∀ (i j : Fin k), i ≠ j → ¬LGV.pathsIntersect (pt.paths i) (pt.paths j)

def LGV.PathTuple.isIntersecting {V : Type u_3} [DecidableEq V] {D : SimpleDigraph V} {k : ℕ} {A B : kVertex V k} (pt : PathTuple D k A B) : Prop

A path tuple is intersecting (ipat) if some two paths share a vertex. Definition def.lgv.path-tups(e)

Equations

• pt.isIntersecting = ¬pt.isNonIntersecting

The Path Weight Matrix

The matrix M where M_{i,j} = ∑_{p : Aᵢ → Bⱼ} w(p).

noncomputable def LGV.pathsFromTo {V : Type u_3} [DecidableEq V] (D : SimpleDigraph V) (hpf : D.IsPathFinite) (u v : V) : Finset D.Path

The set of paths from u to v in a path-finite digraph

Equations

• LGV.pathsFromTo D hpf u v = ⋯.toFinset

noncomputable def LGV.pathWeightSum {K : Type u_2} [CommRing K] {V : Type u_3} [DecidableEq V] {D : SimpleDigraph V} (hpf : D.IsPathFinite) (w : ArcWeight D K) (u v : V) : K

The sum of weights of all paths from u to v. ∑_{p : u → v} w(p)

Equations

• LGV.pathWeightSum hpf w u v = ∑ p ∈ LGV.pathsFromTo D hpf u v, LGV.pathWeight w p

noncomputable def LGV.pathWeightMatrix {K : Type u_2} [CommRing K] {V : Type u_3} [DecidableEq V] {D : SimpleDigraph V} (hpf : D.IsPathFinite) (w : ArcWeight D K) {k : ℕ} (A B : kVertex V k) : Matrix (Fin k) (Fin k) K

The path weight matrix M_{i,j} = ∑_{p : Aᵢ → Bⱼ} w(p)

Equations

• LGV.pathWeightMatrix hpf w A B = Matrix.of fun (i j : Fin k) => LGV.pathWeightSum hpf w (A i) (B j)

LGV Lemma: Weighted Lattice Version

Theorem thm.lgv.kpaths.wt: For the integer lattice with arc weights w, det(M) = ∑{σ ∈ Sₖ} (-1)^σ ∑{𝐩 nipat from 𝐀 to σ(𝐁)} w(𝐩)

noncomputable def LGV.nipatSet {V : Type u_3} [DecidableEq V] {D : SimpleDigraph V} {k : ℕ} (A B : kVertex V k) : Set (PathTuple D k A B)

The set of non-intersecting path tuples from 𝐀 to 𝐁

Equations

• LGV.nipatSet A B = {pt : LGV.PathTuple D k A B | pt.isNonIntersecting}

noncomputable def LGV.nipatSetFinite {V : Type u_3} [DecidableEq V] {D : SimpleDigraph V} (hpf : D.IsPathFinite) {k : ℕ} (A B : kVertex V k) : (nipatSet A B).Finite

The set of nipats is finite (follows from path-finiteness)

Equations

• ⋯ = ⋯

noncomputable def LGV.nipatFinset {V : Type u_3} [DecidableEq V] {D : SimpleDigraph V} (hpf : D.IsPathFinite) {k : ℕ} (A B : kVertex V k) : Finset (PathTuple D k A B)

Convert nipatSet to Finset using the finiteness proof

Equations

• LGV.nipatFinset hpf A B = ⋯.toFinset

theorem LGV.nipatFinset_of_empty {V : Type u_3} [DecidableEq V] {D : SimpleDigraph V} (hpf : D.IsPathFinite) {k : ℕ} (A B : kVertex V k) (h : nipatSet A B = ∅) : nipatFinset hpf A B = ∅

When nipatSet is empty, nipatFinset is empty

noncomputable def LGV.nipatWeightSum {K : Type u_2} [CommRing K] {V : Type u_3} [DecidableEq V] {D : SimpleDigraph V} (hpf : D.IsPathFinite) (w : ArcWeight D K) {k : ℕ} (A B : kVertex V k) (_σ : Equiv.Perm (Fin k)) : K

Sum of weights over all nipats from 𝐀 to 𝐁 Note: σ is not used in this definition since the permutation is already encoded in B (which should be permuteKVertex σ B' for some B')

Equations

• LGV.nipatWeightSum hpf w A B _σ = ∑ pt ∈ LGV.nipatFinset hpf A B, LGV.pathTupleWeight w pt.paths

Path Tuple Infrastructure for LGV

The key step in the LGV proof is to express the product of sums as a sum over path tuples: ∏j (∑{p : A_j → B_j} w(p)) = ∑_{pt : PathTuple} pathTupleWeight w pt.paths

This uses Finset.prod_univ_sum and a bijection between PathTuple and the piFinset.

noncomputable def LGV.pathTupleEquivPiFinset {V : Type u_3} [DecidableEq V] {D : SimpleDigraph V} (hpf : D.IsPathFinite) {k : ℕ} (A B : kVertex V k) : PathTuple D k A B ≃ ↥(Fintype.piFinset fun (j : Fin k) => pathsFromTo D hpf (A j) (B j))

Bijection between PathTuple and the piFinset of pathsFromTo. This is the key to converting the product of sums to a sum over path tuples.

Equations

• One or more equations did not get rendered due to their size.

LGV Lemma: General Digraph Version

Theorem thm.lgv.kpaths.wt-dg: The same result holds for any path-finite acyclic digraph.

The proof uses a sign-reversing involution on intersecting path tuples. The key steps are:

1. Express det(M) using the Leibniz formula as ∑_σ (-1)^σ ∏i M{i,σ(i)}
2. Expand each product as a sum over path tuples from 𝐀 to σ(𝐁)
3. Define a sign-reversing involution f on intersecting path tuples:
   • Find the first crowded point (vertex in multiple paths)
   • Pick the smallest index i whose path contains a crowded point
   • Pick the first crowded point v on path p_i
   • Pick the largest index j such that v is on path p_j
   • Exchange the tails of p_i and p_j at v
   • This maps (σ, 𝐩) to (σ ∘ t_{i,j}, 𝐩'), where t_{i,j} is the transposition
4. The involution preserves weight but flips sign, so intersecting tuples cancel
5. Only non-intersecting path tuples (nipats) contribute to the sum

def LGV.PathTuple.isCrowded {V : Type u_3} [DecidableEq V] {D : SimpleDigraph V} {k : ℕ} {A B : kVertex V k} (pt : PathTuple D k A B) (v : V) : Prop

A crowded point in a path tuple is a vertex that appears in at least two paths

Equations

• pt.isCrowded v = ∃ (i : Fin k) (j : Fin k), i ≠ j ∧ v ∈ (pt.paths i).vertices ∧ v ∈ (pt.paths j).vertices

theorem LGV.PathTuple.isIntersecting_iff_exists_crowded {V : Type u_3} [DecidableEq V] {D : SimpleDigraph V} {k : ℕ} {A B : kVertex V k} (pt : PathTuple D k A B) : pt.isIntersecting ↔ ∃ (v : V), pt.isCrowded v

An intersecting path tuple has at least one crowded point

def LGV.pathTupleWithPerm {V : Type u_3} [DecidableEq V] {D : SimpleDigraph V} {k : ℕ} (A B : kVertex V k) : Type u_3

The set of path tuples from 𝐀 to σ(𝐁) paired with the permutation σ

Equations

• LGV.pathTupleWithPerm A B = ((σ : Equiv.Perm (Fin k)) × LGV.PathTuple D k A (LGV.permuteKVertex σ B))

def LGV.signOfPathTupleWithPerm {V : Type u_3} [DecidableEq V] {D : SimpleDigraph V} {k : ℕ} {A B : kVertex V k} (sp : pathTupleWithPerm A B) : ℤˣ

The sign of a path tuple with permutation is (-1)^σ

Equations

• LGV.signOfPathTupleWithPerm sp = Equiv.Perm.sign sp.fst

noncomputable def LGV.weightOfPathTupleWithPerm {K : Type u_2} [CommRing K] {V : Type u_3} [DecidableEq V] {D : SimpleDigraph V} {k : ℕ} {A B : kVertex V k} (w : ArcWeight D K) (sp : pathTupleWithPerm A B) : K

The weight of a path tuple with permutation

Equations

• LGV.weightOfPathTupleWithPerm w sp = LGV.pathTupleWeight w sp.snd.paths

def LGV.firstIndexIn {V : Type u_3} [DecidableEq V] {D : SimpleDigraph V} (p : D.Path) (v : V) : ℕ

The index of the first occurrence of a vertex in a path's vertex list

Equations

• LGV.firstIndexIn p v = List.findIdx (fun (x : V) => decide (x = v)) p.vertices

theorem LGV.first_intersection_unique {V : Type u_3} [DecidableEq V] {D : SimpleDigraph V} (_hac : D.IsAcyclic) (p q : D.Path) (hp : pathsIntersect p q) : ∃! v : V, v ∈ p.vertices ∧ v ∈ q.vertices ∧ ∀ v' ∈ p.vertices, v' ∈ q.vertices → firstIndexIn p v ≤ firstIndexIn p v'

In an acyclic digraph, the first intersection of two paths (if they intersect) is well-defined: it's the same whether we look from path p or path q. This is because if they were different, we could form a cycle.

noncomputable def LGV.SimpleDigraph.Path.splitAt {V : Type u_3} [DecidableEq V] {D : SimpleDigraph V} (p : D.Path) (v : V) (hv : v ∈ p.vertices) : D.Path × D.Path

Split a path at a vertex v, returning (head ending at v, tail starting at v). The head includes v, the tail starts at v.

Equations

• One or more equations did not get rendered due to their size.

theorem LGV.SimpleDigraph.Path.splitAt_head_finish {V : Type u_3} [DecidableEq V] {D : SimpleDigraph V} (p : D.Path) (v : V) (hv : v ∈ p.vertices) : (p.splitAt v hv).1.finish = v

The head of splitAt ends at v

theorem LGV.SimpleDigraph.Path.splitAt_tail_start {V : Type u_3} [DecidableEq V] {D : SimpleDigraph V} (p : D.Path) (v : V) (hv : v ∈ p.vertices) : (p.splitAt v hv).2.start = v

The tail of splitAt starts at v

noncomputable def LGV.SimpleDigraph.Path.concat {V : Type u_3} {D : SimpleDigraph V} (p q : D.Path) (hpq : p.finish = q.start) : D.Path

Concatenate two paths where the first path ends at v and the second starts at v. The resulting path goes from the start of the first to the end of the second. The vertex v appears once in the result (not duplicated).

Equations

• p.concat q hpq = { vertices := p.vertices ++ q.vertices.tail, nonempty := ⋯, arcs_valid := ⋯ }

theorem LGV.SimpleDigraph.Path.concat_start {V : Type u_3} {D : SimpleDigraph V} (p q : D.Path) (hpq : p.finish = q.start) : (p.concat q hpq).start = p.start

The concatenation of two paths starts at the first path's start

theorem LGV.SimpleDigraph.Path.concat_finish {V : Type u_3} {D : SimpleDigraph V} (p q : D.Path) (hpq : p.finish = q.start) : (p.concat q hpq).finish = q.finish

The concatenation of two paths ends at the second path's finish

theorem LGV.pathWeight_concat {K : Type u_2} [CommRing K] {V : Type u_3} {D : SimpleDigraph V} (w : ArcWeight D K) (p q : D.Path) (hpq : p.finish = q.start) : pathWeight w (p.concat q hpq) = pathWeight w p * pathWeight w q

pathWeight is multiplicative over path concatenation.

theorem LGV.pathWeight_splitAt {K : Type u_2} [CommRing K] {V : Type u_3} [DecidableEq V] {D : SimpleDigraph V} (w : ArcWeight D K) (p : D.Path) (v : V) (hv : v ∈ p.vertices) : pathWeight w p = pathWeight w (p.splitAt v hv).1 * pathWeight w (p.splitAt v hv).2

pathWeight factors over splitAt: the weight of a path is the product of the weights of its head and tail after splitting at any vertex.

theorem LGV.SimpleDigraph.Path.splitAt_head_start {V : Type u_3} [DecidableEq V] {D : SimpleDigraph V} (p : D.Path) (v : V) (hv : v ∈ p.vertices) : (p.splitAt v hv).1.start = p.start

The head of splitAt starts at the original path's start

theorem LGV.SimpleDigraph.Path.splitAt_tail_finish {V : Type u_3} [DecidableEq V] {D : SimpleDigraph V} (p : D.Path) (v : V) (hv : v ∈ p.vertices) : (p.splitAt v hv).2.finish = p.finish

The tail of splitAt ends at the original path's finish

noncomputable def LGV.exchangeTails {V : Type u_3} [DecidableEq V] {D : SimpleDigraph V} (p q : D.Path) (v : V) (hv_p : v ∈ p.vertices) (hv_q : v ∈ q.vertices) : D.Path × D.Path

Exchange the tails of two paths at a common vertex. If p goes A → v → B and q goes A' → v → B', then after exchange: p' goes A → v → B' and q' goes A' → v → B

Equations

• LGV.exchangeTails p q v hv_p hv_q = ((p.splitAt v hv_p).1.concat (q.splitAt v hv_q).2 ⋯, (q.splitAt v hv_q).1.concat (p.splitAt v hv_p).2 ⋯)

theorem LGV.exchangeTails_fst_start {V : Type u_3} [DecidableEq V] {D : SimpleDigraph V} (p q : D.Path) (v : V) (hv_p : v ∈ p.vertices) (hv_q : v ∈ q.vertices) : (exchangeTails p q v hv_p hv_q).1.start = p.start

The first path from exchangeTails starts at the original first path's start

theorem LGV.exchangeTails_fst_finish {V : Type u_3} [DecidableEq V] {D : SimpleDigraph V} (p q : D.Path) (v : V) (hv_p : v ∈ p.vertices) (hv_q : v ∈ q.vertices) : (exchangeTails p q v hv_p hv_q).1.finish = q.finish

The first path from exchangeTails ends at the original second path's finish

theorem LGV.exchangeTails_snd_start {V : Type u_3} [DecidableEq V] {D : SimpleDigraph V} (p q : D.Path) (v : V) (hv_p : v ∈ p.vertices) (hv_q : v ∈ q.vertices) : (exchangeTails p q v hv_p hv_q).2.start = q.start

The second path from exchangeTails starts at the original second path's start

theorem LGV.exchangeTails_snd_finish {V : Type u_3} [DecidableEq V] {D : SimpleDigraph V} (p q : D.Path) (v : V) (hv_p : v ∈ p.vertices) (hv_q : v ∈ q.vertices) : (exchangeTails p q v hv_p hv_q).2.finish = p.finish

The second path from exchangeTails ends at the original first path's finish

theorem LGV.SimpleDigraph.Path.concat_mem_of_finish {V : Type u_3} {D : SimpleDigraph V} (p q : D.Path) (hpq : p.finish = q.start) : p.finish ∈ (p.concat q hpq).vertices

If p.finish = v, then v is in (concat p q).vertices

theorem LGV.exchangeTails_fst_mem_v {V : Type u_3} [DecidableEq V] {D : SimpleDigraph V} (p q : D.Path) (v : V) (hv_p : v ∈ p.vertices) (hv_q : v ∈ q.vertices) : v ∈ (exchangeTails p q v hv_p hv_q).1.vertices

The crowded point v is in the first exchanged path's vertices. Since head_p ends at v, and concat uses head_p.vertices ++ tail_q.vertices.tail, v is in the first path.

theorem LGV.exchangeTails_snd_mem_v {V : Type u_3} [DecidableEq V] {D : SimpleDigraph V} (p q : D.Path) (v : V) (hv_p : v ∈ p.vertices) (hv_q : v ∈ q.vertices) : v ∈ (exchangeTails p q v hv_p hv_q).2.vertices

The crowded point v is in the second exchanged path's vertices. Since head_q ends at v, and concat uses head_q.vertices ++ tail_p.vertices.tail, v is in the second path.

theorem LGV.exchangeTails_involutive {V : Type u_3} [DecidableEq V] {D : SimpleDigraph V} (_hac : D.IsAcyclic) (p q : D.Path) (v : V) (hv_p : v ∈ p.vertices) (hv_q : v ∈ q.vertices) : let p' := (exchangeTails p q v hv_p hv_q).1; let q' := (exchangeTails p q v hv_p hv_q).2; have hv_p' := ⋯; have hv_q' := ⋯; exchangeTails p' q' v hv_p' hv_q' = (p, q)

theorem LGV.exchangeTails_head_eq {V : Type u_3} [DecidableEq V] {D : SimpleDigraph V} (_hac : D.IsAcyclic) (p q : D.Path) (v : V) (hv_p : v ∈ p.vertices) (hv_q : v ∈ q.vertices) : let p' := (exchangeTails p q v hv_p hv_q).1; have hv_p' := ⋯; (p'.splitAt v hv_p').1.vertices = (p.splitAt v hv_p).1.vertices

The head of path p (vertices before v) is preserved after exchangeTails. This is the key lemma for proving that the canonical selection is invariant.

theorem LGV.exchangeTails_weight {K : Type u_2} [CommRing K] {V : Type u_3} [DecidableEq V] {D : SimpleDigraph V} (w : ArcWeight D K) (p q : D.Path) (v : V) (hv_p : v ∈ p.vertices) (hv_q : v ∈ q.vertices) : pathWeight w p * pathWeight w q = pathWeight w (exchangeTails p q v hv_p hv_q).1 * pathWeight w (exchangeTails p q v hv_p hv_q).2

Exchanging tails preserves the total weight.

Proof outline: The key insight is that pathWeight is multiplicative over path concatenation: if p = p₁ ++ p₂ (concatenation at a shared vertex), then w(p) = w(p₁) * w(p₂).

When we exchange tails at vertex v:

• p has weight w(p_head) * w(p_tail) where p_head ends at v and p_tail starts at v
• q has weight w(q_head) * w(q_tail) where q_head ends at v and q_tail starts at v
• p' = p_head ++ q_tail has weight w(p_head) * w(q_tail)
• q' = q_head ++ p_tail has weight w(q_head) * w(p_tail)

Thus: w(p) * w(q) = w(p_head) * w(p_tail) * w(q_head) * w(q_tail) = w(p_head) * w(q_tail) * w(q_head) * w(p_tail) (by commutativity) = w(p') * w(q')

Status: Now that exchangeTails is defined, the proof follows from multiplicativity of pathWeight and commutativity of multiplication in K. The proof requires showing pathWeight is multiplicative over path concatenation.

Deterministic Intersection Data Selection

The sign-reversing involution requires selecting intersection data (i, j, v) deterministically so that applying the involution twice returns the original path tuple. The algorithm from the LaTeX source is:

1. Pick the smallest i such that path i contains a crowded point
2. Pick the first crowded point v on path i (by position in the path)
3. Pick the largest j such that v is on path j

This selection is preserved under the involution because:

• The heads of paths i and j (before v) are unchanged
• So v is still the first crowded point on path i
• And j is still the largest index containing v

def LGV.PathTuple.crowdedPathIndices {V : Type u_3} [DecidableEq V] {D : SimpleDigraph V} {k : ℕ} {A B : kVertex V k} (pt : PathTuple D k A B) : Finset (Fin k)

The set of path indices that have a crowded vertex (shared with another path)

Equations

• pt.crowdedPathIndices = {i : Fin k | ∃ (j : Fin k), i ≠ j ∧ ((pt.paths i).vertices.toFinset ∩ (pt.paths j).vertices.toFinset).Nonempty}

def LGV.PathTuple.crowdedVerticesOnPath {V : Type u_3} [DecidableEq V] {D : SimpleDigraph V} {k : ℕ} {A B : kVertex V k} (pt : PathTuple D k A B) (i : Fin k) : Finset V

The set of crowded vertices on a specific path

Equations

• pt.crowdedVerticesOnPath i = {v ∈ (pt.paths i).vertices.toFinset | ∃ (j : Fin k), i ≠ j ∧ v ∈ (pt.paths j).vertices}

def LGV.PathTuple.pathIndicesContaining {V : Type u_3} [DecidableEq V] {D : SimpleDigraph V} {k : ℕ} {A B : kVertex V k} (pt : PathTuple D k A B) (v : V) : Finset (Fin k)

The set of path indices that contain a given vertex

Equations

• pt.pathIndicesContaining v = {i : Fin k | v ∈ (pt.paths i).vertices}

def LGV.PathTuple.firstCrowdedIndexOnPath {V : Type u_3} [DecidableEq V] {D : SimpleDigraph V} {k : ℕ} {A B : kVertex V k} (pt : PathTuple D k A B) (i : Fin k) : ℕ

The index of the first crowded vertex on a path (by position)

Equations

• pt.firstCrowdedIndexOnPath i = List.findIdx (fun (v : V) => decide (v ∈ pt.crowdedVerticesOnPath i)) (pt.paths i).vertices

theorem LGV.PathTuple.isIntersecting_iff_crowdedPathIndices_nonempty {V : Type u_3} [DecidableEq V] {D : SimpleDigraph V} {k : ℕ} {A B : kVertex V k} (pt : PathTuple D k A B) : pt.isIntersecting ↔ pt.crowdedPathIndices.Nonempty

An intersecting path tuple has nonempty crowdedPathIndices

theorem LGV.PathTuple.crowded_vertex_other_paths_gt {V : Type u_3} [DecidableEq V] {D : SimpleDigraph V} {k : ℕ} {A B : kVertex V k} (pt : PathTuple D k A B) (i : Fin k) (hi_min : ∀ i' ∈ pt.crowdedPathIndices, i ≤ i') (v : V) (hv : v ∈ pt.crowdedVerticesOnPath i) (j : Fin k) (hj : j ∈ pt.pathIndicesContaining v) (hjne : j ≠ i) : i < j

Key lemma: if i is the smallest crowded path index and v is a crowded vertex on path i, then all other paths containing v have index > i

Canonical Intersection Data Selection

The sign-reversing involution requires selecting intersection data (i, j, v) canonically so that applying the involution twice returns the original path tuple. The algorithm is:

1. i = the smallest path index that contains a crowded point
2. v = the first crowded point on path i (by position in the vertex list)
3. j = the largest path index that contains v

This selection is preserved under the involution because:

• The heads of paths i and j (before v) are unchanged by exchangeTails
• So v is still the first crowded point on path i
• And j is still the largest index containing v

def LGV.PathTuple.minCrowdedPathIndex {V : Type u_3} [DecidableEq V] {D : SimpleDigraph V} {k : ℕ} {A B : kVertex V k} (pt : PathTuple D k A B) (hip : pt.isIntersecting) : Fin k

Get the smallest crowded path index.

Equations

• pt.minCrowdedPathIndex hip = pt.crowdedPathIndices.min' ⋯

theorem LGV.PathTuple.minCrowdedPathIndex_mem {V : Type u_3} [DecidableEq V] {D : SimpleDigraph V} {k : ℕ} {A B : kVertex V k} (pt : PathTuple D k A B) (hip : pt.isIntersecting) : pt.minCrowdedPathIndex hip ∈ pt.crowdedPathIndices

The minimum crowded path index is in crowdedPathIndices

theorem LGV.PathTuple.minCrowdedPathIndex_le {V : Type u_3} [DecidableEq V] {D : SimpleDigraph V} {k : ℕ} {A B : kVertex V k} (pt : PathTuple D k A B) (hip : pt.isIntersecting) (i : Fin k) (hi : i ∈ pt.crowdedPathIndices) : pt.minCrowdedPathIndex hip ≤ i

The minimum crowded path index is minimal

theorem LGV.PathTuple.crowdedVerticesOnPath_minCrowded_nonempty {V : Type u_3} [DecidableEq V] {D : SimpleDigraph V} {k : ℕ} {A B : kVertex V k} (pt : PathTuple D k A B) (hip : pt.isIntersecting) : (pt.crowdedVerticesOnPath (pt.minCrowdedPathIndex hip)).Nonempty

The crowded vertices on the minimum path are nonempty

noncomputable def LGV.PathTuple.firstCrowdedVertex {V : Type u_3} [DecidableEq V] {D : SimpleDigraph V} {k : ℕ} {A B : kVertex V k} (pt : PathTuple D k A B) (hip : pt.isIntersecting) : V

Get the first crowded vertex on the minimum crowded path. This uses List.find? to get the first vertex in the path that is crowded.

Equations

• pt.firstCrowdedVertex hip = (List.find? (fun (v : V) => decide (v ∈ pt.crowdedVerticesOnPath (pt.minCrowdedPathIndex hip))) (pt.paths (pt.minCrowdedPathIndex hip)).vertices).get ⋯

theorem LGV.PathTuple.firstCrowdedVertex_mem_path {V : Type u_3} [DecidableEq V] {D : SimpleDigraph V} {k : ℕ} {A B : kVertex V k} (pt : PathTuple D k A B) (hip : pt.isIntersecting) : pt.firstCrowdedVertex hip ∈ (pt.paths (pt.minCrowdedPathIndex hip)).vertices

The first crowded vertex is in the minimum crowded path

theorem LGV.PathTuple.firstCrowdedVertex_mem_crowded {V : Type u_3} [DecidableEq V] {D : SimpleDigraph V} {k : ℕ} {A B : kVertex V k} (pt : PathTuple D k A B) (hip : pt.isIntersecting) : pt.firstCrowdedVertex hip ∈ pt.crowdedVerticesOnPath (pt.minCrowdedPathIndex hip)

The first crowded vertex is in the crowdedVerticesOnPath set

theorem LGV.PathTuple.firstCrowdedVertex_is_crowded {V : Type u_3} [DecidableEq V] {D : SimpleDigraph V} {k : ℕ} {A B : kVertex V k} (pt : PathTuple D k A B) (hip : pt.isIntersecting) : ∃ (j : Fin k), pt.minCrowdedPathIndex hip ≠ j ∧ pt.firstCrowdedVertex hip ∈ (pt.paths j).vertices

The first crowded vertex is crowded (shared with another path)

noncomputable def LGV.PathTuple.otherPathsContainingFirstCrowded {V : Type u_3} [DecidableEq V] {D : SimpleDigraph V} {k : ℕ} {A B : kVertex V k} (pt : PathTuple D k A B) (hip : pt.isIntersecting) : Finset (Fin k)

The set of path indices containing the first crowded vertex (excluding the minimum)

Equations

• pt.otherPathsContainingFirstCrowded hip = {j ∈ pt.pathIndicesContaining (pt.firstCrowdedVertex hip) | j ≠ pt.minCrowdedPathIndex hip}

theorem LGV.PathTuple.otherPathsContainingFirstCrowded_nonempty {V : Type u_3} [DecidableEq V] {D : SimpleDigraph V} {k : ℕ} {A B : kVertex V k} (pt : PathTuple D k A B) (hip : pt.isIntersecting) : (pt.otherPathsContainingFirstCrowded hip).Nonempty

The set of other paths containing the first crowded vertex is nonempty

noncomputable def LGV.PathTuple.maxOtherPathIndex {V : Type u_3} [DecidableEq V] {D : SimpleDigraph V} {k : ℕ} {A B : kVertex V k} (pt : PathTuple D k A B) (hip : pt.isIntersecting) : Fin k

Get the largest path index containing the first crowded vertex (other than the minimum)

Equations

• pt.maxOtherPathIndex hip = (pt.otherPathsContainingFirstCrowded hip).max' ⋯

theorem LGV.PathTuple.maxOtherPathIndex_ne_min {V : Type u_3} [DecidableEq V] {D : SimpleDigraph V} {k : ℕ} {A B : kVertex V k} (pt : PathTuple D k A B) (hip : pt.isIntersecting) : pt.maxOtherPathIndex hip ≠ pt.minCrowdedPathIndex hip

The max other path index is different from the min crowded path index

theorem LGV.PathTuple.firstCrowdedVertex_mem_maxOtherPath {V : Type u_3} [DecidableEq V] {D : SimpleDigraph V} {k : ℕ} {A B : kVertex V k} (pt : PathTuple D k A B) (hip : pt.isIntersecting) : pt.firstCrowdedVertex hip ∈ (pt.paths (pt.maxOtherPathIndex hip)).vertices

The first crowded vertex is in the max other path

noncomputable def LGV.getIntersectionIndices {V : Type u_3} [DecidableEq V] {D : SimpleDigraph V} {k : ℕ} {A B : kVertex V k} (pt : PathTuple D k A B) (hip : pt.isIntersecting) : { p : Fin k × Fin k // p.1 ≠ p.2 }

Helper function to extract intersection indices from an intersecting path tuple. Returns a pair (i, j) with i ≠ j such that paths i and j intersect.

Equations

• LGV.getIntersectionIndices pt hip = Classical.choice ⋯

noncomputable def LGV.getIntersectionData {V : Type u_3} [DecidableEq V] {D : SimpleDigraph V} {k : ℕ} {A B : kVertex V k} (pt : PathTuple D k A B) (hip : pt.isIntersecting) : { data : (i : Fin k) × (j : Fin k) × { v : V // v ∈ (pt.paths i).vertices ∧ v ∈ (pt.paths j).vertices } // data.fst ≠ data.snd.fst }

Helper function to extract full intersection data from an intersecting path tuple. Returns (i, j, v, hvi, hvj) where i ≠ j and v is on both paths i and j.

Equations

• LGV.getIntersectionData pt hip = Classical.choice ⋯

Canonical (Deterministic) Intersection Data Selection

To prove that signReversing is an involution, we need to select intersection data (i, j, v) deterministically so that the same selection is made before and after applying the involution.

The canonical selection algorithm:

1. i = smallest index in crowdedPathIndices (using Finset.min')
2. v = first crowded vertex on path i (by position in the path)
3. j = largest index in pathIndicesContaining v, excluding i (using Finset.max')

This selection is preserved under exchangeTails because:

• The head of path i (vertices before v) is unchanged
• So v is still the first crowded vertex on path i
• And j is still the largest index containing v

theorem LGV.PathTuple.crowdedPathIndex_pathIndicesContaining_card {V : Type u_3} [DecidableEq V] {D : SimpleDigraph V} {k : ℕ} {A B : kVertex V k} (pt : PathTuple D k A B) (i : Fin k) (hi : i ∈ pt.crowdedPathIndices) (v : V) (hv : v ∈ pt.crowdedVerticesOnPath i) : 1 < (pt.pathIndicesContaining v).card

A crowded path index has at least 2 paths containing some crowded vertex

theorem LGV.PathTuple.pathIndicesContaining_sdiff_singleton_nonempty {V : Type u_3} [DecidableEq V] {D : SimpleDigraph V} {k : ℕ} {A B : kVertex V k} (pt : PathTuple D k A B) (i : Fin k) (hi : i ∈ pt.crowdedPathIndices) (v : V) (hv : v ∈ pt.crowdedVerticesOnPath i) : (pt.pathIndicesContaining v \ {i}).Nonempty

If i is a crowded path index, the set of other path indices containing a crowded vertex on i is nonempty

theorem LGV.PathTuple.crowdedPathIndex_crowdedVerticesOnPath_nonempty {V : Type u_3} [DecidableEq V] {D : SimpleDigraph V} {k : ℕ} {A B : kVertex V k} (pt : PathTuple D k A B) (i : Fin k) (hi : i ∈ pt.crowdedPathIndices) : (pt.crowdedVerticesOnPath i).Nonempty

A crowded path index has nonempty crowdedVerticesOnPath

theorem LGV.PathTuple.firstCrowdedIndexOnPath_lt_length {V : Type u_3} [DecidableEq V] {D : SimpleDigraph V} {k : ℕ} {A B : kVertex V k} (pt : PathTuple D k A B) (i : Fin k) (hi : i ∈ pt.crowdedPathIndices) : pt.firstCrowdedIndexOnPath i < (pt.paths i).vertices.length

The first crowded vertex on path i (when i is a crowded path index) exists in the path

theorem LGV.PathTuple.firstCrowdedVertex_mem_crowdedVerticesOnPath {V : Type u_3} [DecidableEq V] {D : SimpleDigraph V} {k : ℕ} {A B : kVertex V k} (pt : PathTuple D k A B) (i : Fin k) (hi : i ∈ pt.crowdedPathIndices) : let idx := pt.firstCrowdedIndexOnPath i; have h := ⋯; (pt.paths i).vertices.get ⟨idx, h⟩ ∈ pt.crowdedVerticesOnPath i

The vertex at firstCrowdedIndexOnPath is in crowdedVerticesOnPath

noncomputable def LGV.getCanonicalIntersectionData {V : Type u_3} [DecidableEq V] {D : SimpleDigraph V} {k : ℕ} {A B : kVertex V k} (pt : PathTuple D k A B) (hip : pt.isIntersecting) : { data : (i : Fin k) × (j : Fin k) × { v : V // v ∈ (pt.paths i).vertices ∧ v ∈ (pt.paths j).vertices } // data.fst ≠ data.snd.fst }

Canonical intersection data: deterministically selects (i, j, v) for an intersecting path tuple.

• i = smallest crowded path index
• v = first crowded vertex on path i
• j = largest path index containing v (other than i)

Equations

• One or more equations did not get rendered due to their size.

noncomputable def LGV.signReversing {V : Type u_3} [DecidableEq V] {D : SimpleDigraph V} (_hac : D.IsAcyclic) {k : ℕ} {A B : kVertex V k} (sp : pathTupleWithPerm A B) (hip : sp.snd.isIntersecting) : pathTupleWithPerm A B

The sign-reversing involution on intersecting path tuples. For an ipat (σ, 𝐩), we:

1. Find the smallest i such that p_i contains a crowded point
2. Find the first crowded point v on p_i
3. Find the largest j such that v is on p_j
4. Exchange tails of p_i and p_j at v
5. Compose σ with the transposition t_{i,j} This gives (σ ∘ t_{i,j}, 𝐩') which is still an ipat.

Implementation note: The permutation component is sp.1 * Equiv.swap i j where i and j are the intersection indices. The path tuple component uses exchangeTails to swap the tails of paths i and j at the crowded vertex v.

Equations

• One or more equations did not get rendered due to their size.

theorem LGV.signReversing_isIntersecting {V : Type u_3} [DecidableEq V] {D : SimpleDigraph V} (hac : D.IsAcyclic) {k : ℕ} {A B : kVertex V k} (sp : pathTupleWithPerm A B) (hip : sp.snd.isIntersecting) : (signReversing hac sp hip).snd.isIntersecting

The signReversing map preserves the intersecting property. The crowded point v at indices i and j is preserved in the exchanged paths.

theorem LGV.signReversing_canonical_eq {V : Type u_3} [DecidableEq V] {D : SimpleDigraph V} (hac : D.IsAcyclic) {k : ℕ} {A B : kVertex V k} (sp : pathTupleWithPerm A B) (hip : sp.snd.isIntersecting) (i j : Fin k) (hij : i ≠ j) (v : V) (hvi : v ∈ (sp.snd.paths i).vertices) (hvj : v ∈ (sp.snd.paths j).vertices) (h_data : getCanonicalIntersectionData sp.snd hip = ⟨⟨i, ⟨j, ⟨v, ⋯⟩⟩⟩, hij⟩) (hip' : (signReversing hac sp hip).snd.isIntersecting) : ∃ (hvi' : v ∈ ((signReversing hac sp hip).snd.paths i).vertices) (hvj' : v ∈ ((signReversing hac sp hip).snd.paths j).vertices), getCanonicalIntersectionData (signReversing hac sp hip).snd hip' = ⟨⟨i, ⟨j, ⟨v, ⋯⟩⟩⟩, hij⟩

Key invariance lemma: The canonical selection returns the same (i, j, v) for sp' as for sp. This is the heart of the involutive proof.

theorem LGV.signReversing_involutive {V : Type u_3} [DecidableEq V] {D : SimpleDigraph V} (hac : D.IsAcyclic) {k : ℕ} {A B : kVertex V k} (sp : pathTupleWithPerm A B) (hip : sp.snd.isIntersecting) : have sp' := signReversing hac sp hip; ∃ (hip' : sp'.snd.isIntersecting), signReversing hac sp' hip' = sp

theorem LGV.signReversing_perm {V : Type u_3} [DecidableEq V] {D : SimpleDigraph V} (hac : D.IsAcyclic) {k : ℕ} {A B : kVertex V k} (sp : pathTupleWithPerm A B) (hip : sp.snd.isIntersecting) : ∃ (i : Fin k) (j : Fin k), i ≠ j ∧ (signReversing hac sp hip).fst = sp.fst * Equiv.swap i j

The permutation of signReversing is the original permutation composed with a transposition. This captures the essential structural property of the sign-reversing involution: when we exchange tails at indices i and j, we compose σ with the transposition (i j).

theorem LGV.signReversing_paths {V : Type u_3} [DecidableEq V] {D : SimpleDigraph V} (hac : D.IsAcyclic) {k : ℕ} {A B : kVertex V k} (sp : pathTupleWithPerm A B) (hip : sp.snd.isIntersecting) : ∃ (i : Fin k) (j : Fin k), i ≠ j ∧ ∃ (v : V) (hvi : v ∈ (sp.snd.paths i).vertices) (hvj : v ∈ (sp.snd.paths j).vertices), (signReversing hac sp hip).snd.paths i = (exchangeTails (sp.snd.paths i) (sp.snd.paths j) v hvi hvj).1 ∧ (signReversing hac sp hip).snd.paths j = (exchangeTails (sp.snd.paths i) (sp.snd.paths j) v hvi hvj).2 ∧ ∀ (l : Fin k), l ≠ i → l ≠ j → (signReversing hac sp hip).snd.paths l = sp.snd.paths l

The paths of signReversing are obtained by exchanging tails at indices i and j. This captures the essential structural property of the sign-reversing involution for the paths: paths at indices i and j have their tails exchanged at the crowded point v, while all other paths remain unchanged.

theorem LGV.signReversing_sign {V : Type u_3} [DecidableEq V] {D : SimpleDigraph V} (hac : D.IsAcyclic) {k : ℕ} {A B : kVertex V k} (sp : pathTupleWithPerm A B) (hip : sp.snd.isIntersecting) : signOfPathTupleWithPerm (signReversing hac sp hip) = -signOfPathTupleWithPerm sp

The sign-reversing map flips the sign

theorem LGV.signReversing_weight {K : Type u_2} [CommRing K] {V : Type u_3} [DecidableEq V] {D : SimpleDigraph V} (hac : D.IsAcyclic) {k : ℕ} {A B : kVertex V k} (w : ArcWeight D K) (sp : pathTupleWithPerm A B) (hip : sp.snd.isIntersecting) : weightOfPathTupleWithPerm w (signReversing hac sp hip) = weightOfPathTupleWithPerm w sp

The sign-reversing map preserves weight

theorem LGV.signReversing_no_fixed_points {V : Type u_3} [DecidableEq V] {D : SimpleDigraph V} (hac : D.IsAcyclic) {k : ℕ} {A B : kVertex V k} (sp : pathTupleWithPerm A B) (hip : sp.snd.isIntersecting) : signReversing hac sp hip ≠ sp

The sign-reversing map has no fixed points (since it always flips the sign)

Infrastructure for LGV Proof

The following definitions and lemmas provide the infrastructure needed to complete the LGV theorem proof. The key steps are:

1. Define the finset of all path tuples
2. Define the finset of intersecting path tuples (ipats)
3. Prove that the signed sum over ipats is 0 using the sign-reversing involution

def LGV.allPathTupleSet {V : Type u_4} [DecidableEq V] {D : SimpleDigraph V} {k : ℕ} (A B : kVertex V k) : Set (PathTuple D k A B)

The set of all path tuples from A to B

Equations

• LGV.allPathTupleSet A B = Set.univ

noncomputable def LGV.allPathTupleSetFinite {V : Type u_4} [DecidableEq V] {D : SimpleDigraph V} (hpf : D.IsPathFinite) {k : ℕ} (A B : kVertex V k) : (allPathTupleSet A B).Finite

The set of all path tuples is finite (follows from path-finiteness)

Equations

• ⋯ = ⋯

noncomputable def LGV.allPathTupleFinset {V : Type u_4} [DecidableEq V] {D : SimpleDigraph V} (hpf : D.IsPathFinite) {k : ℕ} (A B : kVertex V k) : Finset (PathTuple D k A B)

Convert allPathTupleSet to Finset

Equations

• LGV.allPathTupleFinset hpf A B = ⋯.toFinset

theorem LGV.mem_allPathTupleFinset {V : Type u_4} [DecidableEq V] {D : SimpleDigraph V} (hpf : D.IsPathFinite) {k : ℕ} {A B : kVertex V k} (pt : PathTuple D k A B) : pt ∈ allPathTupleFinset hpf A B

Every path tuple is in allPathTupleFinset

def LGV.ipatSet {V : Type u_4} [DecidableEq V] {D : SimpleDigraph V} {k : ℕ} (A B : kVertex V k) : Set (PathTuple D k A B)

The set of intersecting path tuples (ipats)

Equations

• LGV.ipatSet A B = {pt : LGV.PathTuple D k A B | pt.isIntersecting}

noncomputable def LGV.ipatSetFinite {V : Type u_4} [DecidableEq V] {D : SimpleDigraph V} (hpf : D.IsPathFinite) {k : ℕ} (A B : kVertex V k) : (ipatSet A B).Finite

The set of ipats is finite

Equations

• ⋯ = ⋯

noncomputable def LGV.ipatFinset {V : Type u_4} [DecidableEq V] {D : SimpleDigraph V} (hpf : D.IsPathFinite) {k : ℕ} (A B : kVertex V k) : Finset (PathTuple D k A B)

Convert ipatSet to Finset

Equations

• LGV.ipatFinset hpf A B = ⋯.toFinset

theorem LGV.mem_ipatFinset_iff {V : Type u_4} [DecidableEq V] {D : SimpleDigraph V} (hpf : D.IsPathFinite) {k : ℕ} {A B : kVertex V k} (pt : PathTuple D k A B) : pt ∈ ipatFinset hpf A B ↔ pt.isIntersecting

Membership in ipatFinset

theorem LGV.mem_nipatFinset_iff {V : Type u_4} [DecidableEq V] {D : SimpleDigraph V} (hpf : D.IsPathFinite) {k : ℕ} {A B : kVertex V k} (pt : PathTuple D k A B) : pt ∈ nipatFinset hpf A B ↔ pt.isNonIntersecting

Membership in nipatFinset

theorem LGV.nipatFinset_disjoint_ipatFinset {V : Type u_4} [DecidableEq V] {D : SimpleDigraph V} (hpf : D.IsPathFinite) {k : ℕ} (A B : kVertex V k) : Disjoint (nipatFinset hpf A B) (ipatFinset hpf A B)

nipats and ipats are disjoint

theorem LGV.nipatFinset_union_ipatFinset_eq {V : Type u_4} [DecidableEq V] {D : SimpleDigraph V} (hpf : D.IsPathFinite) {k : ℕ} (A B : kVertex V k) (pt : PathTuple D k A B) : pt ∈ nipatFinset hpf A B ∨ pt ∈ ipatFinset hpf A B ↔ pt ∈ allPathTupleFinset hpf A B

nipats ∪ ipats = all path tuples (set-level equality)

theorem LGV.prod_pathWeightSum_eq_sum_pathTupleWeight {K : Type u_2} [CommRing K] {V : Type u_4} [DecidableEq V] {D : SimpleDigraph V} (hpf : D.IsPathFinite) {k : ℕ} (w : ArcWeight D K) (A B : kVertex V k) : ∏ j : Fin k, pathWeightSum hpf w (A j) (B j) = ∑ pt ∈ allPathTupleFinset hpf A B, pathTupleWeight w pt.paths

The product of path weights equals the sum over path tuples

def LGV.ipatWithPermSet {V : Type u_4} [DecidableEq V] {D : SimpleDigraph V} {k : ℕ} (A B : kVertex V k) : Set (pathTupleWithPerm A B)

The set of all intersecting path tuples with permutation. This is the domain of the sign-reversing involution.

Equations

• LGV.ipatWithPermSet A B = {sp : LGV.pathTupleWithPerm A B | sp.snd.isIntersecting}

instance LGV.pathTupleFinite {V : Type u_4} [DecidableEq V] {D : SimpleDigraph V} (hpf : D.IsPathFinite) {k : ℕ} (A B : kVertex V k) : Finite (PathTuple D k A B)

PathTuple is finite when the digraph is path-finite.

instance LGV.pathTupleWithPermFinite {V : Type u_4} [DecidableEq V] {D : SimpleDigraph V} (hpf : D.IsPathFinite) {k : ℕ} (A B : kVertex V k) : Finite (pathTupleWithPerm A B)

pathTupleWithPerm is finite when the digraph is path-finite.

noncomputable def LGV.ipatWithPermSetFinite {V : Type u_4} [DecidableEq V] {D : SimpleDigraph V} (hpf : D.IsPathFinite) {k : ℕ} (A B : kVertex V k) : (ipatWithPermSet A B).Finite

The set of intersecting path tuples with permutation is finite.

Equations

• ⋯ = ⋯

noncomputable def LGV.ipatWithPermFinset {V : Type u_4} [DecidableEq V] {D : SimpleDigraph V} (hpf : D.IsPathFinite) {k : ℕ} (A B : kVertex V k) : Finset (pathTupleWithPerm A B)

Convert ipatWithPermSet to Finset

Equations

• LGV.ipatWithPermFinset hpf A B = ⋯.toFinset

theorem LGV.mem_ipatWithPermFinset_iff {V : Type u_4} [DecidableEq V] {D : SimpleDigraph V} (hpf : D.IsPathFinite) {k : ℕ} {A B : kVertex V k} (sp : pathTupleWithPerm A B) : sp ∈ ipatWithPermFinset hpf A B ↔ sp.snd.isIntersecting

Membership in ipatWithPermFinset

theorem LGV.sum_ipatWithPerm_signed_weight_eq_zero {K : Type u_2} [CommRing K] {V : Type u_4} [DecidableEq V] {D : SimpleDigraph V} (hpf : D.IsPathFinite) (hac : D.IsAcyclic) {k : ℕ} (w : ArcWeight D K) (A B : kVertex V k) : ∑ sp ∈ ipatWithPermFinset hpf A B, ↑↑(Equiv.Perm.sign sp.fst) * pathTupleWeight w sp.snd.paths = 0

The signed sum over ALL intersecting path tuples (with permutation) is zero.

This is the correct formulation of the cancellation lemma. The sign-reversing involution signReversing maps (σ, pt) to (σ * swap i j, pt'), where:

• sign(σ * swap i j) = -sign(σ) (sign flips)
• weight(pt') = weight(pt) (weight preserved)

So each pair {sp, signReversing(sp)} contributes: sign(σ) * w(pt) + sign(σ * swap i j) * w(pt') = sign(σ) * w(pt) + (-sign(σ)) * w(pt) = 0

The total sum is therefore 0.

Note: This works in any CommRing K, including characteristic 2, because we're summing pairs that each contribute 0, not just showing 2x = 0.

def LGV.allPathTupleWithPermSet {V : Type u_4} [DecidableEq V] {D : SimpleDigraph V} {k : ℕ} (A B : kVertex V k) : Set (pathTupleWithPerm A B)

The set of all path tuples with permutation

Equations

• LGV.allPathTupleWithPermSet A B = Set.univ

noncomputable def LGV.allPathTupleWithPermSetFinite {V : Type u_4} [DecidableEq V] {D : SimpleDigraph V} (hpf : D.IsPathFinite) {k : ℕ} (A B : kVertex V k) : (allPathTupleWithPermSet A B).Finite

The set of all path tuples with permutation is finite

Equations

• ⋯ = ⋯

noncomputable def LGV.allPathTupleWithPermFinset {V : Type u_4} [DecidableEq V] {D : SimpleDigraph V} (hpf : D.IsPathFinite) {k : ℕ} (A B : kVertex V k) : Finset (pathTupleWithPerm A B)

Convert allPathTupleWithPermSet to Finset

Equations

• LGV.allPathTupleWithPermFinset hpf A B = ⋯.toFinset

theorem LGV.mem_allPathTupleWithPermFinset {V : Type u_4} [DecidableEq V] {D : SimpleDigraph V} (hpf : D.IsPathFinite) {k : ℕ} {A B : kVertex V k} (sp : pathTupleWithPerm A B) : sp ∈ allPathTupleWithPermFinset hpf A B

Every path tuple with permutation is in allPathTupleWithPermFinset

def LGV.nipatWithPermSet {V : Type u_4} [DecidableEq V] {D : SimpleDigraph V} {k : ℕ} (A B : kVertex V k) : Set (pathTupleWithPerm A B)

The set of non-intersecting path tuples with permutation

Equations

• LGV.nipatWithPermSet A B = {sp : LGV.pathTupleWithPerm A B | sp.snd.isNonIntersecting}

noncomputable def LGV.nipatWithPermSetFinite {V : Type u_4} [DecidableEq V] {D : SimpleDigraph V} (hpf : D.IsPathFinite) {k : ℕ} (A B : kVertex V k) : (nipatWithPermSet A B).Finite

The set of non-intersecting path tuples with permutation is finite

Equations

• ⋯ = ⋯

noncomputable def LGV.nipatWithPermFinset {V : Type u_4} [DecidableEq V] {D : SimpleDigraph V} (hpf : D.IsPathFinite) {k : ℕ} (A B : kVertex V k) : Finset (pathTupleWithPerm A B)

Convert nipatWithPermSet to Finset

Equations

• LGV.nipatWithPermFinset hpf A B = ⋯.toFinset

theorem LGV.mem_nipatWithPermFinset_iff {V : Type u_4} [DecidableEq V] {D : SimpleDigraph V} (hpf : D.IsPathFinite) {k : ℕ} {A B : kVertex V k} (sp : pathTupleWithPerm A B) : sp ∈ nipatWithPermFinset hpf A B ↔ sp.snd.isNonIntersecting

Membership in nipatWithPermFinset

theorem LGV.nipatWithPermFinset_disjoint_ipatWithPermFinset {V : Type u_4} [DecidableEq V] {D : SimpleDigraph V} (hpf : D.IsPathFinite) {k : ℕ} (A B : kVertex V k) : Disjoint (nipatWithPermFinset hpf A B) (ipatWithPermFinset hpf A B)

nipats and ipats with permutation are disjoint

theorem LGV.nipatWithPermFinset_union_ipatWithPermFinset_sum {K : Type u_2} [CommRing K] {V : Type u_4} [DecidableEq V] {D : SimpleDigraph V} (hpf : D.IsPathFinite) {k : ℕ} (A B : kVertex V k) (f : pathTupleWithPerm A B → K) : ∑ sp ∈ nipatWithPermFinset hpf A B, f sp + ∑ sp ∈ ipatWithPermFinset hpf A B, f sp = ∑ sp ∈ allPathTupleWithPermFinset hpf A B, f sp

nipats ∪ ipats with permutation = all path tuples with permutation (as a sum equality)

theorem LGV.sum_allPathTupleWithPerm_eq_sum_nipat_add_sum_ipat {K : Type u_2} [CommRing K] {V : Type u_4} [DecidableEq V] {D : SimpleDigraph V} (hpf : D.IsPathFinite) {k : ℕ} (w : ArcWeight D K) (A B : kVertex V k) : ∑ sp ∈ allPathTupleWithPermFinset hpf A B, ↑↑(Equiv.Perm.sign sp.fst) * pathTupleWeight w sp.snd.paths = ∑ sp ∈ nipatWithPermFinset hpf A B, ↑↑(Equiv.Perm.sign sp.fst) * pathTupleWeight w sp.snd.paths + ∑ sp ∈ ipatWithPermFinset hpf A B, ↑↑(Equiv.Perm.sign sp.fst) * pathTupleWeight w sp.snd.paths

The sum over all path tuples with permutation splits into nipats and ipats

theorem LGV.sum_nipatWithPerm_eq_sum_nipatWeightSum {K : Type u_2} [CommRing K] {V : Type u_4} [DecidableEq V] {D : SimpleDigraph V} (hpf : D.IsPathFinite) {k : ℕ} (w : ArcWeight D K) (A B : kVertex V k) : ∑ sp ∈ nipatWithPermFinset hpf A B, ↑↑(Equiv.Perm.sign sp.fst) * pathTupleWeight w sp.snd.paths = ∑ σ : Equiv.Perm (Fin k), Equiv.Perm.sign σ • nipatWeightSum hpf w A (permuteKVertex σ B) σ

The sum over nipats with permutation equals the sum over permutations of nipatWeightSum

theorem LGV.det_eq_sum_allPathTupleWithPerm {K : Type u_2} [CommRing K] {V : Type u_4} [DecidableEq V] {D : SimpleDigraph V} (hpf : D.IsPathFinite) {k : ℕ} (w : ArcWeight D K) (A B : kVertex V k) : (pathWeightMatrix hpf w A B).det = ∑ sp ∈ allPathTupleWithPermFinset hpf A B, ↑↑(Equiv.Perm.sign sp.fst) * pathTupleWeight w sp.snd.paths

The determinant can be written as a sum over all path tuples with permutation

theorem LGV.lgv_weighted_digraph {K : Type u_2} [CommRing K] {V : Type u_4} [DecidableEq V] {D : SimpleDigraph V} (hpf : D.IsPathFinite) (hac : D.IsAcyclic) {k : ℕ} (w : ArcWeight D K) (A B : kVertex V k) : (pathWeightMatrix hpf w A B).det = ∑ σ : Equiv.Perm (Fin k), Equiv.Perm.sign σ • nipatWeightSum hpf w A (permuteKVertex σ B) σ

LGV lemma, digraph weight version (Theorem thm.lgv.kpaths.wt-dg) Label: thm.lgv.kpaths.wt-dg

For any path-finite acyclic digraph D with arc weights w ∈ K: det((∑{p : Aᵢ → Bⱼ} w(p)){i,j}) = ∑{σ ∈ Sₖ} (-1)^σ ∑{𝐩 nipat from 𝐀 to σ(𝐁)} w(𝐩)

This generalizes the lattice version - we only use that D is path-finite and acyclic.

Proof outline:

1. By Leibniz formula: det(M) = ∑_σ (-1)^σ ∏i M{i,σ(i)}
2. Each M_{i,σ(i)} = ∑{p : A_i → B{σ(i)}} w(p), so the product expands to ∑_{𝐩 : path tuple from 𝐀 to σ(𝐁)} w(𝐩)
3. Thus det(M) = ∑σ (-1)^σ ∑{𝐩 : 𝐀 → σ(𝐁)} w(𝐩)
4. Split the inner sum into nipats and ipats
5. The sign-reversing involution on ipats shows ∑_{ipats} (-1)^σ w(𝐩) = 0
6. Only nipats remain: det(M) = ∑σ (-1)^σ ∑{𝐩 nipat from 𝐀 to σ(𝐁)} w(𝐩)

theorem LGV.lgv_weighted_lattice {K : Type u_2} [CommRing K] {k : ℕ} (w : ArcWeight integerLattice K) (A B : kVertex (ℤ × ℤ) k) : (pathWeightMatrix integerLattice_pathFinite w A B).det = ∑ σ : Equiv.Perm (Fin k), Equiv.Perm.sign σ • nipatWeightSum integerLattice_pathFinite w A (permuteKVertex σ B) σ

LGV lemma, lattice weight version (Theorem thm.lgv.kpaths.wt) Label: thm.lgv.kpaths.wt

For the integer lattice ℤ² with arc weights w ∈ K: det((∑{p : Aᵢ → Bⱼ} w(p)){i,j}) = ∑{σ ∈ Sₖ} (-1)^σ ∑{𝐩 nipat from 𝐀 to σ(𝐁)} w(𝐩)

The proof uses a sign-reversing involution on intersecting path tuples: when two paths intersect, exchange their tails at the first intersection point. This changes the sign (via the permutation) but preserves the weight.

This is a special case of lgv_weighted_digraph for the integer lattice.

The Nonpermutable Case

Corollary cor.lgv.kpaths.wt-np: When the source and target vertices are "sorted" (x-coordinates decreasing, y-coordinates increasing), only the identity permutation contributes to the sum.

def LGV.xCoord : ℤ × ℤ → ℤ

The x-coordinate of a lattice point

Equations

• LGV.xCoord = Prod.fst

def LGV.yCoord : ℤ × ℤ → ℤ

The y-coordinate of a lattice point

Equations

• LGV.yCoord = Prod.snd

def LGV.xDecreasing {k : ℕ} (A : kVertex (ℤ × ℤ) k) : Prop

A k-vertex has weakly decreasing x-coordinates

Equations

• LGV.xDecreasing A = ∀ (i j : Fin k), i ≤ j → LGV.xCoord (A j) ≤ LGV.xCoord (A i)

def LGV.yIncreasing {k : ℕ} (A : kVertex (ℤ × ℤ) k) : Prop

A k-vertex has weakly increasing y-coordinates

Equations

• LGV.yIncreasing A = ∀ (i j : Fin k), i ≤ j → LGV.yCoord (A i) ≤ LGV.yCoord (A j)

theorem LGV.discrete_ivt_aux (n : ℕ) (a b : ℤ) (f : ℤ → ℤ) : a ≤ b → (b - a).toNat = n → (∀ (m : ℤ), a ≤ m → m < b → |f (m + 1) - f m| ≤ 1) → 0 ≤ f a → f b ≤ 0 → ∃ (c : ℤ), a ≤ c ∧ c ≤ b ∧ f c = 0

Discrete intermediate value theorem for integers (auxiliary version with explicit n)

theorem LGV.discrete_ivt {a b : ℤ} (hab : a ≤ b) (f : ℤ → ℤ) (hf : ∀ (n : ℤ), a ≤ n → n < b → |f (n + 1) - f n| ≤ 1) (hfa : 0 ≤ f a) (hfb : f b ≤ 0) : ∃ (c : ℤ), a ≤ c ∧ c ≤ b ∧ f c = 0

Discrete intermediate value theorem for integers. If f : ℤ → ℤ satisfies |f(n+1) - f(n)| ≤ 1 for all n in [a, b), and f(a) ≥ 0 and f(b) ≤ 0, then there exists c in [a, b] with f(c) = 0.

theorem LGV.baby_jordan {A A' B B' : ℤ × ℤ} (hxA : xCoord A' ≤ xCoord A) (hyA : yCoord A ≤ yCoord A') (hxB : xCoord B' ≤ xCoord B) (hyB : yCoord B ≤ yCoord B') (p : integerLattice.Path) (hp_start : p.start = A) (hp_finish : p.finish = B') (p' : integerLattice.Path) (hp'_start : p'.start = A') (hp'_finish : p'.finish = B) : pathsIntersect p p'

Baby Jordan curve theorem (Proposition prop.lgv.jordan-2) Label: prop.lgv.jordan-2

If A' is weakly northwest of A, and B' is weakly northwest of B, then any path from A to B' and any path from A' to B must intersect.

This is used to show that non-identity permutations have no nipats.

Proof sketch: Both paths visit vertices with consecutive sum values (x + y). The sum ranges [A.1+A.2, B'.1+B'.2] for p and [A'.1+A'.2, B.1+B.2] for p' overlap. At each sum s in the overlap, path p has x-coordinate x_p(s) and p' has x_p'(s). At s_lo = max(A.1+A.2, A'.1+A'.2): x_p ≥ x_p' (because A.1 ≥ A'.1 and A.2 ≤ A'.2). At s_hi = min(B'.1+B'.2, B.1+B.2): x_p ≤ x_p' (because B'.1 ≤ B.1 and B'.2 ≥ B.2). By discrete IVT, there exists s where x_p(s) = x_p'(s), so the vertices coincide.

theorem LGV.monotone_perm_eq_id {k : ℕ} (σ : Equiv.Perm (Fin k)) (h : ∀ (i j : Fin k), i < j → σ i ≤ σ j) : σ = Equiv.refl (Fin k)

A monotone bijection on Fin k is the identity. This is used to show that if σ ≠ id, then σ is not monotone.

theorem LGV.no_nipats_nonidentity {k : ℕ} (A B : kVertex (ℤ × ℤ) k) (hxA : xDecreasing A) (hyA : yIncreasing A) (hxB : xDecreasing B) (hyB : yIncreasing B) (σ : Equiv.Perm (Fin k)) (hσ : σ ≠ Equiv.refl (Fin k)) : nipatSet A (permuteKVertex σ B) = ∅

When σ ≠ id, there are no nipats from 𝐀 to σ(𝐁) under the sorting conditions

theorem LGV.nipatWeightSum_of_empty {K : Type u_2} [CommRing K] {k : ℕ} (w : ArcWeight integerLattice K) (A B : kVertex (ℤ × ℤ) k) (σ : Equiv.Perm (Fin k)) (h : nipatSet A B = ∅) : nipatWeightSum integerLattice_pathFinite w A B σ = 0

When the nipatSet is empty, the nipatWeightSum is zero

theorem LGV.permuteKVertex_refl {V : Type u_4} {k : ℕ} (B : kVertex V k) : permuteKVertex (Equiv.refl (Fin k)) B = B

Permuting a k-vertex by the identity permutation gives the same k-vertex

theorem LGV.lgv_nonpermutable {K : Type u_2} [CommRing K] {k : ℕ} (w : ArcWeight integerLattice K) (A B : kVertex (ℤ × ℤ) k) (hxA : xDecreasing A) (hyA : yIncreasing A) (hxB : xDecreasing B) (hyB : yIncreasing B) : (pathWeightMatrix integerLattice_pathFinite w A B).det = nipatWeightSum integerLattice_pathFinite w A B (Equiv.refl (Fin k))

LGV lemma, nonpermutable lattice weight version (Corollary cor.lgv.kpaths.wt-np) Label: cor.lgv.kpaths.wt-np

Under the sorting conditions:

• x(A₁) ≥ x(A₂) ≥ ⋯ ≥ x(Aₖ)
• y(A₁) ≤ y(A₂) ≤ ⋯ ≤ y(Aₖ)
• x(B₁) ≥ x(B₂) ≥ ⋯ ≥ x(Bₖ)
• y(B₁) ≤ y(B₂) ≤ ⋯ ≤ y(Bₖ)

The LGV formula simplifies to: det((∑{p : Aᵢ → Bⱼ} w(p)){i,j}) = ∑_{𝐩 nipat from 𝐀 to 𝐁} w(𝐩)

Applications

Binomial Coefficient Determinants (Corollary cor.lgv.binom-det-nonneg)

When the matrix entries are binomial coefficients, the determinant is nonnegative.

The FKG Inequality for Binomial Coefficients

The key combinatorial inequality underlying the binomial determinant nonnegativity. This is the 2×2 case of the LGV lemma, which can be proved directly by induction.

theorem LGV.binom_2x2_ineq (a b c d : ℕ) (hab : b ≤ a) (hcd : d ≤ c) : ↑(a.choose d) * ↑(b.choose c) ≤ ↑(a.choose c) * ↑(b.choose d)

The FKG inequality for binomial coefficients: C(a,c) * C(b,d) ≥ C(a,d) * C(b,c) when a ≥ b and c ≥ d.

This handles all cases including when some choose values are zero.

Base cases for binomial determinant nonnegativity

Lattice point setup for binomial determinants

The key construction: set Aᵢ = (0, -aᵢ) and Bᵢ = (bᵢ, -bᵢ). These satisfy the sorting conditions for lgv_nonpermutable.

def LGV.binomLatticeA {k : ℕ} (a : Fin k → ℕ) : kVertex (ℤ × ℤ) k

The source lattice points for the binomial coefficient determinant: A_i = (0, -a_i) for the LGV lemma application.

Equations

• LGV.binomLatticeA a i = (0, -↑(a i))

def LGV.binomLatticeB {k : ℕ} (b : Fin k → ℕ) : kVertex (ℤ × ℤ) k

The target lattice points for the binomial coefficient determinant: B_i = (b_i, -b_i) for the LGV lemma application.

Equations

• LGV.binomLatticeB b i = (↑(b i), -↑(b i))

theorem LGV.binomLatticeA_xDecreasing {k : ℕ} (a : Fin k → ℕ) : xDecreasing (binomLatticeA a)

The source lattice points have constant x-coordinate 0, so xDecreasing holds trivially.

theorem LGV.binomLatticeA_yIncreasing {k : ℕ} (a : Fin k → ℕ) (ha : ∀ (i j : Fin k), i ≤ j → a j ≤ a i) : yIncreasing (binomLatticeA a)

The source lattice points satisfy yIncreasing when a is weakly decreasing. If a_i ≥ a_j for i ≤ j, then -a_i ≤ -a_j.

theorem LGV.binomLatticeB_xDecreasing {k : ℕ} (b : Fin k → ℕ) (hb : ∀ (i j : Fin k), i ≤ j → b j ≤ b i) : xDecreasing (binomLatticeB b)

The target lattice points satisfy xDecreasing when b is weakly decreasing. If b_i ≥ b_j for i ≤ j, then x-coordinate b_i ≥ b_j.

theorem LGV.binomLatticeB_yIncreasing {k : ℕ} (b : Fin k → ℕ) (hb : ∀ (i j : Fin k), i ≤ j → b j ≤ b i) : yIncreasing (binomLatticeB b)

The target lattice points satisfy yIncreasing when b is weakly decreasing. If b_i ≥ b_j for i ≤ j, then -b_i ≤ -b_j.

Helper definitions for the path-subset bijection

The bijection between paths from (0, -a) to (b, -b) and b-element subsets of Fin a is constructed using the following helpers:

• eastStepCount a S i: count of elements j ∈ S with j < i
• vertexAtPos a S i: the vertex at position i in the path determined by S
• pathVerticesList a S: the list of vertices for the path determined by S

noncomputable def LGV.paths_equiv_powersetCard (a b : ℕ) : ↥(pathsFromTo integerLattice integerLattice_pathFinite (0, -↑a) (↑b, -↑b)) ≃ ↥(Finset.powersetCard b Finset.univ)

Bijection between paths from (0, -a) to (b, -b) and b-element subsets of Fin a.

This encapsulates the key combinatorial bijection from Proposition prop.lgv.1-paths.ct:

• A path from (0, -a) to (b, -b) has exactly a steps (coordinate sum goes from -a to 0)
• A path has exactly b east-steps (x-coordinate goes from 0 to b)
• A path is uniquely determined by which of its a steps are east-steps
• This gives a bijection to b-element subsets of Fin a

Equations

• One or more equations did not get rendered due to their size.

theorem LGV.paths_count_eq_choose (a b : ℕ) : (pathsFromTo integerLattice integerLattice_pathFinite (0, -↑a) (↑b, -↑b)).card = a.choose b

The number of paths from (0, -a) to (b, -b) in the integer lattice equals C(a, b). This follows from Proposition prop.lgv.1-paths.ct.

Unit weight infrastructure for binomial determinant proof

The unit weight function assigns weight 1 to every arc. With this weight:

• pathWeight p = 1 for any path p
• pathTupleWeight ps = 1 for any path tuple ps
• pathWeightSum = cardinality of paths
• nipatWeightSum = cardinality of nipats ≥ 0

noncomputable def LGV.unitArcWeight : ArcWeight integerLattice ℤ

The unit arc weight function assigns 1 to every arc

Equations

• LGV.unitArcWeight x✝² x✝¹ x✝ = 1

theorem LGV.pathWeight_unitArcWeight (p : integerLattice.Path) : pathWeight unitArcWeight p = 1

With unit weight, pathWeight is always 1

theorem LGV.pathTupleWeight_unitArcWeight {k : ℕ} (ps : Fin k → integerLattice.Path) : pathTupleWeight unitArcWeight ps = 1

With unit weight, pathTupleWeight is always 1

theorem LGV.pathWeightSum_unitArcWeight (u v : ℤ × ℤ) : pathWeightSum integerLattice_pathFinite unitArcWeight u v = ↑(pathsFromTo integerLattice integerLattice_pathFinite u v).card

With unit weight, pathWeightSum equals cardinality of paths

theorem LGV.binom_matrix_eq_pathWeightMatrix {k : ℕ} (a b : Fin k → ℕ) : (Matrix.of fun (i j : Fin k) => ↑((a i).choose (b j))) = pathWeightMatrix integerLattice_pathFinite unitArcWeight (binomLatticeA a) (binomLatticeB b)

The binomial matrix equals pathWeightMatrix with unit weight

theorem LGV.nipatWeightSum_unitArcWeight {k : ℕ} (A B : kVertex (ℤ × ℤ) k) (σ : Equiv.Perm (Fin k)) : nipatWeightSum integerLattice_pathFinite unitArcWeight A B σ = ↑(nipatFinset integerLattice_pathFinite A B).card

With unit weight, nipatWeightSum equals cardinality of nipats

theorem LGV.nipatWeightSum_unitArcWeight_nonneg {k : ℕ} (A B : kVertex (ℤ × ℤ) k) (σ : Equiv.Perm (Fin k)) : 0 ≤ nipatWeightSum integerLattice_pathFinite unitArcWeight A B σ

nipatWeightSum with unit weight is nonnegative

theorem LGV.ipatWithPermFinset_eq_sigma {k : ℕ} (A B : kVertex (ℤ × ℤ) k) : ipatWithPermFinset integerLattice_pathFinite A B = Finset.univ.sigma fun (σ : Equiv.Perm (Fin k)) => ipatFinset integerLattice_pathFinite A (permuteKVertex σ B)

The ipatWithPermFinset can be decomposed as a sigma type over permutations. This is the ipat analogue of the decomposition used for nipats.

theorem LGV.sum_ipatWithPerm_eq_sum_ipatFinset_card {k : ℕ} (A B : kVertex (ℤ × ℤ) k) : ∑ sp ∈ ipatWithPermFinset integerLattice_pathFinite A B, ↑(Equiv.Perm.sign sp.fst) * pathTupleWeight unitArcWeight sp.snd.paths = ∑ σ : Equiv.Perm (Fin k), ↑(Equiv.Perm.sign σ) * ↑(ipatFinset integerLattice_pathFinite A (permuteKVertex σ B)).card

The sum over ipatWithPermFinset equals the sum over permutations of ipat counts. With unit weight, pathTupleWeight = 1, so this becomes a signed count.

theorem LGV.sum_signed_ipatFinset_card_eq_zero {k : ℕ} (A B : kVertex (ℤ × ℤ) k) : ∑ σ : Equiv.Perm (Fin k), ↑(Equiv.Perm.sign σ) * ↑(ipatFinset integerLattice_pathFinite A (permuteKVertex σ B)).card = 0

The signed sum of ipat counts over all permutations is zero. This is the counting version of sum_ipatWithPerm_signed_weight_eq_zero.

The proof uses the sign-reversing involution on intersecting path tuples: for each ipat (σ, pt), swap tails at the first intersection point to get (σ * swap i j, pt'), which has opposite sign but the same weight (= 1).

This lemma is the key step needed to complete LGV1.lean's lgv_involution_cancellation.

theorem LGV.binom_det_nonneg {k : ℕ} (a b : Fin k → ℕ) (ha : ∀ (i j : Fin k), i ≤ j → a j ≤ a i) (hb : ∀ (i j : Fin k), i ≤ j → b j ≤ b i) : 0 ≤ (Matrix.of fun (i j : Fin k) => ↑((a i).choose (b j))).det

Catalan Hankel Determinant (Corollary cor.lgv.catalan-hankel-det-0)

The Hankel determinant of Catalan numbers equals 1.

We use Mathlib's catalan function from Mathlib.Combinatorics.Enumerative.Catalan. The Catalan numbers are defined by cₙ = C(2n,n)/(n+1), and the Hankel matrix has entry (i,j) equal to c_{i+j}. This is a famous result that can be proven using the LGV lemma with Dyck paths.

def LGV.catalanHankelMatrix (k : ℕ) : Matrix (Fin k) (Fin k) ℤ

The Catalan Hankel matrix of size k×k, where entry (i,j) is c_{i+j}. Uses Mathlib's catalan function directly.

Equations

• LGV.catalanHankelMatrix k = Matrix.of fun (i j : Fin k) => ↑(catalan (↑i + ↑j))

theorem LGV.catalanHankelMatrix_symm (k : ℕ) (i j : Fin k) : catalanHankelMatrix k i j = catalanHankelMatrix k j i

The Catalan Hankel matrix is symmetric (since c_{i+j} = c_{j+i}).

theorem LGV.catalanHankelMatrix_zero_zero (k : ℕ) (hk : 0 < k) : catalanHankelMatrix k ⟨0, hk⟩ ⟨0, hk⟩ = 1

The (0,0) entry of the Catalan Hankel matrix is 1 (= c₀).

@[simp]

theorem LGV.catalanHankelMatrix_apply (k : ℕ) (i j : Fin k) : catalanHankelMatrix k i j = ↑(catalan (↑i + ↑j))

Entry (i,j) of the Catalan Hankel matrix is catalan(i+j).

theorem LGV.catalan_hankel_det_zero : (catalanHankelMatrix 0).det = 1

Catalan Hankel determinant for k=0: empty matrix has determinant 1.

theorem LGV.catalan_hankel_det_one : (catalanHankelMatrix 1).det = 1

Catalan Hankel determinant for k=1: 1×1 matrix [c₀] = [1], det = 1.

theorem LGV.catalan_hankel_det_two : (catalanHankelMatrix 2).det = 1

Catalan Hankel determinant for k=2: 2×2 matrix [[c₀, c₁], [c₁, c₂]] = [[1, 1], [1, 2]]. det = 1·2 - 1·1 = 1.

theorem LGV.catalan_hankel_det_three : (catalanHankelMatrix 3).det = 1

Catalan Hankel determinant for k=3.

theorem LGV.catalan_hankel_det_four : (catalanHankelMatrix 4).det = 1

Catalan Hankel determinant for k=4.

theorem LGV.catalan_hankel_det_five : (catalanHankelMatrix 5).det = 1

Catalan Hankel determinant for k=5.

theorem LGV.catalan_hankel_det_six : (catalanHankelMatrix 6).det = 1

Catalan Hankel determinant for k=6.

theorem LGV.catalan_hankel_det_seven : (catalanHankelMatrix 7).det = 1

Catalan Hankel determinant for k=7.

def LGV.dyckDigraph : SimpleDigraph (ℤ × ℕ)

The Dyck path digraph: vertices are ℤ × ℕ, arcs go (i,j) → (i+1, j+1) and (i,j) → (i+1, j-1). Used for counting Catalan numbers via Dyck paths.

A Dyck path from (0,0) to (2n,0) corresponds to a balanced sequence of n up-steps and n down-steps that never goes below the x-axis. A Dyck path is a lattice path that stays on or above the x-axis, where each step goes either up-right or down-right.

Equations

• LGV.dyckDigraph = { arc := fun (u v : ℤ × ℕ) => v.1 = u.1 + 1 ∧ v.2 = u.2 + 1 ∨ v.1 = u.1 + 1 ∧ v.2 + 1 = u.2 ∧ 0 < u.2, arc_irrefl := LGV.dyckDigraph._proof_1 }

theorem LGV.dyckDigraph_arc_fst (u v : ℤ × ℕ) (h : dyckDigraph.arc u v) : v.1 = u.1 + 1

Every arc in the Dyck digraph increases the first coordinate by 1

theorem LGV.dyckDigraph_path_vertex_fst (p : dyckDigraph.Path) (i : ℕ) (hi : i < p.vertices.length) : (p.vertices.get ⟨i, hi⟩).1 = p.start.1 + ↑i

Along a path in the Dyck digraph, the first coordinate increases by the index

theorem LGV.dyckDigraph_path_length_eq (p : dyckDigraph.Path) : ↑p.vertices.length = p.finish.1 - p.start.1 + 1

Path length is determined by start and finish x-coordinates in the Dyck digraph

theorem LGV.dyckDigraph_path_snd_bounded (p : dyckDigraph.Path) (i : ℕ) (hi : i < p.vertices.length) : (p.vertices.get ⟨i, hi⟩).2 ≤ p.start.2 + i

The second coordinate stays bounded along a path in the Dyck digraph

theorem LGV.dyckDigraph_pathFinite : dyckDigraph.IsPathFinite

The Dyck digraph is path-finite.

Proof: We show that paths from u to v are finite by:

1. If v.1 < u.1, no paths exist (x-coordinate strictly increases along arcs)
2. Otherwise, paths have fixed length n = v.1 - u.1 + 1
3. The y-coordinate is bounded: 0 ≤ y ≤ u.2 + n at each vertex
4. Each path is determined by its vertex sequence, which is a function Fin n → box
5. Since box is finite and n is finite, there are finitely many such functions
6. The map from paths to vertex sequences is injective, so paths are finite

theorem LGV.dyckDigraph_acyclic : dyckDigraph.IsAcyclic

The Dyck digraph is acyclic

Unit Arc Weight for Dyck Digraph

Infrastructure for connecting the Catalan Hankel matrix to the LGV lemma.

noncomputable def LGV.dyckUnitArcWeight : ArcWeight dyckDigraph ℤ

Unit arc weight for the Dyck digraph

Equations

• LGV.dyckUnitArcWeight x✝² x✝¹ x✝ = 1

theorem LGV.pathWeight_dyckUnitArcWeight (p : dyckDigraph.Path) : pathWeight dyckUnitArcWeight p = 1

Path weight with unit weight is 1

theorem LGV.pathTupleWeight_dyckUnitArcWeight {k : ℕ} (ps : Fin k → dyckDigraph.Path) : pathTupleWeight dyckUnitArcWeight ps = 1

Path tuple weight with unit weight is 1

theorem LGV.pathWeightSum_dyckUnitArcWeight (u v : ℤ × ℕ) : pathWeightSum dyckDigraph_pathFinite dyckUnitArcWeight u v = ↑(pathsFromTo dyckDigraph dyckDigraph_pathFinite u v).card

With unit weight, pathWeightSum equals cardinality of paths

theorem LGV.nipatWeightSum_dyckUnitArcWeight {k : ℕ} (A B : kVertex (ℤ × ℕ) k) (σ : Equiv.Perm (Fin k)) : nipatWeightSum dyckDigraph_pathFinite dyckUnitArcWeight A B σ = ↑(nipatFinset dyckDigraph_pathFinite A B).card

With unit weight, nipatWeightSum equals cardinality of nipats

def LGV.dyckPathToSteps (p : dyckDigraph.Path) : List DyckStep

Convert a Dyck path to a list of DyckSteps. Each arc (x,y) → (x+1,y+1) becomes U, each arc (x,y) → (x+1,y-1) becomes D.

Equations

• One or more equations did not get rendered due to their size.

theorem LGV.dyckPathToSteps_length (p : dyckDigraph.Path) : (dyckPathToSteps p).length = p.vertices.length - 1

The step list has length = vertices.length - 1 = number of arcs.

def LGV.dyckPathToWord (p : dyckDigraph.Path) (hstart : p.start = (0, 0)) (hfinish : p.finish.2 = 0) : DyckWord

Convert a Dyck path to a DyckWord. Each arc (x,y) → (x+1,y+1) becomes U, each arc (x,y) → (x+1,y-1) becomes D.

Note: This definition requires substantial infrastructure to prove well-formedness. The key properties are:

• count_U_eq_count_D: follows from start.2 = 0 = finish.2
• count_D_le_count_U: follows from y ≥ 0 throughout the path (Dyck condition)

Equations

• LGV.dyckPathToWord p hstart hfinish = { toList := LGV.dyckPathToSteps p, count_U_eq_count_D := ⋯, count_D_le_count_U := ⋯ }

theorem LGV.dyckPathToWord_semilength (p : dyckDigraph.Path) (hstart : p.start = (0, 0)) (hfinish : p.finish.2 = 0) : (dyckPathToWord p hstart hfinish).semilength = List.count DyckStep.U (dyckPathToSteps p)

The semilength of dyckPathToWord equals the count of U steps.

def LGV.dyckWordY (w : DyckWord) (i : ℕ) : ℕ

Helper function to compute the y-coordinate at position i in a DyckWord path

Equations

• LGV.dyckWordY w i = List.count DyckStep.U (List.take i ↑w) - List.count DyckStep.D (List.take i ↑w)

def LGV.dyckWordToVertices (w : DyckWord) : List (ℤ × ℕ)

Convert a DyckWord to a list of vertices

Equations

• LGV.dyckWordToVertices w = List.map (fun (x : Fin ((↑w).length + 1)) => match x with | ⟨i, isLt⟩ => (↑i, LGV.dyckWordY w i)) (List.finRange ((↑w).length + 1))

theorem LGV.dyckWordToVertices_length (w : DyckWord) : (dyckWordToVertices w).length = (↑w).length + 1

theorem LGV.dyckWordToVertices_nonempty (w : DyckWord) : dyckWordToVertices w ≠ []

theorem LGV.dyckWordToVertices_getElem (w : DyckWord) (i : ℕ) (hi : i < (dyckWordToVertices w).length) : (dyckWordToVertices w)[i] = (↑i, dyckWordY w i)

theorem LGV.dyckWord_y_pos_before_D (w : DyckWord) (i : ℕ) (hi : i < (↑w).length) (hD : (↑w)[i] = DyckStep.D) : 0 < dyckWordY w i

Key lemma: if we take a D step at position i, then y > 0 at position i

def LGV.dyckWordToPath (w : DyckWord) : dyckDigraph.Path

Convert a DyckWord to a Dyck path from (0, 0) to (2n, 0) where n = semilength.

Note: The vertices are constructed as (i, y_i) where y_i = #U - #D in the first i steps. The Dyck word conditions ensure y_i ≥ 0 and the path stays in the valid region.

Equations

• LGV.dyckWordToPath w = { vertices := LGV.dyckWordToVertices w, nonempty := ⋯, arcs_valid := ⋯ }

theorem LGV.dyckWordToPath_start (w : DyckWord) : (dyckWordToPath w).start = (0, 0)

The start of dyckWordToPath is (0, 0)

theorem LGV.dyckWordToPath_finish (w : DyckWord) : (dyckWordToPath w).finish = (↑(2 * w.semilength), 0)

The finish of dyckWordToPath is (2 * semilength, 0)

theorem LGV.dyck_paths_eq_catalan (n : ℕ) : (pathsFromTo dyckDigraph dyckDigraph_pathFinite (0, 0) (2 * ↑n, 0)).card = catalan n

The number of Dyck paths from (0, 0) to (2n, 0) equals the n-th Catalan number. This is a classical result connecting Dyck paths to Catalan numbers.

Proof strategy: We construct a bijection between Dyck paths and DyckWords of semilength n.

• Each arc (x,y) → (x+1,y+1) corresponds to U
• Each arc (x,y) → (x+1,y-1) corresponds to D
• The Dyck condition (y ≥ 0) ensures the prefix condition for DyckWords
• Equal start and end y-coordinates ensures equal counts of U and D

Then we use Mathlib's DyckWord.card_dyckWord_semilength_eq_catalan.

Key lemmas needed:

1. dyckPathToWord is well-defined (DyckWord conditions satisfied) ✓
2. dyckWordToPath is well-defined (arc validity) ✓
3. The maps are inverses (bijection) ✓
4. dyckPathToWord maps paths from (0,0) to (2n,0) to words of semilength n ✓

def LGV.translatePath (d : ℤ) (p : dyckDigraph.Path) : dyckDigraph.Path

Create translated path by shifting x-coordinates

Equations

• LGV.translatePath d p = { vertices := List.map (LGV.translateVertex✝ d) p.vertices, nonempty := ⋯, arcs_valid := ⋯ }

theorem LGV.translatePath_injective (d : ℤ) : Function.Injective (translatePath d)

theorem LGV.dyck_paths_shifted_eq_catalan (i j : ℕ) : (pathsFromTo dyckDigraph dyckDigraph_pathFinite (-(2 * ↑i), 0) (2 * ↑j, 0)).card = catalan (i + j)

The number of Dyck paths from (-2i, 0) to (2j, 0) equals catalan(i+j). This follows from translation invariance: shifting by 2i gives a bijection with paths from (0, 0) to (2(i+j), 0), which equal catalan(i+j) by dyck_paths_eq_catalan.

theorem LGV.catalanHankelMatrix_eq_pathWeightMatrix (k : ℕ) : catalanHankelMatrix k = pathWeightMatrix dyckDigraph_pathFinite dyckUnitArcWeight (fun (i : Fin k) => (-(2 * ↑↑i), 0)) fun (j : Fin k) => (2 * ↑↑j, 0)

The Catalan Hankel matrix equals the path weight matrix for the Dyck digraph. Entry (i,j) = catalan(i+j) = number of Dyck paths from (-2i, 0) to (2j, 0).

theorem LGV.catalan_hankel_det_general (n : ℕ) : (catalanHankelMatrix (n + 8)).det = 1

General case of Catalan Hankel determinant for k ≥ 8. The proof uses the LGV lemma with Dyck paths. Source: The TeX source says "The details are LTTR" (Left To The Reader).

The full proof requires:

1. catalan_unique_nipat: There is exactly one non-intersecting path tuple
2. dyck_no_nipat_for_nonidentity: Non-identity permutations have no nipats These lemmas are defined later in this file but the proof structure requires them to be available here.

theorem LGV.catalan_hankel_det (k : ℕ) : (catalanHankelMatrix k).det = 1

Catalan Hankel determinant equals 1 (Corollary cor.lgv.catalan-hankel-det-0) Label: cor.lgv.catalan-hankel-det-0

det((c_{i+j})_{0 ≤ i,j < k}) = 1

where cₙ is the n-th Catalan number.

Note: The TeX source uses 1-indexed notation det((c_{i+j-2}){1 ≤ i,j ≤ k}), which is equivalent to our 0-indexed det((c{i+j})_{0 ≤ i,j < k}).

Proof sketch (via LGV lemma): Use the Dyck path digraph with Aᵢ = (-2i, 0) and Bᵢ = (2i, 0).

• The (i,j) entry of the path matrix counts paths from Aᵢ to Bⱼ, which equals c_{i+j} (Catalan number).
• There is exactly one non-intersecting path tuple from 𝐀 to 𝐁 (the nested Dyck paths).
• For non-identity permutations σ, there are no nipats from 𝐀 to σ(𝐁).
• By LGV, det = 1 · 1 = 1.

theorem LGV.dyck_arc_x_inc (u v : ℤ × ℕ) (h : dyckDigraph.arc u v) : v.1 = u.1 + 1

In the Dyck digraph, x-coordinate increases by 1 on each arc

theorem LGV.dyck_path_x_monotone (p : dyckDigraph.Path) (i j : ℕ) (hi : i < p.vertices.length) (hj : j < p.vertices.length) (hij : i ≤ j) : (p.vertices.get ⟨i, hi⟩).1 + (↑j - ↑i) = (p.vertices.get ⟨j, hj⟩).1

In a Dyck path, x increases strictly along the path

theorem LGV.dyck_path_x_diff (p : dyckDigraph.Path) : p.start.1 + (↑p.vertices.length - 1) = p.finish.1

The x-coordinate difference between start and finish equals path length minus 1

theorem LGV.dyck_path_trivial_if_same_x (p : dyckDigraph.Path) (h : p.start.1 = p.finish.1) : p.vertices.length = 1

A path from (x, y) to (x, y') must have length 1 (i.e., be trivial)

Nested Dyck Paths for the Catalan Hankel Determinant

The nested Dyck path from (-2n, 0) to (2n, 0) goes: (-2n, 0) → (-2n+1, 1) → ... → (0, 2n) → (1, 2n-1) → ... → (2n, 0)

At step i (0 ≤ i ≤ 4n), the vertex is (i - 2n, min(i, 4n - i)).

def LGV.nestedDyckVertices (n : ℕ) : List (ℤ × ℕ)

The vertices of the nested Dyck path from (-2n, 0) to (2n, 0)

Equations

• LGV.nestedDyckVertices n = List.map (fun (x : Fin (4 * n + 1)) => match x with | ⟨i, isLt⟩ => (↑i - 2 * ↑n, min i (4 * n - i))) (List.finRange (4 * n + 1))

theorem LGV.nestedDyckVertices_nonempty (n : ℕ) : nestedDyckVertices n ≠ []

theorem LGV.nestedDyckVertices_length (n : ℕ) : (nestedDyckVertices n).length = 4 * n + 1

theorem LGV.nestedDyckVertices_getElem (n i : ℕ) (hi : i < (nestedDyckVertices n).length) : (nestedDyckVertices n)[i] = (↑i - 2 * ↑n, min i (4 * n - i))

theorem LGV.nestedDyckVertices_arcs_valid (n i : ℕ) (hi : i + 1 < (nestedDyckVertices n).length) : dyckDigraph.arc ((nestedDyckVertices n).get ⟨i, ⋯⟩) ((nestedDyckVertices n).get ⟨i + 1, hi⟩)

def LGV.nestedDyckPath (n : ℕ) : dyckDigraph.Path

The nested Dyck path from (-2n, 0) to (2n, 0)

Equations

• LGV.nestedDyckPath n = { vertices := LGV.nestedDyckVertices n, nonempty := ⋯, arcs_valid := ⋯ }

theorem LGV.nestedDyckPath_start (n : ℕ) : (nestedDyckPath n).start = (-(2 * ↑n), 0)

theorem LGV.nestedDyckPath_finish (n : ℕ) : (nestedDyckPath n).finish = (2 * ↑n, 0)

theorem LGV.nestedDyckPath_vertex_mem (n : ℕ) (v : ℤ × ℕ) (hv : v ∈ (nestedDyckPath n).vertices) : ∃ i ≤ 4 * n, v = (↑i - 2 * ↑n, min i (4 * n - i))

theorem LGV.nestedDyckPath_disjoint (n m : ℕ) (hnm : n ≠ m) : ¬pathsIntersect (nestedDyckPath n) (nestedDyckPath m)

Different nested Dyck paths don't share any vertices

theorem LGV.dyck_path_parity (p : dyckDigraph.Path) (j : ℕ) (hj : j < p.vertices.length) : (p.vertices.get ⟨j, hj⟩).2 % 2 = (j + p.start.2) % 2

In a Dyck path, the y-coordinate at step j has the same parity as j + start.2

theorem LGV.dyck_path_y_upper_bound (p : dyckDigraph.Path) (n : ℕ) (hstart : p.start = (-(2 * ↑n), 0)) (hfinish : p.finish = (2 * ↑n, 0)) (j : ℕ) (hj : j < p.vertices.length) : (p.vertices.get ⟨j, hj⟩).2 ≤ min j (4 * n - j)

For a Dyck path from (-2n, 0) to (2n, 0), the y-coordinate at step j is ≤ min(j, 4n - j)

theorem LGV.catalan_unique_nipat (k : ℕ) : have A := fun (i : Fin k) => (-2 * ↑↑i, 0); have B := fun (i : Fin k) => (2 * ↑↑i, 0); ∃! pt : PathTuple dyckDigraph k A B, pt.isNonIntersecting

There is exactly one nipat in the Catalan Hankel setup.

The proof constructs the canonical nipat where path_i is the "nested" Dyck path from (-2i, 0) to (2i, 0) that goes up to height 2i and back down: (-2i, 0) → (-2i+1, 1) → ... → (0, 2i) → (1, 2i-1) → ... → (2i, 0)

Existence: The canonical paths form a valid PathTuple because:

• Each path is a valid Dyck path (arcs go up-right or down-right)
• Start/finish conditions are satisfied by construction

Non-intersection: The canonical paths don't intersect because:

• Path_i visits vertices (x, y) with y ≤ 2i
• At height y, path_i is at x = -2i + y (going up) or x = y (going down)
• Path_j (j > i) at height y ≤ 2i is at x = -2j + y or x = y
• These x-coordinates differ when j ≠ i

Uniqueness: Any nipat must equal the canonical one because:

• In the Dyck digraph, paths from (-2i, 0) to (2i, 0) must have length 4i
• For non-intersection with outer paths, inner paths must stay "inside"
• The only way to do this is the nested structure

Bridge Between LGV1 and LGV2 Path Representations

This section documents the connection between the path representations used in LGV1.lean (list of steps) and LGV2.lean (list of vertices), and provides key infrastructure for bridging them.

Key Insight

A LatticePath (list of east/north steps) starting at point A can be converted to a SimpleDigraph.Path by computing the list of vertices visited:

• [east, north, east] starting at (0,0) → [(0,0), (1,0), (1,1), (2,1)]

The conversion is bijective for paths between fixed endpoints.

Status

The key theorem sum_signed_ipatFinset_card_eq_zero proves that the signed sum of ipat counts is zero. To use this in LGV1.lean's lgv_involution_cancellation, we need:

numIpatsK A B σ = (ipatFinset integerLattice_pathFinite A (permuteKVertex σ B)).card

This requires showing that ipatsFromTo (LGV1) and ipatFinset (LGV2) have the same cardinality, which follows from a bijection between the path tuple representations.

Approach

The bijection works as follows:

1. Given a LatticePath (list of steps) starting at A, compute the vertex list
2. This vertex list forms a valid SimpleDigraph.Path in integerLattice
3. The map is injective because different step sequences give different vertex lists
4. The map is surjective because every SimpleDigraph.Path in integerLattice corresponds to a unique step sequence (each arc is either east or north)

The intersection property is preserved because both representations check if any vertex appears in multiple paths of the tuple.

inductive LGV.LatticeStep' : Type

A lattice step on the integer lattice: either east (+1,0) or north (0,+1).

This is the canonical definition for lattice steps. LGV1.lean defines an equivalent type LGV1.LatticeStep with an explicit equivalence LGV1.latticeStepEquiv.

The two types are isomorphic via:

• LGV1.latticeStepEquiv : LGV1.LatticeStep ≃ LGV.LatticeStep'
• LGV1.latticePathToLatticePath' : LGV1.LatticePath → LGV.LatticePath'
• LGV1.latticePath'ToLatticePath : LGV.LatticePath' → LGV1.LatticePath

Note: The duplication exists because LGV1 imports LGV2, so LGV2 cannot reference LGV1's definitions. Both definitions are intentionally kept compatible.

• east : LatticeStep'
• north : LatticeStep'

instance LGV.instDecidableEqLatticeStep' : DecidableEq LatticeStep'

Equations

• LGV.instDecidableEqLatticeStep' x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

instance LGV.instReprLatticeStep' : Repr LatticeStep'

Equations

• LGV.instReprLatticeStep' = { reprPrec := LGV.instReprLatticeStep'.repr }

def LGV.instReprLatticeStep'.repr : LatticeStep' → ℕ → Std.Format

Equations

• LGV.instReprLatticeStep'.repr LGV.LatticeStep'.east prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "LGV.LatticeStep'.east")).group prec✝
• LGV.instReprLatticeStep'.repr LGV.LatticeStep'.north prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "LGV.LatticeStep'.north")).group prec✝

def LGV.LatticeStep'.apply (s : LatticeStep') (p : ℤ × ℤ) : ℤ × ℤ

Apply a step to a lattice point

Equations

• LGV.LatticeStep'.east.apply p = (p.1 + 1, p.2)
• LGV.LatticeStep'.north.apply p = (p.1, p.2 + 1)

@[reducible, inline]

abbrev LGV.LatticePath' : Type

A lattice path as a list of steps (matching LGV1.lean's definition)

Equations

• LGV.LatticePath' = List LGV.LatticeStep'

def LGV.LatticePath'.endpoint (path : LatticePath') (start : ℤ × ℤ) : ℤ × ℤ

Compute the endpoint of a lattice path starting from a given point

Equations

• path.endpoint start = List.foldl (fun (p : ℤ × ℤ) (s : LGV.LatticeStep') => s.apply p) start path

def LGV.LatticePath'.toVertices (path : LatticePath') (start : ℤ × ℤ) : List (ℤ × ℤ)

Compute all vertices visited by a lattice path, including start. For path = [s₁, s₂, ..., sₙ], this returns [start, s₁(start), s₂(s₁(start)), ...]

Equations

• LGV.LatticePath'.toVertices [] start = [start]
• LGV.LatticePath'.toVertices (s :: rest) start = start :: LGV.LatticePath'.toVertices rest (s.apply start)

theorem LGV.LatticePath'.toVertices_nonempty (path : LatticePath') (start : ℤ × ℤ) : path.toVertices start ≠ []

The vertices list is nonempty

theorem LGV.LatticeStep'.apply_creates_arc (s : LatticeStep') (p : ℤ × ℤ) : integerLattice.arc p (s.apply p)

Each step creates a valid arc in the integer lattice

theorem LGV.LatticePath'.toVertices_arcs_valid (path : LatticePath') (start : ℤ × ℤ) (i : ℕ) (hi : i + 1 < (path.toVertices start).length) : integerLattice.arc ((path.toVertices start).get ⟨i, ⋯⟩) ((path.toVertices start).get ⟨i + 1, hi⟩)

Consecutive vertices in toVertices are connected by arcs

noncomputable def LGV.LatticePath'.toPath (path : LatticePath') (start : ℤ × ℤ) : integerLattice.Path

Convert a lattice path to a SimpleDigraph.Path

Equations

• path.toPath start = { vertices := path.toVertices start, nonempty := ⋯, arcs_valid := ⋯ }

theorem LGV.LatticePath'.toVertices_head (path : LatticePath') (start : ℤ × ℤ) : (path.toVertices start).head ⋯ = start

The first vertex is the start point

theorem LGV.LatticePath'.toPath_start (path : LatticePath') (start : ℤ × ℤ) : (path.toPath start).start = start

The start of the converted path is the original start point

theorem LGV.LatticePath'.toVertices_getLast (path : LatticePath') (start : ℤ × ℤ) : (path.toVertices start).getLast ⋯ = path.endpoint start

The last vertex is the endpoint

theorem LGV.LatticePath'.toPath_finish (path : LatticePath') (start : ℤ × ℤ) : (path.toPath start).finish = path.endpoint start

The finish of the converted path is the endpoint

theorem LGV.LatticePath'.toPath_endpoints (path : LatticePath') (A B : ℤ × ℤ) (h : path.endpoint A = B) : (path.toPath A).start = A ∧ (path.toPath A).finish = B

Key bridge lemma: A lattice path going from A to B converts to a SimpleDigraph.Path from A to B. This is the foundation for showing the path representations are equivalent.

theorem LGV.LatticePath'.toVertices_length (path : LatticePath') (start : ℤ × ℤ) : (path.toVertices start).length = List.length path + 1

The length of the vertex list equals the number of steps plus one

Bridge Bijection Lemmas

The following lemmas establish that LatticePath'.toPath is a bijection between step-based lattice paths and vertex-based digraph paths.

These lemmas provide the foundation for connecting LGV1.lean's counting results with LGV2.lean's weighted results.

theorem LGV.LatticePath'.toPath_vertices (path : LatticePath') (start : ℤ × ℤ) : (path.toPath start).vertices = path.toVertices start

The vertices of a converted path match the original vertex list

theorem LGV.SimpleDigraph.Path.ext_vertices' (p q : integerLattice.Path) (h : p.vertices = q.vertices) : p = q

Two paths with the same vertices are equal

theorem LGV.LatticePath'.toPath_injective (start : ℤ × ℤ) : Function.Injective fun (path : LatticePath') => path.toPath start

toPath is injective: different step sequences give different paths.

Proof sketch:

1. If toPath p1 start = toPath p2 start, then their vertex lists are equal
2. The vertex list uniquely determines the step sequence because:
   • Each arc in the integer lattice is uniquely determined by source and target
   • Given consecutive vertices u, v, the step is east iff v.1 = u.1 + 1
3. By induction on the path length, equal vertex lists imply equal step sequences

This is a key lemma for the bridge between LGV1 and LGV2 path representations.

Surjectivity of toPath

To complete the bridge between path representations, we need to show that every SimpleDigraph.Path in the integer lattice comes from a LatticePath'.

The key insight is that each arc in the integer lattice uniquely determines a step:

• If v.1 = u.1 + 1 (and v.2 = u.2), the step is east
• If v.2 = u.2 + 1 (and v.1 = u.1), the step is north

def LGV.arcToStep' (u v : ℤ × ℤ) (_h : integerLattice.arc u v) : LatticeStep'

Convert an arc in the integer lattice to a step. This is the inverse operation to LatticeStep'.apply.

Equations

• LGV.arcToStep' u v _h = if v.1 = u.1 + 1 then LGV.LatticeStep'.east else LGV.LatticeStep'.north

theorem LGV.arcToStep'_apply (u v : ℤ × ℤ) (h : integerLattice.arc u v) : (arcToStep' u v h).apply u = v

arcToStep' produces the correct step

def LGV.verticesToSteps' (vs : List (ℤ × ℤ)) (harcs : ∀ (i : ℕ) (hi : i + 1 < vs.length), integerLattice.arc (vs.get ⟨i, ⋯⟩) (vs.get ⟨i + 1, hi⟩)) : LatticePath'

Convert a vertex list to a step list (partial inverse of toVertices)

Equations

• LGV.verticesToSteps' [] x_2 = []
• LGV.verticesToSteps' [head] x_2 = []
• LGV.verticesToSteps' (u :: v :: rest) harcs = LGV.arcToStep' u v ⋯ :: LGV.verticesToSteps' (v :: rest) ⋯

def LGV.pathToLatticePath' (p : integerLattice.Path) : LatticePath'

Convert a SimpleDigraph.Path to a LatticePath'

Equations

• LGV.pathToLatticePath' p = LGV.verticesToSteps' p.vertices ⋯

theorem LGV.verticesToSteps'_toVertices (vs : List (ℤ × ℤ)) (hne : vs ≠ []) (harcs : ∀ (i : ℕ) (hi : i + 1 < vs.length), integerLattice.arc (vs.get ⟨i, ⋯⟩) (vs.get ⟨i + 1, hi⟩)) : (verticesToSteps' vs harcs).toVertices (vs.head hne) = vs

verticesToSteps' produces the correct vertex list when applied to the original vertices

theorem LGV.LatticePath'.toPath_surjective (start : ℤ × ℤ) (p : integerLattice.Path) : p.start = start → ∃ (path : LatticePath'), path.toPath start = p

toPath is surjective: every SimpleDigraph.Path comes from a LatticePath'.

This completes the bijection between step-based and vertex-based path representations. Together with toPath_injective, this shows that the two representations are equivalent.

noncomputable def LGV.latticePath'Equiv (start : ℤ × ℤ) : LatticePath' ≃ { p : integerLattice.Path // p.start = start }

The bijection between LatticePath' and SimpleDigraph.Path starting at a fixed point.

This establishes that the two path representations are equivalent, which is the key step needed to bridge LGV1.lean's counting results with LGV2.lean's weighted results.

Equations

• One or more equations did not get rendered due to their size.

Path Tuple Bridge

This section provides the bridge between LGV1-style path tuples (using LatticePath = List LatticeStep) and LGV2-style path tuples (using SimpleDigraph.Path).

The key results are:

1. latticePath'TupleEquiv - bijection between path tuples
2. latticePath'Tuple_isIntersecting_iff - intersection property is preserved

These results allow us to transfer the counting result sum_signed_ipatFinset_card_eq_zero from LGV2 types to LGV1 types.

structure LGV.LatticePath'Tuple (k : ℕ) (A B : kVertex (ℤ × ℤ) k) : Type

A path tuple in the LGV1 style: k paths from A to B where each path is a list of steps.

• paths : Fin k → LatticePath'

  The paths in the tuple

• valid (i : Fin k) : (self.paths i).endpoint (A i) = B i

  Each path goes from A_i to B_i

theorem LGV.LatticePath'Tuple.ext {k : ℕ} {A B : kVertex (ℤ × ℤ) k} {pt1 pt2 : LatticePath'Tuple k A B} (h : ∀ (i : Fin k), pt1.paths i = pt2.paths i) : pt1 = pt2

theorem LGV.LatticePath'Tuple.ext_iff {k : ℕ} {A B : kVertex (ℤ × ℤ) k} {pt1 pt2 : LatticePath'Tuple k A B} : pt1 = pt2 ↔ ∀ (i : Fin k), pt1.paths i = pt2.paths i

def LGV.LatticePath'Tuple.verticesOf {k : ℕ} {A B : kVertex (ℤ × ℤ) k} (pt : LatticePath'Tuple k A B) (i : Fin k) : Set (ℤ × ℤ)

The vertices visited by a path in a LatticePath'Tuple

Equations

• pt.verticesOf i = {p : ℤ × ℤ | p ∈ (pt.paths i).toVertices (A i)}

def LGV.LatticePath'Tuple.isNonIntersecting {k : ℕ} {A B : kVertex (ℤ × ℤ) k} (pt : LatticePath'Tuple k A B) : Prop

A LatticePath'Tuple is non-intersecting if no two paths share a vertex

Equations

• pt.isNonIntersecting = ∀ (i j : Fin k), i ≠ j → Disjoint (pt.verticesOf i) (pt.verticesOf j)

def LGV.LatticePath'Tuple.isIntersecting {k : ℕ} {A B : kVertex (ℤ × ℤ) k} (pt : LatticePath'Tuple k A B) : Prop

A LatticePath'Tuple is intersecting if it is not non-intersecting

Equations

• pt.isIntersecting = ¬pt.isNonIntersecting

noncomputable def LGV.latticePath'TupleToPathTuple {k : ℕ} {A B : kVertex (ℤ × ℤ) k} (pt : LatticePath'Tuple k A B) : PathTuple integerLattice k A B

Convert a LatticePath'Tuple to a PathTuple

Equations

• LGV.latticePath'TupleToPathTuple pt = { paths := fun (i : Fin k) => (pt.paths i).toPath (A i), starts := ⋯, finishes := ⋯ }

noncomputable def LGV.pathTupleToLatticePath'Tuple {k : ℕ} {A B : kVertex (ℤ × ℤ) k} (pt : PathTuple integerLattice k A B) : LatticePath'Tuple k A B

Convert a PathTuple to a LatticePath'Tuple

Equations

• LGV.pathTupleToLatticePath'Tuple pt = { paths := fun (i : Fin k) => LGV.pathToLatticePath' (pt.paths i), valid := ⋯ }

noncomputable def LGV.latticePath'TupleEquiv {k : ℕ} (A B : kVertex (ℤ × ℤ) k) : LatticePath'Tuple k A B ≃ PathTuple integerLattice k A B

The bijection between LatticePath'Tuple and PathTuple

Equations

• LGV.latticePath'TupleEquiv A B = { toFun := LGV.latticePath'TupleToPathTuple, invFun := LGV.pathTupleToLatticePath'Tuple, left_inv := ⋯, right_inv := ⋯ }

theorem LGV.latticePath'TupleToPathTuple_vertices {k : ℕ} {A B : kVertex (ℤ × ℤ) k} (pt : LatticePath'Tuple k A B) (i : Fin k) : ((latticePath'TupleToPathTuple pt).paths i).vertices = (pt.paths i).toVertices (A i)

The vertices of a converted path match the original vertices

theorem LGV.latticePath'Tuple_isIntersecting_iff {k : ℕ} {A B : kVertex (ℤ × ℤ) k} (pt : LatticePath'Tuple k A B) : pt.isIntersecting ↔ (latticePath'TupleToPathTuple pt).isIntersecting

The intersection property is preserved by the bijection