By induction on \(p_1\): applying the steps of \(p_1 \cdot p_2\) starting from \(A\) is the same as first applying the steps of \(p_1\) (reaching the endpoint of \(p_1\)) and then applying the steps of \(p_2\).

Follows from the fact that \(p\) equals its first \(n\) steps concatenated with its remaining steps, together with Lemma 5.121.

By Lemma 5.121: \(\operatorname {endpoint}(h \cdot t, A) = \operatorname {endpoint}(t, \operatorname {endpoint}(h, A)) = \operatorname {endpoint}(t, v) = B\).

By induction on \(p\): each step increases the coordinate sum by exactly \(1\).

By induction: each east-step increments the x-coordinate by \(1\), and each north-step leaves it unchanged.

If \(B\) is not componentwise \(\ge A\), the set is empty. Otherwise, every path from \(A\) to \(B\) has a bounded number of steps (exactly \(\operatorname {cs}(B) - \operatorname {cs}(A)\)), and there are finitely many lists of bounded length over the two-element set \(\{ \text{east}, \text{north}\} \).

By induction on the path: each east-step increments the x-coordinate and each north-step increments the y-coordinate.

Observation 1: We define the coordinate sum of a point \((x,y) \in \mathbb {Z}^{2}\) to be \(x+y\), denoted \(\operatorname {cs}(x,y)\). The coordinate sum increases by exactly \(1\) along each arc. If the path visits vertices \(v_0, v_1, \ldots , v_n\) with \(v_0 = (a,b)\) and \(v_n = (c,d)\), then by the telescope principle,

Observation 2: The x-coordinate of a point increases by exactly \(1\) along each east-step and stays unchanged along each north-step. By telescoping on the x-coordinate:

Observation 1 immediately shows that no path from \((a,b)\) to \((c,d)\) exists when \(c+d {\lt} a+b\) (it would need a negative number of steps), so the count is \(0\).

Otherwise, \(c + d \ge a + b\), so \(c+d-a-b \in \mathbb {N}\). Observations 1 and 2 show that every path from \((a,b)\) to \((c,d)\) has exactly \(c + d - a - b\) steps, of which exactly \(c - a\) are east-steps.

Observation 3: Let \(p\) be a path that starts at the point \((a,b)\) and has exactly \(c+d-a-b\) steps. Assume that exactly \(c-a\) of these steps are east-steps. Then, this path \(p\) ends at \((c,d)\).

(This follows by applying Observations 1 and 2 to the endpoint of \(p\) and comparing.)

Combining Observations 1, 2 and 3, the paths from \((a,b)\) to \((c,d)\) are precisely the paths that start at \((a,b)\) and have exactly \(c+d-a-b\) steps and exactly \(c-a\) east-steps. Such a path is uniquely determined by which \(c-a\) of its \(c+d-a-b\) steps are east-steps. By the bijection principle,

The set of path tuples embeds injectively into the product \(\prod _{i=1}^k \{ \text{paths from } A_i \text{ to } B_i\} \), which is finite by Lemma 5.126.

Subset of the finite set of all path tuples (Lemma 5.131).

Subset of the finite set of all path tuples (Lemma 5.131).

Immediate from the definitions: the negation of “all pairs of paths are disjoint” is equivalent to the existence of a shared vertex.

The signed path tuples inject into the product of two finite path sets times a two-element set. All three subsets are finite as subsets of this finite set.

The existence of a shared vertex guarantees that a valid index is found before the end of the vertex list.

Property (1) is by definition. Property (2) follows from the search semantics: the predicate tested is membership in \(p_1\)’s vertices. Property (3) follows from the minimality of the search: all earlier indices fail the predicate.

By Lemma 5.122, taking \(n\) steps gives a path from \(A\) to the intermediate point, and dropping \(n\) steps gives a path from that point to \(B\). The key fact is that the vertex at the split position equals \(v\), so the intermediate point is \(v\).

The new path \(q_0 = \mathrm{head}(p_0) \cdot \mathrm{tail}(p_1)\) shares the same prefix as \(p_0\) up to the split index. The value \(v\) at this index is preserved. For \(j\) less than the split index, the \(j\)-th vertex of \(q_0\) equals the \(j\)-th vertex of \(p_0\), which is not among the new \(p_1\)’s vertices (the head of old \(p_1\) is a subset of old \(p_1\)’s vertices, and the tail of old \(p_0\) cannot contain an earlier vertex because coordinate sums strictly increase). Thus the search on \(q_0\) returns the same index.

