LemmaStatement: Literature-sourcedProof: AI-generatedPipeline-generatedprecheck passjudge pass (gpt-5.6-terra)audited 2026-09-06

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.

A reachable-vertex count is verifiable in NL

Statement

Given the true count $c = ∣ C_{i} (G, s) ∣$ , there is a nondeterministic $O (\log N)$ -work-space verifier that accepts a certificate exactly when $v \notin C_{i} (G, s)$ . The certificate lists all $c$ reachable vertices in strictly increasing order, each with a walk from $s$ of length at most $i$ .

Facts & Assumptions

Given: an $N$ -vertex digraph, $s$ , $i \leq N - 1$ , the true count $c = ∣ C_{i} (G, s) ∣$ , and a vertex $v$ .

[L1]

$C_{i}$ consists of precisely the vertices with an $s$ -to-vertex walk of length at most $i$ (Inductive counts of reachable vertices).

Proof

technique · positive certificate and counting

1.1

Guess, in strictly increasing vertex-label order, $c$ distinct vertices different from $v$ , together with for each an $s$ -to-that-vertex walk of length at most $i$ . Check each edge and count the listed vertices.

givenconstruct

2.1

The current vertex, previous path vertex, path-length counter, list counter, and labels use $O (\log N)$ space. Thus this is an NL verifier.

step 1.1algebra

3.1

If it accepts, [L1] puts all $c$ listed vertices in $C_{i}$ . The given equality $c = ∣ C_{i} ∣$ makes this list exhaust $C_{i}$ , so $v \notin C_{i}$ . Conversely, when $v \notin C_{i}$ , list every member of $C_{i}$ with a witnessing bounded walk; the list has exactly the given length $c$ , and the verifier accepts.

L1step 1.1cases∎

Depends on

Used by

Nonreachability has an inductive counting certificate Lemma

Dependency tree · two levels

7 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

Arora and Barak, Computational Complexity, §3.4.2 (standard reference, not scraped)