The Lindström-Gessel-Viennot Lemma: Part 1

This file formalizes the first part of the Lindström-Gessel-Viennot (LGV) lemma, covering the basic definitions and counting results for lattice paths.

Main definitions

• LGV1.LatticePoint - A point on the integer lattice ℤ²
• LGV1.integerLattice - The integer lattice as a Mathlib Digraph
• LGV1.LatticePath - A path on the integer lattice using only east (right) and north (up) steps
• LGV1.LatticePath.stepCount - The total number of steps in a path
• LGV1.LatticePath.eastStepCount - The number of east steps in a path
• LGV1.PathTuple - A k-tuple of lattice paths from k source vertices to k target vertices
• LGV1.PathTuple.isNonIntersecting - Property that no two paths share a vertex (nipat)
• LGV1.PathTuple.isIntersecting - Property that some two paths share a vertex (ipat)
• LGV1.kVertex - A k-tuple of lattice points

Main results

• latticePath_count - Number of paths from (a,b) to (c,d) equals C(c+d-a-b, c-a) (Proposition prop.lgv.1-paths.ct)
• lgv_two_paths - LGV lemma for k=2: determinant equals #nipats to (B,B') - #nipats to (B',B) (Proposition prop.lgv.2paths.count)
• baby_jordan_curve - Paths from A to B' and A' to B must intersect under NW conditions (Proposition prop.lgv.jordan-2)
• binom_log_concave - C(n,k)² ≥ C(n,k-1)·C(n,k+1) (Corollary cor.lgv.binom-unimod)
• lgv_k_paths - General LGV lemma: determinant equals signed sum of nipat counts (Proposition prop.lgv.kpaths.count)

References

• Source: AlgebraicCombinatorics/tex/Determinants/LGV1.tex (sec.det.comb.lgv)

Implementation notes

We formalize lattice paths as lists of steps (east or north), rather than as sequences of vertices. This makes it easier to work with path concatenation and step counting.

The LGV lemma relates determinants to non-intersecting lattice paths. The key insight is a sign-reversing involution that cancels intersecting path tuples.

Relationship with LGV2.lean

This file (LGV1.lean) and LGV2.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:

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

LatticeStep and LatticePath equivalence

Both files define a LatticeStep type for representing east/north steps:

• LGV1.LatticeStep (this file)
• LGV.LatticeStep' (in LGV2.lean)

These are equivalent types, with explicit conversion functions:

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

The duplication exists because LGV1 imports LGV2, preventing LGV2 from referencing LGV1's definitions. Both definitions are kept compatible with trivial conversions.

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

The Integer Lattice (Definition def.lgv.lattice)

The integer lattice ℤ² is an infinite digraph with vertices at integer points and directed edges (arcs) going east (i,j) → (i+1,j) and north (i,j) → (i,j+1).

This digraph is acyclic and path-finite (only finitely many paths between any two points).

Formalization of Definition def.lgv.lattice

From the TeX source (AlgebraicCombinatorics/tex/Determinants/LGV1.tex):

We consider the infinite simple digraph with vertex set ℤ² (so the vertices are pairs of integers) and arcs: (i,j) → (i+1,j) for all (i,j) ∈ ℤ² [east-steps/right-steps] (i,j) → (i,j+1) for all (i,j) ∈ ℤ² [north-steps/up-steps]

The entire digraph is denoted by ℤ² and called the "integer lattice" or "integer grid".

@[reducible, inline]

abbrev LGV1.LatticePoint : Type

A point on the integer lattice ℤ². The vertices of the integer lattice are pairs of integers. Label: def.lgv.lattice

Equations

• LGV1.LatticePoint = (ℤ × ℤ)

def LGV1.LatticePoint.x (p : LatticePoint) : ℤ

The x-coordinate of a lattice point.

Equations

• p.x = p.1

def LGV1.LatticePoint.y (p : LatticePoint) : ℤ

The y-coordinate of a lattice point.

Equations

• p.y = p.2

@[simp]

theorem LGV1.LatticePoint.x_mk (a b : ℤ) : x (a, b) = a

Simp lemma for the x-coordinate of a constructed lattice point.

@[simp]

theorem LGV1.LatticePoint.y_mk (a b : ℤ) : y (a, b) = b

Simp lemma for the y-coordinate of a constructed lattice point.

def LGV1.LatticePoint.coordSum (p : LatticePoint) : ℤ

The coordinate sum of a lattice point (x + y).

Equations

• p.coordSum = p.1 + p.2

@[simp]

theorem LGV1.LatticePoint.coordSum_mk (a b : ℤ) : coordSum (a, b) = a + b

Simp lemma for the coordinate sum of a constructed lattice point.

The Integer Lattice as a Digraph

We formalize the integer lattice as a Digraph instance, where an arc exists from vertex p to vertex q if and only if q is obtained from p by either:

• An east step: q = (p.1 + 1, p.2)
• A north step: q = (p.1, p.2 + 1)

def LGV1.IntegerLatticeAdj (p q : LatticePoint) : Prop

The adjacency relation for the integer lattice digraph. There is an arc from p to q iff q is one step east or north of p. Label: eq.def.lgv.lattice.east, eq.def.lgv.lattice.north

Equations

• LGV1.IntegerLatticeAdj p q = (q = (p.1 + 1, p.2) ∨ q = (p.1, p.2 + 1))

def LGV1.integerLattice : Digraph LatticePoint

The integer lattice as a digraph. This is the digraph with vertex set ℤ² and arcs (i,j) → (i+1,j) and (i,j) → (i,j+1). Label: def.lgv.lattice

Equations

• LGV1.integerLattice = { Adj := LGV1.IntegerLatticeAdj }

instance LGV1.instDecidableRelLatticePointIntegerLatticeAdj : DecidableRel IntegerLatticeAdj

Decidability of adjacency in the integer lattice.

Equations

• LGV1.instDecidableRelLatticePointIntegerLatticeAdj p q = decidable_of_iff (q.1 = p.1 + 1 ∧ q.2 = p.2 ∨ q.1 = p.1 ∧ q.2 = p.2 + 1) ⋯

theorem LGV1.integerLattice_adj_east (p : LatticePoint) : integerLattice.Adj p (p.1 + 1, p.2)

An arc exists from p to (p.1 + 1, p.2) (east step). Label: eq.def.lgv.lattice.east

theorem LGV1.integerLattice_adj_north (p : LatticePoint) : integerLattice.Adj p (p.1, p.2 + 1)

An arc exists from p to (p.1, p.2 + 1) (north step). Label: eq.def.lgv.lattice.north

