LemmaStatement: Literature-sourcedProof: AI-generatedprecheck pass

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

The bounded reachability recursion is correct

Statement

Let $G = (V, A)$ be a finite digraph, let $u, v \in V$ , and let $i \in N$ . Then ${Reach}_{i}^{G} (u, v)$ holds if and only if $G$ contains a directed path from $u$ to $v$ of length at most $2^{i}$ .

Facts & Assumptions

Given: a finite digraph $G = (V, A)$ , vertices $u, v \in V$ , and a natural number $i$ .

[L1]

The definition of ${Reach}_{0}^{G} (u, v)$ says exactly that $u = v$ or $(u, v) \in A$ , and the definition of ${Reach}_{i}^{G}$ for $i \geq 1$ says that some midpoint $z$ makes both ${Reach}_{i - 1}^{G} (u, z)$ and ${Reach}_{i - 1}^{G} (z, v)$ hold (The bounded reachability recursion for directed paths of length at most $2^{i}$ ).

Proof

technique · induction

1.1L1base

For $i = 0$ , [L1] says ${Reach}_{0}^{G} (u, v)$ holds exactly when $u = v$ or there is an arc $u \to v$ . These are precisely the directed paths from $u$ to $v$ of lengths $0$ and $1$ , hence of length at most $2^{0}$ .

1.2L1ihconstruct

Assume the claim for $i - 1$ with $i \geq 1$ . If ${Reach}_{i}^{G} (u, v)$ holds, [L1] gives a midpoint $z$ with ${Reach}_{i - 1}^{G} (u, z)$ and ${Reach}_{i - 1}^{G} (z, v)$ . By the induction hypothesis there are directed paths from $u$ to $z$ and from $z$ to $v$ , each of length at most $2^{i - 1}$ , and concatenating them gives a path from $u$ to $v$ of length at most $2^{i}$ .

1.3L1ihchoosealgebra

Conversely, suppose there is a directed path $u = v_{0} \to v_{1} \to \dots \to v_{ℓ} = v$ with $ℓ \leq 2^{i}$ . Put $m : = \min (2^{i - 1}, ℓ)$ and choose $z : = v_{m}$ . Then the initial segment from $u$ to $z$ has length at most $2^{i - 1}$ , and the remaining segment from $z$ to $v$ has length $ℓ - m \leq 2^{i - 1}$ . The induction hypothesis gives ${Reach}_{i - 1}^{G} (u, z)$ and ${Reach}_{i - 1}^{G} (z, v)$ , so [L1] yields ${Reach}_{i}^{G} (u, v)$ .

2.1step 1.1step 1.2step 1.3discharge-induction∎

Steps 1.1, 1.2, and 1.3 prove the equivalence for every $i$ .

Remarks

For $i \geq 1$ , the split in step 1.3 can be pictured as follows, with $m = \min (2^{i - 1}, ℓ)$ . Each arrow represents an entire directed subpath, possibly of length zero, rather than a single arc.

The labels below the subpaths follow from the induction hypothesis. If $ℓ \leq 2^{i - 1}$ , then $m = ℓ$ and $z = v$ , so the second subpath has length zero. Conversely, the two bounds give a total length at most $2^{i - 1} + 2^{i - 1} = 2^{i}$ , as in step 1.2. The proof above is independent of this illustration.

Depends on

The bounded reachability recursion for directed paths of length at most $2^i$

Used by

Dependency tree · two levels

2 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources

Eric Blais, Models of Computation, 17. Space Complexity (standard reference, not scraped)
Sanjeev Arora and Boaz Barak, Computational Complexity: A Modern Approach (standard reference, not scraped)