This is the special case of Theorem 5.155 for the integer lattice \(\mathbb {Z}^2\), which is a path-finite acyclic digraph.

The same argument as for Proposition 5.153 can be used here; just replace \(\operatorname {sign}(\sigma , \mathbf{p}) := (-1)^{\sigma }\) by \(\operatorname {sign}(\sigma , \mathbf{p}) = (-1)^{\sigma } \cdot w(\mathbf{p})\). The only new observation required is that when we exchange the tails of two paths in our path tuple, the weight of the path tuple does not change. This is clear: the weight of a path tuple is the product of the weights of all arcs in all paths of the tuple; when we exchange the tails of two paths, some arcs get moved from one path to the other, but the total product stays unchanged.

More precisely, the proof expands the determinant via the Leibniz formula. Each summand \((-1)^\sigma \prod _i M_{i,\sigma (i)}\) expands (by distributivity) into a sum over all path tuples from \(\mathbf{A}\) to \(\sigma (\mathbf{B})\), weighted by \((-1)^\sigma \, w(\mathbf{p})\). Split the sum into non-intersecting and intersecting path tuples.

For the intersecting path tuples, a sign-reversing involution \(\varphi \) (Lemma 5.161) is defined as follows: given an intersecting path tuple paired with a permutation \((\sigma , \mathbf{p})\), find the canonical first intersection point, exchange the tails of the two relevant paths at that point, and compose \(\sigma \) with the corresponding transposition. This involution reverses the sign factor \((-1)^\sigma \) (Lemma 5.162) while preserving the weight \(w(\mathbf{p})\) (Lemma 5.163), and has no fixed points among intersecting path tuples (Lemma 5.164). Therefore the contributions of intersecting path tuples cancel in pairs, leaving only the non-intersecting ones.

If a vertex appeared twice at positions \(i {\lt} j\), we could extract the subpath from \(i\) to \(j\), which forms a cycle. By acyclicity, this subpath has length \(1\), so \(i = j\).

The weight of a path is the product of the weights of its arcs. When we exchange tails at \(v\), arcs are redistributed between the two paths, but the total multiset of arcs is preserved. Hence the product is unchanged.

Exchanging tails at \(v\) twice returns each path to its original form, since the head and tail of each path at \(v\) are restored.

By Lemma 5.158, exchanging tails is an involution. If the result were non-intersecting, applying \(\varphi \) again would give a non-intersecting tuple equal to the original (contradicting the hypothesis that it is intersecting).

The head of path \(i\) (vertices before \(v\), inclusive) is unchanged by the tail exchange, so \(v\) remains the first crowded vertex on path \(i\). Furthermore, \(i\) is still the smallest crowded path index (indices below \(i\) have unchanged paths), and \(j\) is still the largest index sharing vertex \(v\) with \(i\) (the set of path indices containing \(v\) is preserved).

After applying \(\varphi \), the canonical intersection data \((i, j, v)\) is preserved (Lemma 5.160). Applying \(\varphi \) again thus uses the same \((i, j, v)\), and the paths and permutation are restored by Lemma 5.158 and the identity \((\sigma \cdot (i\; j)) \cdot (i\; j) = \sigma \).

The permutation component of \(\varphi (\sigma , \mathbf{p})\) is \(\sigma \cdot (i\; j)\) for distinct \(i \ne j\) (Lemma 5.165). Since transpositions have sign \(-1\), the sign of the new permutation is \(-(-1)^\sigma \).

Only paths \(i\) and \(j\) are modified (their tails are exchanged), and the remaining paths are unchanged (Lemma 5.166). By Lemma 5.157, the product of the weights of paths \(i\) and \(j\) is preserved. Hence the total weight \(w(\mathbf{p}) = \prod _l w(p_l)\) is unchanged.

The permutation component changes by a non-trivial transposition, so it cannot equal \(\sigma \).

By definition: the canonical intersection data selects indices \(i\) and \(j\), and \(\varphi \) composes \(\sigma \) with the transposition \((i\; j)\).

By definition: \(\varphi \) selects the canonical intersection data \((i, j, v)\) and exchanges the tails of paths \(i\) and \(j\) at \(v\), leaving all other paths untouched.

Apply the sign-reversing involution \(\varphi \) as a fixed-point-free involution. Each pair \(\{ (\sigma , \mathbf{p}),\; \varphi (\sigma , \mathbf{p})\} \) contributes \((-1)^\sigma w(\mathbf{p}) + (-(-1)^\sigma ) w(\mathbf{p}) = 0\).

Expand \(\det (M)\) by the Leibniz formula. Each summand \((-1)^\sigma \prod _i M_{i,\sigma (i)}\) expands (using the definition \(M_{i,j} = \sum _{p : A_i \to B_j} w(p)\) and distributivity) into a sum over all path tuples from \(\mathbf{A}\) to \(\sigma (\mathbf{B})\). Combine over all \(\sigma \) to obtain the sum over all pairs \((\sigma , \mathbf{p})\).