theorem LGV1.integerLattice_adj_iff (p q : LatticePoint) : integerLattice.Adj p q ↔ q = (p.1 + 1, p.2) ∨ q = (p.1, p.2 + 1)

Characterization of adjacency: q is adjacent from p iff q is one step east or north. Label: def.lgv.lattice

theorem LGV1.integerLattice_irrefl (p : LatticePoint) : ¬integerLattice.Adj p p

The integer lattice has no self-loops (irreflexive).

theorem LGV1.integerLattice_coordSum_increases {p q : LatticePoint} (h : integerLattice.Adj p q) : p.coordSum < q.coordSum

The integer lattice is acyclic: the coordinate sum strictly increases along any arc. This implies there are no cycles.

theorem LGV1.integerLattice_acyclic (p q : LatticePoint) : (∃ (path : List LatticePoint), List.IsChain integerLattice.Adj path ∧ path.head? = some p ∧ path.getLast? = some q) → p.coordSum ≤ q.coordSum

The integer lattice is acyclic: if there's a chain from p to q, then p.coordSum ≤ q.coordSum. This implies there are no cycles: any path from p to itself would require p.coordSum < p.coordSum.

Lattice Steps and Paths

A step on the lattice is either east (right) or north (up). A lattice path is a sequence of steps starting from a given point.

We formalize paths as lists of steps rather than lists of vertices, which makes it easier to work with path concatenation and step counting.

inductive LGV1.LatticeStep : Type

A step on the integer lattice: either east (right) or north (up).

• east: (i,j) → (i+1,j)
• north: (i,j) → (i,j+1)

This type is equivalent to LGV.LatticeStep' defined in LGV2.lean. The equivalence is provided by latticeStepEquiv : LatticeStep ≃ LGV.LatticeStep'.

Label: eq.def.lgv.lattice.east, eq.def.lgv.lattice.north

• east : LatticeStep
• north : LatticeStep

instance LGV1.instDecidableEqLatticeStep : DecidableEq LatticeStep

Equations

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

def LGV1.instReprLatticeStep.repr : LatticeStep → ℕ → Std.Format

Equations

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

instance LGV1.instReprLatticeStep : Repr LatticeStep

Equations

• LGV1.instReprLatticeStep = { reprPrec := LGV1.instReprLatticeStep.repr }

instance LGV1.instFintypeLatticeStep : Fintype LatticeStep

Equations

• LGV1.instFintypeLatticeStep = { elems := { val := ↑LGV1.LatticeStep.enumList, nodup := LGV1.LatticeStep.enumList_nodup }, complete := LGV1.instFintypeLatticeStep._proof_1 }

def LGV1.LatticeStep.apply (s : LatticeStep) (p : LatticePoint) : LatticePoint

Apply a step to a lattice point.

Equations

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

theorem LGV1.LatticeStep.isArc (s : LatticeStep) (p : LatticePoint) : integerLattice.Adj p (s.apply p)

A step corresponds to an arc in the integer lattice digraph.

@[reducible, inline]

abbrev LGV1.LatticePath : Type

A lattice path is a list of steps.

This type is equivalent to LGV.LatticePath' defined in LGV2.lean. Conversion functions are provided:

• latticePathToLatticePath' : LatticePath → LGV.LatticePath'
• latticePath'ToLatticePath : LGV.LatticePath' → LatticePath
• latticePathToLatticePath'_endpoint proves endpoint preservation

Equations

• LGV1.LatticePath = List LGV1.LatticeStep

def LGV1.LatticePath.endpoint (path : LatticePath) (start : LatticePoint) : LatticePoint

The endpoint of a path starting from a given point.

Equations

• path.endpoint start = List.foldl (fun (p : LGV1.LatticePoint) (s : LGV1.LatticeStep) => s.apply p) start path

@[simp]

theorem LGV1.LatticePath.endpoint_nil (start : LatticePoint) : endpoint [] start = start

Simp lemma: the endpoint of an empty path is the start.

@[simp]

theorem LGV1.LatticePath.endpoint_cons (s : LatticeStep) (path : LatticePath) (start : LatticePoint) : endpoint (s :: path) start = path.endpoint (s.apply start)

Simp lemma: the endpoint of a cons path applies the first step then continues.

theorem LGV1.LatticePath.endpoint_append (path1 path2 : LatticePath) (start : LatticePoint) : (path1 ++ path2).endpoint start = path2.endpoint (path1.endpoint start)

The endpoint of appended paths: endpoint(p1 ++ p2, A) = endpoint(p2, endpoint(p1, A)).

def LGV1.LatticePath.stepCount (path : LatticePath) : ℕ

The number of steps in a path.

Equations

• path.stepCount = List.length path

@[simp]

theorem LGV1.LatticePath.stepCount_nil : stepCount [] = 0

Simp lemma: the step count of an empty path is 0.

@[simp]

theorem LGV1.LatticePath.stepCount_cons (s : LatticeStep) (path : LatticePath) : stepCount (s :: path) = List.length path + 1

Simp lemma: the step count of a cons path is one more than the rest.

def LGV1.LatticePath.eastStepCount (path : LatticePath) : ℕ

The number of east steps in a path.

Equations

• path.eastStepCount = List.count LGV1.LatticeStep.east path

@[simp]

theorem LGV1.LatticePath.eastStepCount_nil : eastStepCount [] = 0

Simp lemma: the east step count of an empty path is 0.

@[simp]

theorem LGV1.LatticePath.eastStepCount_cons_east (path : LatticePath) : eastStepCount (LatticeStep.east :: path) = path.eastStepCount + 1

Simp lemma: the east step count of a path starting with an east step.

@[simp]

theorem LGV1.LatticePath.eastStepCount_cons_north (path : LatticePath) : eastStepCount (LatticeStep.north :: path) = path.eastStepCount

Simp lemma: the east step count of a path starting with a north step.

def LGV1.LatticePath.northStepCount (path : LatticePath) : ℕ

The number of north steps in a path.

Equations

• path.northStepCount = List.count LGV1.LatticeStep.north path

@[simp]

theorem LGV1.LatticePath.northStepCount_nil : northStepCount [] = 0

Simp lemma: the north step count of an empty path is 0.

@[simp]

theorem LGV1.LatticePath.northStepCount_cons_north (path : LatticePath) : northStepCount (LatticeStep.north :: path) = path.northStepCount + 1

Simp lemma: the north step count of a path starting with a north step.

@[simp]

theorem LGV1.LatticePath.northStepCount_cons_east (path : LatticePath) : northStepCount (LatticeStep.east :: path) = path.northStepCount

Simp lemma: the north step count of a path starting with an east step.