If \((p, p')\) is an ipat from \((A, A')\) to \((B, B')\), then \(f(p, p') = (q, q')\) is an ipat from \((A, A')\) to \((B', B)\) (exchanging tails swaps the endpoints), and vice versa. Thus \(f\) is well-defined and sign-reversing.

To show \(f \circ f = \operatorname {id}\): after exchanging tails, the heads are unchanged, so \(v\) is still the first intersection point (Lemma 5.141). Exchanging tails again undoes the swap.

Since \(f\) is sign-reversing, it has no fixed points.

By Lemma 4.10 applied to the sign-reversing involution of Lemma 5.142.

The first identity follows from the product rule: the product of path counts equals the count of path tuples.

The second identity is immediate from the definitions: among the nipats, those going to \((B,B')\) contribute \(+1\) each and those going to \((B',B)\) contribute \(-1\) each.

We have

(by the product rule). By Lemma 5.144, the right hand side equals \(\sum _{(p,p') \in \mathcal{A}} \operatorname {sign}(p,p')\).

By Lemma 4.10, using the sign-reversing involution of Lemma 5.142 (which uses Lemma 5.143), we obtain

The right hand side equals

by Lemma 5.144.

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

Case 3 (\(A' = A\)): Then \(A\) is a common vertex of both paths and we are done.

Case 1 (\(\operatorname {y}(A') {\gt} \operatorname {y}(A)\)): Let \(P\) be the second vertex of \(p\). Every vertex of the subpath \(r\) from \(P\) to \(B'\) is a vertex of \(p\), so \(r\) and \(p'\) have no vertex in common. Also \(\ell (r) + \ell (p') {\lt} \ell (p) + \ell (p')\). If \(\operatorname {y}(A') \ge \operatorname {y}(P)\), then we could apply the induction hypothesis to \(r\) and \(p'\), contradicting \(r \cap p' = \emptyset \). Hence \(\operatorname {y}(A') {\lt} \operatorname {y}(P)\), so \(\operatorname {y}(A') \le \operatorname {y}(P) - 1\). If the arc from \(A\) to \(P\) were an east-step, we would have \(\operatorname {y}(P) = \operatorname {y}(A)\), contradicting \(\operatorname {y}(A) \le \operatorname {y}(A') {\lt} \operatorname {y}(P)\). So the arc is a north-step, giving \(\operatorname {y}(P) = \operatorname {y}(A) + 1\), hence \(\operatorname {y}(A') \le \operatorname {y}(A)\), contradicting \(\operatorname {y}(A') {\gt} \operatorname {y}(A)\).

Case 2 (\(\operatorname {x}(A') {\lt} \operatorname {x}(A)\)): Symmetric to Case 1, looking at the first step of \(p'\) and using reflection across the line \(x = y\).

The consequence that there are no nipats from \((A, A')\) to \((B', B)\) follows immediately: if any pair of paths (one from \(A\) to \(B'\), one from \(A'\) to \(B\)) must intersect, then there can be no nipats from \((A, A')\) to \((B', B)\).

Combinatorial proof (from the source text, using LGV): Define four lattice points \(A=\left( 1,0\right) \) and \(A^{\prime }=\left( 0,1\right) \) and \(B=\left( k+1,n-k\right) \) and \(B^{\prime }=\left( k,n-k+1\right) \). Then, Proposition 5.145 yields

(Here, the second term is \(0\) by Proposition 5.146.) However, Proposition 5.129 yields

so the determinant is \(\binom {n}{k}^{2}-\binom {n}{k-1}\cdot \binom {n}{k+1}\geq 0\).

Lean formalization (algebraic proof): The Lean proof avoids the LGV machinery and proceeds purely algebraically, using the recurrences

These allow rewriting both sides after multiplying by \(k(k+1) {\gt} 0\). The inequality reduces to \((n-k+1)(k+1) \ge (n-k) \cdot k\), which holds because the difference is \(n + 1 \ge 0\). This proof is complete.

Both types are two-element enumerations with the same constructors. The equivalence and endpoint preservation follow by case analysis.

The proof constructs an equivalence between the two representations of intersecting path tuples, converting between list-of-steps and list-of-vertices representations, then verifies that the intersection property is preserved at each step.

(a) A path tuple from \(\mathbf{A}\) to \(\sigma (\mathbf{B})\) is just a tuple of independent choices (one path per index), so by the product rule the count is the product.

(b) Every path tuple is intersecting or not (classical logic); the sets are disjoint and their union is the set of all path tuples.

(c) This is the Leibniz formula \(\det (M) = \sum _\sigma (-1)^\sigma \prod _i M_{i,\sigma (i)}\).

The proof uses:

• The partition of path tuples (Lemma 5.151).

• The sign-reversing involution described above.

• Lemma 4.10 to cancel the signed sum of ipats.

• The bridge Lemma 5.150 to invoke the sign-reversing involution from the weighted LGV formalization.

Define \(\mathcal{A}:=\left\{ \left( \sigma ,\mathbf{p}\right) \ \mid \ \sigma \in S_{k}\text{, and}\ \mathbf{p}\text{ is a path tuple from }\mathbf{A}\text{ to }\sigma \left( \mathbf{B}\right) \right\} \) and \(\mathcal{X}:=\left\{ \left( \sigma ,\mathbf{p}\right) \in \mathcal{A}\ \mid \ \mathbf{p}\text{ is intersecting}\right\} \). Set \(\operatorname {sign}\left( \sigma ,\mathbf{p}\right) :=\left( -1\right) ^{\sigma }\).

By Lemma 4.10 applied to the sign-reversing involution of Lemma 5.152,

The left hand side equals

(by Lemma 5.151(a) and the definition of the determinant), and the right hand side equals