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.
Directed s-t connectivity is NL-complete
Statement
STCON is NL-complete under .
Facts & Assumptions
Given: an encoded digraph , or a language .
A fixed logspace machine has polynomially many configurations, and accepting branches may be made simple (Logspace machines have polynomially many configurations).
A logspace many-one reduction is a deterministic bitwise polynomial-output transduction (Logspace many-one reduction).
Proof
To decide STCON nondeterministically, retain a current vertex and a counter through moves, guessing an outgoing edge at each move and accepting on reaching . A path exists exactly when one exists with at most moves.
For , fix its machine . On input , make vertices from the valid configurations of on , add a fresh target , use legal transitions as arcs, and add an arc from every accepting configuration to .
Both stored vertex labels and the counter have bits, so step 1.1 puts STCON in NL.
By [L1], there are polynomially many configuration names of bits. A transducer enumerates candidate pairs, checks locally whether one is a legal successor of the other, and streams the encoded graph, start configuration, and using work space.
A directed path from the start to is exactly an accepting computation branch of on . Thus the transducer is an reduction, which with step 2.1 proves NL-completeness.
Depends on
Used by
Nothing in the library uses this result yet.
Dependency tree · two levels
8 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, Theorem 3.16 (standard reference, not scraped)
- Harvard CS 221, Lecture 5, Theorem 2 (standard reference, not scraped)