theorem LGV1.LatticePath.stepCount_eq_east_plus_north (path : LatticePath) : path.stepCount = path.eastStepCount + path.northStepCount

A path's step count equals east steps plus north steps.

def LGV1.LatticePath.vertices (path : LatticePath) (start : LatticePoint) : List LatticePoint

All vertices visited by a path, including start and end.

Equations

• path.vertices start = (start :: List.scanl (fun (p : LGV1.LatticePoint) (s : LGV1.LatticeStep) => s.apply p) start path).tail

def LGV1.LatticePath.isPathFromTo (path : LatticePath) (a b : LatticePoint) : Prop

Check if a path goes from point a to point b.

Equations

• path.isPathFromTo a b = (path.endpoint a = b)

theorem LGV1.LatticePath.isPathFromTo_take_drop (path : LatticePath) (n : ℕ) (A B : LatticePoint) (h : path.isPathFromTo A B) : have mid := endpoint (List.take n path) A; isPathFromTo (List.take n path) A mid ∧ isPathFromTo (List.drop n path) mid B

If a path goes from A to B, then take n goes from A to an intermediate point, and drop n goes from that point to B.

theorem LGV1.LatticePath.isPathFromTo_append (head tail : LatticePath) (A v B : LatticePoint) (hhead : head.isPathFromTo A v) (htail : tail.isPathFromTo v B) : (head ++ tail).isPathFromTo A B

If head goes A→v and tail goes v→B, then head ++ tail goes A→B.

theorem LGV1.LatticeStep.coordSum_apply (s : LatticeStep) (p : LatticePoint) : (s.apply p).coordSum = p.coordSum + 1

Each step increases the coordinate sum by 1.

theorem LGV1.LatticePath.coordSum_endpoint (path : LatticePath) (start : LatticePoint) : (path.endpoint start).coordSum = start.coordSum + ↑path.stepCount

The coordinate sum increases by the step count along any path.

Counting Paths (Proposition prop.lgv.1-paths.ct)

The number of lattice paths from (a,b) to (c,d) is:

• C(c+d-a-b, c-a) if c+d ≥ a+b (i.e., d-b ≥ a-c)
• 0 if c+d < a+b

This follows from:

• Observation 1: Each path has exactly c+d-a-b steps
• Observation 2: Each path has exactly c-a east steps
• Observation 3: A path with these counts from (a,b) must end at (c,d)

theorem LGV1.path_stepCount_eq (path : LatticePath) (a b c d : ℤ) (h : path.isPathFromTo (a, b) (c, d)) : ↑path.stepCount = c + d - a - b

Observation 1: Any path from (a,b) to (c,d) has exactly c+d-a-b steps. Label: pf.prop.lgv.1-paths.ct.o1

theorem LGV1.endpoint_x_eq (path : LatticePath) (start : LatticePoint) : (path.endpoint start).1 = start.1 + ↑path.eastStepCount

Helper: The x-coordinate of the endpoint equals start.x + eastStepCount.

theorem LGV1.path_eastStepCount_eq (path : LatticePath) (a b c d : ℤ) (h : path.isPathFromTo (a, b) (c, d)) : ↑path.eastStepCount = c - a

Observation 2: Any path from (a,b) to (c,d) has exactly c-a east steps. Label: pf.prop.lgv.1-paths.ct.o2

def LGV1.pathsFromTo (a b : LatticePoint) : Set LatticePath

The set of all lattice paths from point a to point b.

Equations

• LGV1.pathsFromTo a b = {path : LGV1.LatticePath | path.isPathFromTo a b}

theorem LGV1.pathsFromTo_finite (a b : LatticePoint) : (pathsFromTo a b).Finite

The set of paths from a to b is finite.

def LGV1.numPaths (a b : LatticePoint) : ℕ

The number of paths from (a,b) to (c,d). This equals C(c+d-a-b, c-a) when c ≥ a and d ≥ b, and 0 otherwise. (Proposition prop.lgv.1-paths.ct) Label: prop.lgv.1-paths.ct

Equations

• LGV1.numPaths a b = if a.1 ≤ b.1 ∧ a.2 ≤ b.2 then (b.1 - a.1 + (b.2 - a.2)).toNat.choose (b.1 - a.1).toNat else 0

Bijection between paths and subsets

The key to proving the counting formula is establishing a bijection between:

• Lattice paths from (0,0) to (m,n) with m east steps and n north steps
• Subsets S ⊆ {0, 1, ..., m+n-1} of cardinality m

The bijection: A path corresponds to choosing which m positions (out of m+n total steps) are east steps. The subset S records exactly those positions.

theorem LGV1.numPaths_eq_card (a b : LatticePoint) (hfin : (pathsFromTo a b).Finite) : numPaths a b = hfin.toFinset.card

The number of paths formula is correct. Label: prop.lgv.1-paths.ct

The proof uses a bijection between lattice paths from a to b and subsets of {0, ..., m+n-1} of size m, where m = (b.1 - a.1).toNat and n = (b.2 - a.2).toNat. A path corresponds to choosing which m positions (out of m+n total steps) are east steps. The number of such choices is C(m+n, m).

theorem LGV1.no_paths_when_sum_decreases (a b : LatticePoint) (h : b.coordSum < a.coordSum) : pathsFromTo a b = ∅

No paths exist when c+d < a+b.

Path Tuples, Nipats, and Ipats (Definition def.lgv.path-tups)

A k-vertex is a k-tuple of lattice points. A path tuple from k-vertex A to k-vertex B is a k-tuple of paths where the i-th path goes from A_i to B_i.

A path tuple is non-intersecting (nipat) if no two paths share a vertex. A path tuple is intersecting (ipat) if some two paths share a vertex.

@[reducible, inline]

abbrev LGV1.kVertex (k : ℕ) : Type

A k-vertex is a k-tuple of lattice points. Label: def.lgv.path-tups (a)

Equations

• LGV1.kVertex k = (Fin k → LGV1.LatticePoint)

def LGV1.kVertex.permute {k : ℕ} (v : kVertex k) (σ : Equiv.Perm (Fin k)) : kVertex k

Permute a k-vertex by a permutation σ. Label: def.lgv.path-tups (b)

Equations

• v.permute σ i = v (σ i)

structure LGV1.PathTuple (k : ℕ) (A B : kVertex k) : Type

A path tuple from k-vertex A to k-vertex B. Label: def.lgv.path-tups (c)

• paths : Fin k → LatticePath

  The i-th path in the tuple

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

  Each path goes from A_i to B_i

def LGV1.PathTuple.verticesOf {k : ℕ} {A B : kVertex k} (pt : PathTuple k A B) (i : Fin k) : Set LatticePoint

The set of vertices visited by a path in a path tuple.

