Finite reachability by inductive counting

This file isolates the finite-graph correctness argument behind the Immerman--Szelepcsényi theorem. For a finite directed graph, reached edge source k is the set of vertices reachable in at most k steps. It stabilizes after at most Fintype.card V rounds and then agrees with reflexive-transitive reachability.

Enumeration, Round, CertifiedCount, and Rejection describe an inductive-counting certificate for nonreachability. Their Finset fields are mathematical transcripts of canonical scans through Finset.univ; they need not be stored by an implementation. A space-bounded verifier can stream a scan while retaining only the current vertex, a path certificate, and counters bounded by Fintype.card V.

The final correctness result is nonreachable_iff_counting_certificate.

def FiniteReachabilityCounting.grow {V : Type u_1} [Fintype V] [DecidableEq V] (edge : V → V → Prop) [DecidableRel edge] (S : Finset V) : Finset V

Add every one-step successor of a finite set.

Equations

• FiniteReachabilityCounting.grow edge S = S ∪ {v : V | ∃ u ∈ S, edge u v}

theorem FiniteReachabilityCounting.mem_grow {V : Type u_1} [Fintype V] [DecidableEq V] (edge : V → V → Prop) [DecidableRel edge] {S : Finset V} {v : V} : v ∈ grow edge S ↔ v ∈ S ∨ ∃ u ∈ S, edge u v

Membership in grow is old membership or a one-step successor of an old vertex.

theorem FiniteReachabilityCounting.subset_grow {V : Type u_1} [Fintype V] [DecidableEq V] (edge : V → V → Prop) [DecidableRel edge] (S : Finset V) : S ⊆ grow edge S

theorem FiniteReachabilityCounting.grow_mono {V : Type u_1} [Fintype V] [DecidableEq V] (edge : V → V → Prop) [DecidableRel edge] {S T : Finset V} (hST : S ⊆ T) : grow edge S ⊆ grow edge T

def FiniteReachabilityCounting.reached {V : Type u_1} [Fintype V] [DecidableEq V] (edge : V → V → Prop) [DecidableRel edge] (source : V) : ℕ → Finset V

The vertices reachable from source in at most k directed steps.

Equations

• FiniteReachabilityCounting.reached edge source 0 = {source}
• FiniteReachabilityCounting.reached edge source k.succ = FiniteReachabilityCounting.grow edge (FiniteReachabilityCounting.reached edge source k)

@[simp]

theorem FiniteReachabilityCounting.reached_zero {V : Type u_1} [Fintype V] [DecidableEq V] (edge : V → V → Prop) [DecidableRel edge] (source : V) : reached edge source 0 = {source}

@[simp]

theorem FiniteReachabilityCounting.reached_succ {V : Type u_1} [Fintype V] [DecidableEq V] (edge : V → V → Prop) [DecidableRel edge] (source : V) (k : ℕ) : reached edge source (k + 1) = grow edge (reached edge source k)

theorem FiniteReachabilityCounting.reached_mono {V : Type u_1} [Fintype V] [DecidableEq V] (edge : V → V → Prop) [DecidableRel edge] (source : V) (k : ℕ) : reached edge source k ⊆ reached edge source (k + 1)

theorem FiniteReachabilityCounting.reached_mono_nat {V : Type u_1} [Fintype V] [DecidableEq V] (edge : V → V → Prop) [DecidableRel edge] (source : V) {i j : ℕ} (hij : i ≤ j) : reached edge source i ⊆ reached edge source j

inductive FiniteReachabilityCounting.PaddedPath {V : Type u_1} (edge : V → V → Prop) (source : V) : ℕ → V → Prop

An exactly fuel-indexed path in the reflexive closure of edge. Stuttering allows a path of at most k genuine edges to be padded to exactly k verifier steps without changing its endpoint.

• zero {V : Type u_1} {edge : V → V → Prop} {source : V} : PaddedPath edge source 0 source
• succ {V : Type u_1} {edge : V → V → Prop} {source : V} {k : ℕ} {old new : V} : PaddedPath edge source k old → old = new ∨ edge old new → PaddedPath edge source (k + 1) new

theorem FiniteReachabilityCounting.mem_reached_iff_paddedPath {V : Type u_1} [Fintype V] [DecidableEq V] (edge : V → V → Prop) [DecidableRel edge] (source : V) {k : ℕ} {v : V} : v ∈ reached edge source k ↔ PaddedPath edge source k v

Bounded reachability is exactly existence of a fuel-indexed padded path.