Decompose the set of non-intersecting path tuples with permutation as a disjoint union over permutations \(\sigma \) and nipats from \(\mathbf{A}\) to \(\sigma (\mathbf{B})\), then factor out \((-1)^\sigma \) from each inner sum.

Expand the finite product of finite sums using distributivity. The resulting index set bijects with all path tuples (choosing one path for each component).

By induction on \(b - a\). If \(f(a) = 0\), take \(c = a\). Otherwise, \(f(a) {\gt} 0\) and the step bound gives \(f(a+1) \ge 0\). If \(f(a+1) \le 0\), take \(c = a + 1\); otherwise apply the induction hypothesis to \([a+1, b]\).

Consider the “coordinate sum” \(s = x + y\) along each path. The range of \(s\)-values for \(p\) is \([A_x + A_y,\; B'_x + B'_y]\), and for \(p'\) it is \([A'_x + A'_y,\; B_x + B_y]\). These ranges overlap. At the low end of the overlap, the \(x\)-coordinate of \(p\) is \(\ge \) that of \(p'\); at the high end, it is \(\le \). Since the \(x\)-coordinate changes by at most \(1\) per step, a discrete intermediate value argument (Lemma 5.171) yields a value of \(s\) where \(p\) and \(p'\) have the same \(x\)-coordinate. Since they also have the same coordinate sum \(s\), the \(y\)-coordinates agree as well, so they share that vertex.

By strong induction. If \(\sigma \) is monotone, then for the smallest element \(i\) we have \(\sigma (i) \ge i\) (otherwise injectivity is violated) and \(\sigma (i) \le i\) (otherwise the preimage of \(i\) would have to be smaller, violating monotonicity). Hence \(\sigma (i) = i\), and the claim follows by induction.

Since \(\sigma \ne \operatorname {id}\), by Lemma 5.173 there exists \(i \in [k-1]\) with \(\sigma (i) {\gt} \sigma (i+1)\). The sorting conditions then satisfy the hypotheses of Lemma 5.172 for paths \(p_i : A_i \to B_{\sigma (i+1)}\) and \(p_{i+1} : A_{i+1} \to B_{\sigma (i)}\), so these two paths must intersect. Hence no nipat exists.

Let \(\sigma \in S_k\) be a permutation that is not the identity permutation \(\operatorname {id} \in S_k\). By Lemma 5.174, there are no nipats from \(\mathbf{A}\) to \(\sigma (\mathbf{B})\), so

Now, Theorem 5.154 yields

By induction on \(c - d\). The base case \(c = d\) is trivial. For the inductive step, use the identity \(\binom {n}{m+1}(m+1) = \binom {n}{m}(n - m)\) to reduce the \((c+1)\) case to the \(c\) case, together with the inequality \(b - m \le a - m\) (from \(b \le a\)).

A path from \((0,-a)\) to \((b,-b)\) has exactly \(a\) steps (the coordinate sum \(x+y\) increases from \(-a\) to \(0\)), of which exactly \(b\) are east-steps (the \(x\)-coordinate increases from \(0\) to \(b\)). Choosing which \(b\) of the \(a\) steps are east-steps gives a bijection with \(b\)-element subsets of \([a]\), so the count is \(\binom {a}{b}\).

A path is uniquely determined by the positions of its east-steps among all \(a\) steps. This gives a bijection to \(b\)-element subsets of \(\{ 1, \ldots , a\} \).

The \((i,j)\) entry of the path weight matrix (with unit weights) is the number of paths from \(A_i\) to \(B_j\), which by Lemma 5.177 equals \(\binom {a_i}{b_j}\).

This is the specialization of the signed ipat cancellation (Lemma 5.167) to unit weights, where the weight of each path tuple is \(1\) and the sum reduces to a signed cardinality count.

Set \(K = \mathbb {Z}\) and \(w(a) := 1\) for each arc \(a\) of \(\mathbb {Z}^2\). Define the lattice points

for all \(i \in [k]\). These lattice points satisfy the assumptions of Corollary 5.175. Hence, 20 entails

Using Proposition 5.129, the matrix on the left hand side is \(\bigl(\binom {a_i}{b_j}\bigr)_{1 \le i \le k,\; 1 \le j \le k}\). The right hand side is \(\ge 0\), so the determinant is \(\ge 0\).

In Lean, the cases \(k = 0\) and \(k = 1\) are proved directly (empty and \(1\times 1\) determinants), \(k = 2\) uses the FKG inequality (Lemma 5.176), and \(k \ge 3\) uses the full LGV machinery.

Every arc increases the first coordinate by \(1\), so any path is strictly increasing in the first coordinate. Hence there can be no cycle.

Since the first coordinate increases by exactly \(1\) on each arc, a path of length \(n\) visits vertices whose first coordinates form a consecutive sequence. The second coordinate is bounded by the first coordinate difference, so there are only finitely many possible vertex sequences.

A path from \((0,0)\) to \((2n, 0)\) in the Dyck digraph consists of \(2n\) steps, each going either up-right or down-right, and never going below the \(x\)-axis. Such a path is exactly a Dyck path of semilength \(n\). The bijection with Dyck words (Lemma 5.185) establishes the correspondence with the Catalan number.

The forward map sends each arc \((x, y) \to (x+1, y+1)\) to an up-step and each arc \((x, y) \to (x+1, y-1)\) to a down-step, verifying that the resulting list of steps forms a well-formed Dyck word. The backward map constructs vertices by scanning the Dyck word and accumulating \(y\)-coordinates. Round-trip equalities (the two maps are mutual inverses) are verified by induction on the step list.

By translation invariance (Lemma 5.187), the set of paths from \((-2i, 0)\) to \((2j, 0)\) bijects with paths from \((0, 0)\) to \((2(i+j), 0)\), which has cardinality \(c_{i+j}\) by Lemma 5.184.

Each arc \((x, y) \to (x+1, y \pm 1)\) is preserved by horizontal translation, so the translated vertex list forms a valid path. Injectivity follows from injectivity of the translation map on vertices. Surjectivity follows from the inverse translation.

The \((i,j)\) entry of the path weight matrix (with unit weights) counts paths from \((-2i, 0)\) to \((2j, 0)\), which equals \(c_{i+j}\) by Lemma 5.186.

The vertex list is constructed explicitly. The start and finish are verified by evaluating the vertex list at positions \(0\) and \(4i\). Each consecutive pair of vertices forms a valid Dyck arc (either up-right or down-right, with \(y \ge 0\)).

A vertex on \(\gamma _i\) at position \(m\) has \(y = \min (m, 4i - m)\). At any shared \(x\)-coordinate, the corresponding positions yield different \(y\)-coordinates when \(i \ne j\), because the maximum height \(2i\) differs.

By induction on \(m\). Each arc changes \(y\) by \(\pm 1\), flipping the parity.

Each step changes \(y\) by at most \(+1\), so \(y_m \le m\). Symmetrically, \(y\) must return to \(0\) in \(4i - m\) remaining steps, so \(y_m \le 4i - m\).

Existence and non-intersection: The nested Dyck path for index \(i\) visits only vertices \((x, y)\) with \(|x| \le 2i\) and \(y \le 2i\), and at the midpoint \(x = 0\) it reaches height exactly \(2i\). Two nested paths for indices \(i \ne j\) are disjoint because they reach different maximum heights (Lemma 5.190).

Uniqueness: Any nipat must equal the nested one. At the midpoint of path \(i\) (step \(2i\)), the \(y\)-coordinate must be exactly \(2i\): it is at most \(2i\) (by Lemma 5.192), has the correct parity (by Lemma 5.191), and cannot equal \(2m\) for any \(m {\lt} i\) because that would force a shared vertex with the (inductively determined) path \(m\). Once the midpoint heights are fixed, the entire path is forced (it must go straight up, then straight down) by parity and the non-intersection constraint.

For \(k \ge 2\), the full proof uses strong induction on the path index.

We use not the lattice \(\mathbb {Z}^2\), but a different digraph: the simple digraph with vertex set \(\mathbb {Z} \times \mathbb {N}\) and arcs \((i,j) \to (i+1, j+1)\) for all \((i,j) \in \mathbb {Z} \times \mathbb {N}\) and \((i,j) \to (i+1, j-1)\) for all \((i,j) \in \mathbb {Z} \times \mathbb {P}\). It is easy to see that this digraph is acyclic and path-finite.

Set \(K = \mathbb {Z}\) and \(w(a) = 1\) for each arc \(a\). Define \(A_i := (-2(i-1), 0)\) and \(B_i := (2(i-1), 0)\) for \(i \in [k]\).

The Catalan number \(c_n\) counts the paths from \((0,0)\) to \((2n,0)\) on this digraph (Dyck paths). Hence \(c_n\) also counts the paths from \((i,0)\) to \((2n+i, 0)\) for any \(i \in \mathbb {N}\). By Lemma 5.184, the number of paths from \(A_i\) to \(B_j\) is \(c_{i+j-2}\). Hence the path weight matrix is the Catalan Hankel matrix (Lemma 5.188).

It is not hard to show (Lemma 5.193) that there is only one nipat from \(\mathbf{A}\) to \(\mathbf{B}\). Moreover, there are no nipats from \(\mathbf{A}\) to \(\sigma (\mathbf{B})\) for \(\sigma \ne \operatorname {id}\) (by an argument analogous to Corollary 5.175). Hence, by Theorem 5.155, the determinant equals \(1\).

The forward map is injective (Lemma 5.196) and surjective (Lemma 5.197), establishing the equivalence.

By induction on the path length. If two step sequences produce the same vertex list, the second vertices must agree. Since each step (east or north) produces a distinct target from the same source, the first steps must be equal. Apply the induction hypothesis to the tails.

Convert the path’s vertex list to a step list by recovering each step from consecutive vertex pairs: if the \(x\)-coordinate increases by \(1\), the step is east; otherwise it is north. The round-trip identity follows by construction.

Both representations check whether any two paths share a vertex. Since the step-to-vertex map preserves the vertex list, a vertex \(v\) appears in two step-based paths if and only if it appears in the corresponding vertex-based paths.