Endpoint-degree bound and the square-lattice maximum

The theorem asserts the conjunction of two statements. For its notation, a grid network on $N$ vertices is an injective assignment of positions $x_i\in\mathbb Z^2$ to $V=\{0,\ldots,N-1\}$; its physical edge set $E_G$ consists of pairs $(i,j)$ with $i<j$ and Manhattan distance $1$ between their positions, and $d_G(c)$ is the number of these pairs incident to $c$. An encoded route $r$ has length $1\le m(r)\le N^2$ and vertices $(v_0,\ldots,v_{m(r)})$; it is admissible in $H$ from $a$ to $b$ when its endpoints are $a,b$, its canonical consecutive edge pairs are distinct members of $H$, and no intermediate vertex equals either endpoint. Other vertex repetitions are allowed. A feasible family is a finite set of admissible encoded routes with pairwise disjoint edge sets. First, for every natural number $N$, every such network $G$, every pair of distinct vertices $a,b$, every finite set $H\subseteq E_G$, every feasible family $F$ in $H$ from $a$ to $b$, and every Boolean assignment $\phi$ to every pair consisting of any encoded route on these $N$ vertices and one of its intermediate positions, let $D(F,\phi)$ count the routes in $F$ for which every intermediate-position flag is true. Then

The flags have no further assumptions; a length-one route has no intermediate flags and therefore satisfies the all-true condition automatically, and an empty family has delivered count $0$. The universal statement has no endpoint instances when $N=0$, and its distinct-endpoint hypothesis excludes $a=b$. Second, for every two distinct points $A,B\in\mathbb Z^2$, there exist a natural number $N$, such a network $G$, vertices $a,b$, and a finite feasible family $F$ using $E_G$, with $x_a=A$ and $x_b=B$, whose delivered count under the assignment that makes every flag true is exactly $4$; equivalently, that family contains exactly four encoded routes.