theorem FiniteReachabilityCounting.reached_sound {V : Type u_1} [Fintype V] [DecidableEq V] (edge : V → V → Prop) [DecidableRel edge] (source : V) {k : ℕ} {v : V} (hv : v ∈ reached edge source k) : Relation.ReflTransGen edge source v

Every bounded-reachable vertex is reachable in the ordinary relational sense.

theorem FiniteReachabilityCounting.reached_eq_of_plateau {V : Type u_1} [Fintype V] [DecidableEq V] (edge : V → V → Prop) [DecidableRel edge] (source : V) {k : ℕ} (h : reached edge source k = reached edge source (k + 1)) (m : ℕ) : reached edge source (k + m) = reached edge source k

Once a reachability round adds no vertex, every later round is identical.

theorem FiniteReachabilityCounting.no_earlier_plateau {V : Type u_1} [Fintype V] [DecidableEq V] (edge : V → V → Prop) [DecidableRel edge] (source : V) {n k : ℕ} (hkn : k ≤ n) (hn : reached edge source n ≠ reached edge source (n + 1)) : reached edge source k ≠ reached edge source (k + 1)

If round n has not stabilized, no earlier round has stabilized.

theorem FiniteReachabilityCounting.card_reached_lower_of_nonplateau {V : Type u_1} [Fintype V] [DecidableEq V] (edge : V → V → Prop) [DecidableRel edge] (source : V) {n : ℕ} (hn : reached edge source n ≠ reached edge source (n + 1)) : n + 1 ≤ (reached edge source n).card

theorem FiniteReachabilityCounting.reached_card_fixed {V : Type u_1} [Fintype V] [DecidableEq V] (edge : V → V → Prop) [DecidableRel edge] (source : V) : reached edge source (Fintype.card V) = reached edge source (Fintype.card V + 1)

Finite reachability has stabilized after Fintype.card V rounds.

theorem FiniteReachabilityCounting.mem_reached_card_iff {V : Type u_1} [Fintype V] [DecidableEq V] (edge : V → V → Prop) [DecidableRel edge] (source : V) {v : V} : v ∈ reached edge source (Fintype.card V) ↔ Relation.ReflTransGen edge source v

Saturated bounded reachability is exactly reflexive-transitive reachability.

structure FiniteReachabilityCounting.Enumeration {V : Type u_1} [Fintype V] [DecidableEq V] (edge : V → V → Prop) [DecidableRel edge] (source : V) (k c : ℕ) : Type u_1

A transcript of vertices for which a canonical scan guessed reachability witnesses.

The fixed scan order means an implementation does not need a duplicate table.

• vertices : Finset V
• card_eq : self.vertices.card = c
• sound {v : V} : v ∈ self.vertices → v ∈ reached edge source k

theorem FiniteReachabilityCounting.Enumeration.eq_reached {V : Type u_1} [Fintype V] [DecidableEq V] (edge : V → V → Prop) [DecidableRel edge] (source : V) {k c : ℕ} (hc : c = (reached edge source k).card) (E : Enumeration edge source k c) : E.vertices = reached edge source k

A sound enumeration of the exact expected cardinality contains every reachable vertex.

structure FiniteReachabilityCounting.Round {V : Type u_1} [Fintype V] [DecidableEq V] (edge : V → V → Prop) [DecidableRel edge] (source : V) (k c d : ℕ) : Type u_1

One complete inductive-counting round.

old records successful old-reachability guesses. new records the vertices declared reachable in the next round; positive and negative validate both outcomes of the scan.

• old : Enumeration edge source k c
• new : Finset V
• new_card : self.new.card = d
• positive {v : V} : v ∈ self.new → v ∈ self.old.vertices ∨ ∃ u ∈ self.old.vertices, edge u v
• negative {v : V} : v ∉ self.new → v ∉ self.old.vertices ∧ ∀ u ∈ self.old.vertices, ¬edge u v

theorem FiniteReachabilityCounting.Round.correct {V : Type u_1} [Fintype V] [DecidableEq V] (edge : V → V → Prop) [DecidableRel edge] (source : V) {k c d : ℕ} (hc : c = (reached edge source k).card) (R : Round edge source k c d) : d = (reached edge source (k + 1)).card

If the input count to a round is exact, so is its output count.

theorem FiniteReachabilityCounting.Round.reached_eq_succ_of_count_eq {V : Type u_1} [Fintype V] [DecidableEq V] (edge : V → V → Prop) [DecidableRel edge] (source : V) {k c d : ℕ} (hc : c = (reached edge source k).card) (R : Round edge source k c d) (hdc : d = c) : reached edge source k = reached edge source (k + 1)

If an exact counting round leaves the count unchanged, bounded reachability has reached a fixed point. This is the plateau test used by the streaming Immerman--Szelepcsényi verifier.