Equations

• pt.verticesOf i = {p : LGV1.LatticePoint | p ∈ (pt.paths i).vertices (A i)}

def LGV1.PathTuple.isNonIntersecting {k : ℕ} {A B : kVertex k} (pt : PathTuple k A B) : Prop

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

Equations

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

def LGV1.PathTuple.isIntersecting {k : ℕ} {A B : kVertex k} (pt : PathTuple k A B) : Prop

A path tuple is intersecting (ipat) if it is not non-intersecting. Label: def.lgv.path-tups (e)

Equations

• pt.isIntersecting = ¬pt.isNonIntersecting

def LGV1.pathTuplesFromTo {k : ℕ} (A B : kVertex k) : Set (PathTuple k A B)

The set of all path tuples from A to B.

Equations

• LGV1.pathTuplesFromTo A B = Set.univ

def LGV1.nipatsFromTo {k : ℕ} (A B : kVertex k) : Set (PathTuple k A B)

The set of all non-intersecting path tuples (nipats) from A to B.

Equations

• LGV1.nipatsFromTo A B = {pt : LGV1.PathTuple k A B | pt.isNonIntersecting}

def LGV1.ipatsFromTo {k : ℕ} (A B : kVertex k) : Set (PathTuple k A B)

The set of all intersecting path tuples (ipats) from A to B.

Equations

• LGV1.ipatsFromTo A B = {pt : LGV1.PathTuple k A B | pt.isIntersecting}

theorem LGV1.pathTuplesFromTo_finite {k : ℕ} (A B : kVertex k) : (pathTuplesFromTo A B).Finite

The set of path tuples from A to B is finite (follows from finiteness of paths).

theorem LGV1.nipatsFromTo_finite {k : ℕ} (A B : kVertex k) : (nipatsFromTo A B).Finite

The set of nipats from A to B is finite (subset of finite set).

theorem LGV1.ipatsFromTo_finite {k : ℕ} (A B : kVertex k) : (ipatsFromTo A B).Finite

The set of ipats from A to B is finite (subset of finite set).

General k Involution Infrastructure

The sign-reversing involution for general k path tuples works as follows: Given an intersecting path tuple (ipat), we:

1. Find the smallest path index i that contains a "crowded" vertex (shared with another path)
2. Find the first crowded vertex v on path i (by position in the path)
3. Find the largest path index j that contains v (j > i since v is crowded)
4. Exchange the tails of paths i and j at v
5. Compose σ with the transposition (i j) to flip the sign

