Nonreachability has an inductive counting certificate

Start with $c_0=1=\mathrm{\mid }{C}_0\mathrm{\mid }$.

Assume inductively that the supplied $c_{i-1}$ equals $\mathrm{\mid }{C}_{i-1}\mathrm{\mid }$. Process every vertex $u$: either verify a positive path of length at most $i$ to $u$, or, for every $w$ with $w=u$ or $(w,u)\in E$, invoke the [L2] certificate for $w\mathrm{\notin }{C}_{i-1}$. Count the vertices in the first case and require the supplied total $c_i$.

The second case is sound: if $u\in C_i$, either $u\in C_{i-1}$ (the $w=u$ test fails) or the final edge of a length-at-most-$i$ walk has a predecessor in $C_{i-1}$, contradicting one of its [L2] certificates. Conversely, every $u\mathrm{\notin }{C}_i$ is outside $C_{i-1}$ and has no in-neighbor in $C_{i-1}$, while every $u\in C_i$ has a positive bounded path. Hence an accepted layer has $c_i=\mathrm{\mid }{C}_i\mathrm{\mid }$.

Induction from step 1.1 makes every accepted layer correct. Each nested certificate is checked by counters, vertex labels, and one bounded path at a time, so the verifier retains only $O(\log N)$ work space and reads a polynomial-size certificate once. At layer $N-1$, accept precisely when $t$ is absent from the certified list; by [L1] this is equivalent to nonreachability.