theorem FiniteReachabilityCounting.Round.reached_eq_add_of_count_eq {V : Type u_1} [Fintype V] [DecidableEq V] (edge : V → V → Prop) [DecidableRel edge] (source : V) {k c d : ℕ} (hc : c = (reached edge source k).card) (R : Round edge source k c d) (hdc : d = c) (m : ℕ) : reached edge source (k + m) = reached edge source k

After a count plateau, every later bounded-reachability layer is the same layer.

theorem FiniteReachabilityCounting.Round.mem_reached_iff_of_count_eq {V : Type u_1} [Fintype V] [DecidableEq V] (edge : V → V → Prop) [DecidableRel edge] (source : V) {k c d : ℕ} (hc : c = (reached edge source k).card) (R : Round edge source k c d) (hdc : d = c) {v : V} : v ∈ reached edge source k ↔ Relation.ReflTransGen edge source v

A plateau layer is the full reflexive-transitive reachable set, not merely a bounded approximation.

theorem FiniteReachabilityCounting.Round.count_lt_of_ne {V : Type u_1} [Fintype V] [DecidableEq V] (edge : V → V → Prop) [DecidableRel edge] (source : V) {k c d : ℕ} (hc : c = (reached edge source k).card) (R : Round edge source k c d) (hne : d ≠ c) : c < d

A non-plateau exact round strictly increases the reachable count.

theorem FiniteReachabilityCounting.Round.depth_lt_card_of_ne {V : Type u_1} [Fintype V] [DecidableEq V] (edge : V → V → Prop) [DecidableRel edge] (source : V) {k c d : ℕ} (hc : c = (reached edge source k).card) (R : Round edge source k c d) (hne : d ≠ c) : k < Fintype.card V

A non-plateau round occurs before the number of vertices. Thus a width-n row counter needs only enough values for the |V| possible strict-growth rounds.

inductive FiniteReachabilityCounting.CertifiedCount {V : Type u_1} [Fintype V] [DecidableEq V] (edge : V → V → Prop) [DecidableRel edge] (source : V) : ℕ → ℕ → Prop

A sequence of locally verified counting rounds, starting with the singleton source.

• zero {V : Type u_1} [Fintype V] [DecidableEq V] {edge : V → V → Prop} [DecidableRel edge] {source : V} : CertifiedCount edge source 0 1
• succ {V : Type u_1} [Fintype V] [DecidableEq V] {edge : V → V → Prop} [DecidableRel edge] {source : V} {k c d : ℕ} : CertifiedCount edge source k c → ∀ (a✝ : Round edge source k c d), CertifiedCount edge source (k + 1) d

theorem FiniteReachabilityCounting.certifiedCount_sound {V : Type u_1} [Fintype V] [DecidableEq V] (edge : V → V → Prop) [DecidableRel edge] (source : V) {k c : ℕ} (h : CertifiedCount edge source k c) : c = (reached edge source k).card

Every certified count is the true bounded-reachability count.

def FiniteReachabilityCounting.canonicalEnumeration {V : Type u_1} [Fintype V] [DecidableEq V] (edge : V → V → Prop) [DecidableRel edge] (source : V) (k : ℕ) : Enumeration edge source k (reached edge source k).card

The canonical transcript enumerating exactly the bounded-reachable vertices.

Equations

• FiniteReachabilityCounting.canonicalEnumeration edge source k = { vertices := FiniteReachabilityCounting.reached edge source k, card_eq := ⋯, sound := ⋯ }

def FiniteReachabilityCounting.canonicalRound {V : Type u_1} [Fintype V] [DecidableEq V] (edge : V → V → Prop) [DecidableRel edge] (source : V) (k : ℕ) : Round edge source k (reached edge source k).card (reached edge source (k + 1)).card

The canonical transcript for one counting round.

Equations

• One or more equations did not get rendered due to their size.

theorem FiniteReachabilityCounting.certifiedCount_complete {V : Type u_1} [Fintype V] [DecidableEq V] (edge : V → V → Prop) [DecidableRel edge] (source : V) (k : ℕ) : CertifiedCount edge source k (reached edge source k).card

Exact bounded-reachability counts always have a certificate.

theorem FiniteReachabilityCounting.certifiedCount_iff {V : Type u_1} [Fintype V] [DecidableEq V] (edge : V → V → Prop) [DecidableRel edge] (source : V) {k c : ℕ} : CertifiedCount edge source k c ↔ c = (reached edge source k).card

Certified counts are precisely the true bounded-reachability counts.