This maps (σ, ipat) to (σ * swap(i,j), ipat') where:

• sign(σ * swap(i,j)) = -sign(σ) (transposition flips sign)
• ipat' is still intersecting (v is still a crowded point)
• The involution is its own inverse (applying twice returns the original)

Since every ipat has at least one crowded point, the involution has no fixed points.

def LGV1.PathTuple.isCrowded {k : ℕ} {A B : kVertex k} (pt : PathTuple k A B) (v : LatticePoint) : Prop

A vertex is crowded in a path tuple if it appears in at least two paths

Equations

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

theorem LGV1.PathTuple.isIntersecting_iff_exists_crowded {k : ℕ} {A B : kVertex k} (pt : PathTuple k A B) : pt.isIntersecting ↔ ∃ (v : LatticePoint), pt.isCrowded v

An intersecting path tuple has at least one crowded vertex

noncomputable def LGV1.PathTuple.crowdedPathIndices {k : ℕ} {A B : kVertex k} (pt : PathTuple 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 ∧ ¬Disjoint (pt.verticesOf i) (pt.verticesOf j)}

theorem LGV1.PathTuple.isIntersecting_iff_crowdedPathIndices_nonempty {k : ℕ} {A B : kVertex k} (pt : PathTuple k A B) : pt.isIntersecting ↔ pt.crowdedPathIndices.Nonempty

An intersecting path tuple has nonempty crowdedPathIndices

noncomputable def LGV1.PathTuple.minCrowdedPathIndex {k : ℕ} {A B : kVertex k} (pt : PathTuple k A B) (hip : pt.isIntersecting) : Fin k

The minimum crowded path index for an intersecting path tuple. This is the smallest index i such that path i shares a vertex with some other path.

This is a key component of the sign-reversing involution for general k: the involution swaps tails at the first crowded vertex on this path.

Equations

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

theorem LGV1.PathTuple.minCrowdedPathIndex_mem {k : ℕ} {A B : kVertex k} (pt : PathTuple k A B) (hip : pt.isIntersecting) : pt.minCrowdedPathIndex hip ∈ pt.crowdedPathIndices

The min crowded path index is in crowdedPathIndices

theorem LGV1.PathTuple.minCrowdedPathIndex_le {k : ℕ} {A B : kVertex k} (pt : PathTuple k A B) (hip : pt.isIntersecting) (i : Fin k) (hi : i ∈ pt.crowdedPathIndices) : pt.minCrowdedPathIndex hip ≤ i

The min crowded path index is minimal

def LGV1.PathTuple.crowdedVerticesOnPath {k : ℕ} {A B : kVertex k} (pt : PathTuple k A B) (i : Fin k) : Set LatticePoint

The crowded vertices on a specific path: vertices that appear in multiple paths

Equations

• pt.crowdedVerticesOnPath i = {v : LGV1.LatticePoint | v ∈ pt.verticesOf i ∧ ∃ (j : Fin k), i ≠ j ∧ v ∈ pt.verticesOf j}

theorem LGV1.PathTuple.crowdedVerticesOnMinPath_nonempty {k : ℕ} {A B : kVertex k} (pt : PathTuple k A B) (hip : pt.isIntersecting) : (pt.crowdedVerticesOnPath (pt.minCrowdedPathIndex hip)).Nonempty

The crowded vertices on the min crowded path are nonempty

theorem LGV1.PathTuple.verticesOf_finite {k : ℕ} {A B : kVertex k} (pt : PathTuple k A B) (i : Fin k) : (pt.verticesOf i).Finite

The vertices on a path form a finite set

def LGV1.pathTupleWithPerm {k : ℕ} (A B : kVertex k) : Type

A path tuple with permutation: pairs (σ, pt) where pt is a path tuple from A to σ(B)

Equations

• LGV1.pathTupleWithPerm A B = ((σ : Equiv.Perm (Fin k)) × LGV1.PathTuple k A (B.permute σ))

def LGV1.signOfPathTupleWithPerm {k : ℕ} {A B : kVertex k} (sp : pathTupleWithPerm A B) : ℤ

The sign of a path tuple with permutation

Equations

• LGV1.signOfPathTupleWithPerm sp = ↑(Equiv.Perm.sign sp.fst)

def LGV1.ipatWithPerm {k : ℕ} (A B : kVertex k) : Set (pathTupleWithPerm A B)

The set of all ipats with permutation

Equations

• LGV1.ipatWithPerm A B = {sp : LGV1.pathTupleWithPerm A B | sp.snd.isIntersecting}

theorem LGV1.ipatWithPerm_finite {k : ℕ} (A B : kVertex k) : (ipatWithPerm A B).Finite

The set of ipats with permutation is finite

The LGV Lemma for Two Paths (Proposition prop.lgv.2paths.count)

For two 2-vertices (A, A') and (B, B'):

det | #paths(A→B) #paths(A→B') | | #paths(A'→B) #paths(A'→B') |

= #nipats from (A,A') to (B,B') - #nipats from (A,A') to (B',B)

The proof uses a sign-reversing involution on intersecting path tuples that exchanges the tails of two intersecting paths.

def LGV1.pathMatrix2 (A A' B B' : LatticePoint) : Matrix (Fin 2) (Fin 2) ℤ

The path count matrix for two source and target points.

Equations

• LGV1.pathMatrix2 A A' B B' = !![↑(LGV1.numPaths A B), ↑(LGV1.numPaths A B'); ↑(LGV1.numPaths A' B), ↑(LGV1.numPaths A' B')]

noncomputable def LGV1.numNipats2 (A A' B B' : LatticePoint) : ℕ

Number of nipats from (A,A') to (B,B'). Defined as the cardinality of the set of non-intersecting path tuples.

Equations

• LGV1.numNipats2 A A' B B' = (LGV1.nipatsFromTo ![A, A'] ![B, B']).ncard

theorem LGV1.pathMatrix2_det (A A' B B' : LatticePoint) : (pathMatrix2 A A' B B').det = ↑(numPaths A B) * ↑(numPaths A' B') - ↑(numPaths A B') * ↑(numPaths A' B)

Helper: the 2x2 determinant expands to the difference of products.

structure LGV1.SignedPathTuple2 (A A' B B' : LatticePoint) : Type

A path tuple from (A,A') to (B,B') or (B',B) with a sign. Sign is +1 for (B,B') and -1 for (B',B).

• path0 : LatticePath

  The first path

• path1 : LatticePath

  The second path

• toBB' : Bool

  Whether this is to (B,B') (true) or (B',B) (false)

• valid0 : self.path0.isPathFromTo A (if self.toBB' = true then B else B')

  Path 0 goes from A to its destination

• valid1 : self.path1.isPathFromTo A' (if self.toBB' = true then B' else B)

  Path 1 goes from A' to its destination

def LGV1.SignedPathTuple2.sign {A A' B B' : LatticePoint} (spt : SignedPathTuple2 A A' B B') : ℤ

The sign of a signed path tuple.

Equations

• spt.sign = if spt.toBB' = true then 1 else -1

def LGV1.SignedPathTuple2.isIntersecting {A A' B B' : LatticePoint} (spt : SignedPathTuple2 A A' B B') : Prop

Check if a signed path tuple is intersecting (the two paths share a vertex).

Equations

• spt.isIntersecting = ∃ v ∈ spt.path0.vertices A, v ∈ spt.path1.vertices A'

def LGV1.signedPathTuples2 (A A' B B' : LatticePoint) : Set (SignedPathTuple2 A A' B B')

The set of all signed path tuples from (A,A') to (B,B') or (B',B).

Equations

• LGV1.signedPathTuples2 A A' B B' = Set.univ

def LGV1.signedIpats2 (A A' B B' : LatticePoint) : Set (SignedPathTuple2 A A' B B')

The set of intersecting signed path tuples.

Equations

• LGV1.signedIpats2 A A' B B' = {spt : LGV1.SignedPathTuple2 A A' B B' | spt.isIntersecting}

def LGV1.signedNipats2 (A A' B B' : LatticePoint) : Set (SignedPathTuple2 A A' B B')

The set of non-intersecting signed path tuples.

Equations

• LGV1.signedNipats2 A A' B B' = {spt : LGV1.SignedPathTuple2 A A' B B' | ¬spt.isIntersecting}

Deterministic intersection point selection

The key to proving that the sign-reversing involution is involutive is to use a deterministic choice of intersection point. We define firstIntersection to be the first intersection point in path0's vertex list (by index). This ensures that after swapping tails, the same point is still the first intersection.

noncomputable def LGV1.firstIntersectionIdx {A A' B B' : LatticePoint} (spt : SignedPathTuple2 A A' B B') (_h : spt.isIntersecting) : ℕ

The index of the first intersection point in path0's vertices. This is the smallest index i such that (path0.vertices A)[i] ∈ path1.vertices A'.

Equations

• LGV1.firstIntersectionIdx spt _h = List.findIdx (fun (v : LGV1.LatticePoint) => decide (v ∈ spt.path1.vertices A')) (spt.path0.vertices A)

theorem LGV1.firstIntersectionIdx_lt {A A' B B' : LatticePoint} (spt : SignedPathTuple2 A A' B B') (h : spt.isIntersecting) : firstIntersectionIdx spt h < (spt.path0.vertices A).length

The index of the first intersection point is valid (less than the length of path0's vertices).

noncomputable def LGV1.firstIntersection {A A' B B' : LatticePoint} (spt : SignedPathTuple2 A A' B B') (h : spt.isIntersecting) : LatticePoint

The first intersection point of two intersecting paths. This is the first vertex (by index in path0) that is shared by both paths.

Equations

• LGV1.firstIntersection spt h = (spt.path0.vertices A)[LGV1.firstIntersectionIdx spt h]

theorem LGV1.firstIntersection_mem_path0 {A A' B B' : LatticePoint} (spt : SignedPathTuple2 A A' B B') (h : spt.isIntersecting) : firstIntersection spt h ∈ spt.path0.vertices A

The first intersection point is in path0's vertices.

theorem LGV1.firstIntersection_mem_path1 {A A' B B' : LatticePoint} (spt : SignedPathTuple2 A A' B B') (h : spt.isIntersecting) : firstIntersection spt h ∈ spt.path1.vertices A'

The first intersection point is in path1's vertices.

theorem LGV1.firstIntersection_is_first {A A' B B' : LatticePoint} (spt : SignedPathTuple2 A A' B B') (h : spt.isIntersecting) : have v := firstIntersection spt h; let idx := firstIntersectionIdx spt h; (spt.path0.vertices A)[idx] = v ∧ ∀ (i : ℕ) (hi : i < idx), (spt.path0.vertices A)[i] ∉ spt.path1.vertices A'

The first intersection point is the first vertex (by index in path0) shared by both paths. This is a key property for proving the involution is involutive: after swapping tails, the same point v is still the first intersection because:

1. The head of path0 (indices 0..idx) is unchanged
2. v is at index idx in both the original and swapped paths
3. No earlier vertex in path0's head is in path1's vertices (by minimality of findIdx)

noncomputable def LGV1.splitPathAt (path : LatticePath) (start v : LatticePoint) (_hv : v ∈ path.vertices start) : LatticePath × LatticePath

Split a path at a vertex, returning (head, tail) where head ends at v and tail starts at v.

Equations

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

Helper lemmas for the involution proof

noncomputable def LGV1.ipatInvolution {A A' B B' : LatticePoint} (spt : SignedPathTuple2 A A' B B') (h : spt.isIntersecting) : SignedPathTuple2 A A' B B'

The sign-reversing involution on intersecting signed path tuples. Given an ipat, we:

1. Find the first intersection point v (deterministically, by index in path0)
2. Exchange the tails of the two paths at v
3. Flip the sign (swap toBB')

This maps ipats to (B,B') ↔ ipats to (B',B).

Note: We use firstIntersection instead of Classical.choose to ensure the involution is truly involutive. The key property is that after swapping tails, the same point v is still the first intersection point.

Equations

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

theorem LGV1.ipatInvolution_sign {A A' B B' : LatticePoint} (spt : SignedPathTuple2 A A' B B') (h : spt.isIntersecting) : (ipatInvolution spt h).sign = -spt.sign

The involution is sign-reversing.

theorem LGV1.ipatInvolution_isIntersecting {A A' B B' : LatticePoint} (spt : SignedPathTuple2 A A' B B') (h : spt.isIntersecting) : (ipatInvolution spt h).isIntersecting

The involution preserves being intersecting.

theorem LGV1.firstIntersection_preserved {A A' B B' : LatticePoint} (spt : SignedPathTuple2 A A' B B') (h : spt.isIntersecting) (h' : (ipatInvolution spt h).isIntersecting) : firstIntersection (ipatInvolution spt h) h' = firstIntersection spt h

Key lemma: The first intersection point is preserved after swapping tails.

If we swap tails at the first intersection point v, then v is still the first intersection point in the new paths. This is because:

1. The head of path0 (vertices 0..idx) is unchanged
2. v is at index idx in both the original and new path0's vertices
3. No earlier vertex in head0 is in path1's vertices (by minimality)

This lemma is essential for proving that the involution is involutive.

theorem LGV1.ipatInvolution_involutive {A A' B B' : LatticePoint} (spt : SignedPathTuple2 A A' B B') (h : spt.isIntersecting) : have spt' := ipatInvolution spt h; ∃ (h' : spt'.isIntersecting), ipatInvolution spt' h' = spt

The involution is its own inverse.

After applying the involution twice, we get back the original path tuple. The key insight is that:

1. The first intersection point v is preserved after swapping tails (by firstIntersection_preserved)
2. The indices idx0 and idx1 are also preserved
3. Exchanging tails twice returns the original paths (take_append_drop)
4. toBB' flips twice (!!b = b)

Proof strategy:

• Use firstIntersection_preserved to show v' = v
• Use findIdx_beq_eq_firstIntersectionIdx and findIdx_beq_newPath1_eq to show idx0' = idx0 and idx1' = idx1
• Apply List.take_append_drop to reconstruct the original paths

theorem LGV1.signedPathTuples2_finite (A A' B B' : LatticePoint) : (signedPathTuples2 A A' B B').Finite

The set of signed path tuples is finite.

theorem LGV1.signedNipats2_finite (A A' B B' : LatticePoint) : (signedNipats2 A A' B B').Finite

The set of non-intersecting signed path tuples is finite.

theorem LGV1.signedIpats2_finite (A A' B B' : LatticePoint) : (signedIpats2 A A' B B').Finite

The set of intersecting signed path tuples is finite.

theorem LGV1.sum_signedPathTuples2 (A A' B B' : LatticePoint) (hfin : (signedPathTuples2 A A' B B').Finite) : ∑ spt ∈ hfin.toFinset, spt.sign = ↑(numPaths A B) * ↑(numPaths A' B') - ↑(numPaths A B') * ↑(numPaths A' B)

The sum over all signed path tuples equals the difference of path tuple counts.

theorem LGV1.sum_signedIpats2_eq_zero (A A' B B' : LatticePoint) (hfin : (signedIpats2 A A' B B').Finite) : ∑ spt ∈ hfin.toFinset, spt.sign = 0

The sum over intersecting path tuples is zero (by sign-reversing involution).

theorem LGV1.sum_signedNipats2 (A A' B B' : LatticePoint) (hfin : (signedNipats2 A A' B B').Finite) : ∑ spt ∈ hfin.toFinset, spt.sign = ↑(numNipats2 A A' B B') - ↑(numNipats2 A A' B' B)

The sum over non-intersecting path tuples equals the difference of nipat counts.

theorem LGV1.lgv_two_paths (A A' B B' : LatticePoint) : (pathMatrix2 A A' B B').det = ↑(numNipats2 A A' B B') - ↑(numNipats2 A A' B' B)

The LGV lemma for two paths. (Proposition prop.lgv.2paths.count) Label: prop.lgv.2paths.count

The proof uses a sign-reversing involution on intersecting path tuples:

1. Expand the determinant: det(M) = #paths(A→B)·#paths(A'→B') - #paths(A→B')·#paths(A'→B)
2. By product rule, this equals #pathTuples(→(B,B')) - #pathTuples(→(B',B))
3. Define signed path tuples with sign +1 for (B,B') and -1 for (B',B)
4. The involution exchanges tails at the first intersection, flipping the sign
5. By Lemma lem.sign.cancel2, ipats cancel, leaving only nipats

Baby Jordan Curve Theorem (Proposition 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' must intersect any path from A' to B.

This means:

• x(A') ≤ x(A) and y(A') ≥ y(A)
• x(B') ≤ x(B) and y(B') ≥ y(B)

Under these conditions, #nipats from (A,A') to (B',B) = 0.

def LGV1.isWeaklyNorthwestOf (p q : LatticePoint) : Prop

Point p is weakly northwest of point q.

Equations

• LGV1.isWeaklyNorthwestOf p q = (p.x ≤ q.x ∧ p.y ≥ q.y)

theorem LGV1.path_coords_nondecreasing (path : LatticePath) (a b : LatticePoint) (h : path.isPathFromTo a b) : a.1 ≤ b.1 ∧ a.2 ≤ b.2

Helper: If a path exists from a to b, then a.1 ≤ b.1 and a.2 ≤ b.2.

theorem LGV1.start_mem_vertices (path : LatticePath) (start : LatticePoint) : start ∈ path.vertices start

Helper: Start vertex is in vertices.

theorem LGV1.mem_vertices_cons (s : LatticeStep) (rest : LatticePath) (start v : LatticePoint) : v ∈ LatticePath.vertices (s :: rest) start ↔ v = start ∨ v ∈ rest.vertices (s.apply start)

Helper: Vertices of a cons path.

theorem LGV1.vertices_cons_subset (s : LatticeStep) (rest : LatticePath) (start v : LatticePoint) : v ∈ rest.vertices (s.apply start) → v ∈ LatticePath.vertices (s :: rest) start

Helper: Vertices of tail are contained in vertices of full path.

@[irreducible]

theorem LGV1.baby_jordan_curve (A A' B B' : LatticePoint) (hA : isWeaklyNorthwestOf A' A) (hB : isWeaklyNorthwestOf B' B) (p p' : LatticePath) (hp : p.isPathFromTo A B') (hp' : p'.isPathFromTo A' B) : ∃ v ∈ p.vertices A, v ∈ p'.vertices A'

Baby Jordan curve theorem: Under NW conditions, paths must intersect. (Proposition prop.lgv.jordan-2) Label: prop.lgv.jordan-2

Proof strategy (from tex source, Section sec.details.det.comb):

The proof is by strong induction on ℓ(p) + ℓ(p'), the sum of path lengths.

Base case: If ℓ(p) + ℓ(p') = 0, then both paths are empty, so A = B' and A' = B. From the NW conditions:

• A'.x ≤ A.x = B'.x ≤ B.x = A'.x, so A'.x = A.x
• A'.y ≥ A.y = B'.y ≥ B.y = A'.y, so A'.y = A.y Thus A = A', and A is a common vertex.

Induction step: Assume the theorem holds for smaller path lengths. If A = A', then A is a common vertex and we're done. Otherwise, since A' is weakly NW of A and A ≠ A', we have either:

• Case 1: A'.y > A.y (A' strictly north of A)
• Case 2: A'.x < A.x (A' strictly west of A)

In Case 1 (A'.y > A.y):

• Let P be the next vertex after A on path p

• If the first step of p is north, then P = (A.x, A.y + 1)

• Since A'.y > A.y and integers, A'.y ≥ A.y + 1 = P.y

• So A' is still weakly NW of P

• The rest of p goes from P to B', and p' goes from A' to B

• By IH (with smaller path length), these paths intersect

• Any common vertex of (rest of p) and p' is also on p

• If the first step of p is east, then P = (A.x + 1, A.y)

• We need to look at the first step of p' and apply IH appropriately

Case 2 (A'.x < A.x) is symmetric, looking at the first step of p' instead.

The key insight is that the "river" created by path p from A to B' must be crossed by path p' from A' to B, since A' is northwest of A and B' is northwest of B.

Reference: https://math.stackexchange.com/questions/2870640/

theorem LGV1.no_nipats_under_nw (A A' B B' : LatticePoint) (hA : isWeaklyNorthwestOf A' A) (hB : isWeaklyNorthwestOf B' B) : numNipats2 A A' B' B = 0

Under NW conditions, there are no nipats from (A,A') to (B',B). Label: prop.lgv.jordan-2

Log-Concavity of Binomial Coefficients (Corollary cor.lgv.binom-unimod)

As an application of the LGV lemma: C(n,k)² ≥ C(n,k-1) · C(n,k+1)

This follows by choosing appropriate lattice points and applying Propositions prop.lgv.2paths.count and prop.lgv.jordan-2.

theorem LGV1.binom_log_concave (n k : ℕ) (hk : 1 ≤ k) : n.choose k * n.choose k ≥ n.choose (k - 1) * n.choose (k + 1)

Binomial coefficients are log-concave. (Corollary cor.lgv.binom-unimod) Label: cor.lgv.binom-unimod

For k ≥ 1: C(n,k)² ≥ C(n,k-1) · C(n,k+1)

Note: We require k ≥ 1 because in natural number arithmetic, (0:ℕ) - 1 = 0, so C(n, 0-1) = C(n, 0) = 1, and the inequality 1 ≥ n fails for n ≥ 2. In the mathematical statement, C(n, -1) = 0, so the k=0 case is trivially true.

Proof sketch (algebraic): Using the recurrences

• C(n, k+1) · (k+1) = C(n, k) · (n-k)
• C(n, k) · k = C(n, k-1) · (n-k+1) we can show that C(n,k)² / (C(n,k-1) · C(n,k+1)) = (k+1)(n-k+1) / (k(n-k)). This ratio is ≥ 1 because (k+1)(n-k+1) - k(n-k) = n + 1 ≥ 0.

Combinatorial proof (via LGV): Define lattice points A=(1,0), A'=(0,1), B=(k+1, n-k), B'=(k, n-k+1). Then det(path matrix) = #nipats ≥ 0.

The LGV Lemma for k Paths (Proposition prop.lgv.kpaths.count)

For k-vertices A = (A₁, ..., Aₖ) and B = (B₁, ..., Bₖ):

det(#paths from Aᵢ to Bⱼ){i,j} = ∑{σ ∈ Sₖ} (-1)^σ · #nipats from A to σ(B)

The proof generalizes the k=2 case by using a sign-reversing involution that picks the first pair of intersecting paths and exchanges their tails.

Helper lemmas for the product rule

theorem LGV1.pathTuplesFromTo_ncard_eq_prod {k : ℕ} (A B : kVertex k) : (pathTuplesFromTo A B).ncard = ∏ i : Fin k, (pathsFromTo (A i) (B i)).ncard

The ncard of pathTuplesFromTo equals the product of ncards of pathsFromTo. This is the "product rule" for path tuples.

theorem LGV1.prod_numPaths_eq_pathTuples_ncard {k : ℕ} (A B : kVertex k) : ∏ i : Fin k, numPaths (A i) (B i) = (pathTuplesFromTo A B).ncard

The product of numPaths equals the ncard of pathTuplesFromTo.

def LGV1.pathMatrixK {k : ℕ} (A B : kVertex k) : Matrix (Fin k) (Fin k) ℤ

The path count matrix for k source and target vertices.

Equations

• LGV1.pathMatrixK A B = Matrix.of fun (i j : Fin k) => ↑(LGV1.numPaths (A i) (B j))

noncomputable def LGV1.numNipatsK {k : ℕ} (A B : kVertex k) (σ : Equiv.Perm (Fin k)) : ℕ

Number of nipats from A to σ(B). Defined as the cardinality of the set of non-intersecting path tuples.

Equations

• LGV1.numNipatsK A B σ = (LGV1.nipatsFromTo A (B.permute σ)).ncard

noncomputable def LGV1.numIpatsK {k : ℕ} (A B : kVertex k) (σ : Equiv.Perm (Fin k)) : ℕ

Number of ipats from A to σ(B). Defined as the cardinality of the set of intersecting path tuples.

Equations

• LGV1.numIpatsK A B σ = (LGV1.ipatsFromTo A (B.permute σ)).ncard

Bridge to LGV2.lean

We establish the connection between LGV1's path representation and LGV2's. The key observation is that both represent the same mathematical objects.

The bridge uses the following chain of equivalences:

1. LGV1.LatticeStep ≃ LGV.LatticeStep' (both are {east, north})
2. LGV1.LatticePath ≃ LGV.LatticePath' (both are lists of steps)
3. LGV1.PathTuple k A B ≃ LGV.LatticePath'Tuple k A B (same structure)
4. LGV.LatticePath'Tuple k A B ≃ LGV.PathTuple integerLattice k A B (via latticePath'TupleEquiv)

The intersection property is preserved at each step, so:

• ipatsFromTo A B ≃ ipatSet integerLattice A B
• numIpatsK A B σ = (ipatFinset ... A (permuteKVertex σ B)).card

def LGV1.latticeStepEquiv : LatticeStep ≃ LGV.LatticeStep'

Equivalence between LGV1.LatticeStep and LGV.LatticeStep'.

This is a definitional equivalence: both types have the same structure (two constructors east and north), so the equivalence is trivial. The equivalence preserves the apply function: latticeStepEquiv_apply.

Equations

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

theorem LGV1.latticeStepEquiv_apply (s : LatticeStep) (p : LatticePoint) : (latticeStepEquiv s).apply p = s.apply p

The step equivalence preserves the apply function

def LGV1.latticePathToLatticePath' (path : LatticePath) : LGV.LatticePath'

Map a LatticePath to a LatticePath'

Equations

• LGV1.latticePathToLatticePath' path = List.map (⇑LGV1.latticeStepEquiv) path

def LGV1.latticePath'ToLatticePath (path : LGV.LatticePath') : LatticePath

Map a LatticePath' to a LatticePath

Equations

• LGV1.latticePath'ToLatticePath path = List.map (⇑LGV1.latticeStepEquiv.symm) path

theorem LGV1.latticePathToLatticePath'_endpoint (path : LatticePath) (start : LatticePoint) : (latticePathToLatticePath' path).endpoint start = path.endpoint start

The path mapping preserves endpoints

theorem LGV1.latticePathToLatticePath'_toVertices (path : LatticePath) (start : LatticePoint) : (latticePathToLatticePath' path).toVertices start = path.vertices start

The path mapping preserves vertices

theorem LGV1.permute_eq_permuteKVertex {k : ℕ} (B : kVertex k) (σ : Equiv.Perm (Fin k)) : B.permute σ = LGV.permuteKVertex σ B

The permutation functions are equal

theorem LGV1.numIpatsK_eq_ipatFinset_card {k : ℕ} (A B : kVertex k) (σ : Equiv.Perm (Fin k)) : numIpatsK A B σ = (LGV.ipatFinset LGV.integerLattice_pathFinite A (LGV.permuteKVertex σ B)).card

theorem LGV1.det_eq_sum_path_tuples {k : ℕ} (A B : kVertex k) : (pathMatrixK A B).det = ∑ σ : Equiv.Perm (Fin k), ↑(Equiv.Perm.sign σ) * ∏ i : Fin k, ↑(numPaths (A i) (B (σ i)))

The determinant equals a sum over path tuples to σ(B). This rewrites det(M) = ∑ σ, sign(σ) * ∏ᵢ M(σ i, i) into det(M) = ∑ σ, sign(σ) * ∏ᵢ numPaths(A i, B(σ i)).

theorem LGV1.lgv_involution_cancellation {k : ℕ} (A B : kVertex k) : ∑ σ : Equiv.Perm (Fin k), ↑(Equiv.Perm.sign σ) * ∏ i : Fin k, ↑(numPaths (A i) (B (σ i))) = ∑ σ : Equiv.Perm (Fin k), ↑(Equiv.Perm.sign σ) * ↑(numNipatsK A B σ)

The key combinatorial lemma: intersecting path tuples cancel via sign-reversing involution.

This encapsulates the main combinatorial content of the LGV lemma:

1. ∏ᵢ numPaths(A i, B(σ i)) = #path tuples from A to σ(B) (product rule)
2. Intersecting path tuples cancel via sign-reversing involution
3. Only non-intersecting path tuples (nipats) survive

The sign-reversing involution works by:

• Finding the first crowded point v on the path with smallest index i
• Finding the largest index j of a path containing v
• Exchanging tails of paths pᵢ and pⱼ at v
• Composing σ with the transposition (i,j) to flip the sign

By Finset.sum_involution, the intersecting path tuples cancel. Label: pf.prop.lgv.kpaths.count.involution

theorem LGV1.lgv_k_paths {k : ℕ} (A B : kVertex k) : (pathMatrixK A B).det = ∑ σ : Equiv.Perm (Fin k), ↑(Equiv.Perm.sign σ) * ↑(numNipatsK A B σ)

The LGV lemma for k paths. (Proposition prop.lgv.kpaths.count)

For k-vertices A = (A₁, ..., Aₖ) and B = (B₁, ..., Bₖ): det(#paths from Aᵢ to Bⱼ){i,j} = ∑{σ ∈ Sₖ} (-1)^σ · #nipats from A to σ(B)

The proof uses:

1. The determinant formula: det(M) = ∑ σ, sign(σ) * ∏ᵢ M(σ i, i)
2. Rewriting in terms of path tuples to σ(B)
3. A sign-reversing involution that cancels intersecting path tuples

Label: prop.lgv.kpaths.count

Sign-Reversing Involution (Proof Technique)

The proofs of the LGV lemmas use a sign-reversing involution on intersecting path tuples. Given an ipat, we:

1. Find the first intersection point v (first crowded point on the path with smallest index)
2. Let i be the smallest index of a path containing v
3. Let j be the largest index of a path containing v (j > i since v is crowded)
4. Exchange the tails (parts after v) of paths pᵢ and pⱼ
5. Compose σ with the transposition (i j)

This involution:

• Maps ipats to ipats
• Reverses sign (since composing with a transposition changes parity)
• Has no fixed points
• Is its own inverse (applying twice returns the original)

By Lemma lem.sign.cancel2, the sum over ipats cancels, leaving only nipats.