structure FiniteReachabilityCounting.Rejection {V : Type u_1} [Fintype V] [DecidableEq V] (edge : V → V → Prop) [DecidableRel edge] (source : V) (k c : ℕ) (target : V) : Type u_1

A final scan transcript claiming that target is absent.

• seen : Enumeration edge source k c
• target_absent : target ∉ self.seen.vertices

theorem FiniteReachabilityCounting.Rejection.correct {V : Type u_1} [Fintype V] [DecidableEq V] (edge : V → V → Prop) [DecidableRel edge] (source : V) {k c : ℕ} {target : V} (hc : c = (reached edge source k).card) (R : Rejection edge source k c target) : target ∉ reached edge source k

A rejection backed by the exact count proves bounded nonreachability.

def FiniteReachabilityCounting.canonicalRejection {V : Type u_1} [Fintype V] [DecidableEq V] (edge : V → V → Prop) [DecidableRel edge] (source : V) {k : ℕ} {target : V} (h : target ∉ reached edge source k) : Rejection edge source k (reached edge source k).card target

The canonical rejection transcript for an absent target.

Equations

• FiniteReachabilityCounting.canonicalRejection edge source h = { seen := FiniteReachabilityCounting.canonicalEnumeration edge source k, target_absent := h }

structure FiniteReachabilityCounting.FinalRejection {V : Type u_1} [Fintype V] [DecidableEq V] (edge : V → V → Prop) [DecidableRel edge] (source : V) (k c : ℕ) (final : V → Prop) : Type u_1

A final scan transcript claiming that every bounded-reachable vertex is nonfinal.

• seen : Enumeration edge source k c
• all_nonfinal {v : V} : v ∈ self.seen.vertices → ¬final v

theorem FiniteReachabilityCounting.FinalRejection.correct {V : Type u_1} [Fintype V] [DecidableEq V] (edge : V → V → Prop) [DecidableRel edge] (source : V) {k c : ℕ} {final : V → Prop} (hc : c = (reached edge source k).card) (R : FinalRejection edge source k c final) {v : V} : v ∈ reached edge source k → ¬final v

A final rejection backed by the exact count excludes every reachable final vertex.

def FiniteReachabilityCounting.canonicalFinalRejection {V : Type u_1} [Fintype V] [DecidableEq V] (edge : V → V → Prop) [DecidableRel edge] (source : V) {k : ℕ} {final : V → Prop} (h : ∀ {v : V}, v ∈ reached edge source k → ¬final v) : FinalRejection edge source k (reached edge source k).card final

The canonical final rejection transcript.

Equations

• FiniteReachabilityCounting.canonicalFinalRejection edge source h = { seen := FiniteReachabilityCounting.canonicalEnumeration edge source k, all_nonfinal := ⋯ }

theorem FiniteReachabilityCounting.nonreachable_iff_counting_certificate {V : Type u_1} [Fintype V] [DecidableEq V] (edge : V → V → Prop) [DecidableRel edge] (source : V) {target : V} : ¬Relation.ReflTransGen edge source target ↔ ∃ (c : ℕ), CertifiedCount edge source (Fintype.card V) c ∧ Nonempty (Rejection edge source (Fintype.card V) c target)

Abstract Immerman--Szelepcsényi correctness for a finite directed graph: nonreachability is equivalent to certified inductive counts followed by a rejecting scan.

theorem FiniteReachabilityCounting.no_reachable_final_iff_counting_certificate {V : Type u_1} [Fintype V] [DecidableEq V] (edge : V → V → Prop) [DecidableRel edge] (source : V) {final : V → Prop} : (¬∃ (v : V), Relation.ReflTransGen edge source v ∧ final v) ↔ ∃ (c : ℕ), CertifiedCount edge source (Fintype.card V) c ∧ Nonempty (FinalRejection edge source (Fintype.card V) c final)

No final vertex is reachable exactly when inductive counting can finish with a scan certifying that every reachable vertex is nonfinal.

theorem FiniteReachabilityCounting.immerman_szelepcsenyi {V : Type u_1} [Fintype V] [DecidableEq V] (edge : V → V → Prop) [DecidableRel edge] (source : V) {final : V → Prop} : (¬∃ (v : V), Relation.ReflTransGen edge source v ∧ final v) ↔ ∃ (c : ℕ), CertifiedCount edge source (Fintype.card V) c ∧ Nonempty (FinalRejection edge source (Fintype.card V) c final)

Finite-graph Immerman--Szelepcsényi theorem. For every finite directed graph, source vertex, and final predicate, absence of a reachable final vertex is equivalent to an inductive-counting certificate followed by an exhaustive rejecting scan. No automaton model or particular vertex type is built into the statement.