The counting principle behind inductive counting

⚠️ Unreviewed by Bolton

Immerman–Szelepcsényi's machine cannot store a round of the breadth-first search — that would take polynomially many bits, not logarithmically many. It stores only the round's size, and recovers everything else by guessing. The reason that is sound is a counting principle: a subset of a round that is at least as large as the round is the whole round. So a machine that has verified r_i distinct members of round i, and has not seen c among them, may conclude that c is not in round i — which is a negative fact, certified positively.

This file isolates that principle and the round recursion it is applied to. Neither mentions a machine: what remains for NL ⊆ coNL is the guessing procedure and its space accounting.

Main results

• NTM.reachCodes_mono — the rounds only grow
• NTM.eq_reachCodes_of_card_le — the counting certificate
• NTM.not_mem_reachCodes_of_card_le — non-membership certified by a count
• NTM.mem_reachCodes_succ_iff — the round recursion the count is carried along
• NTM.not_mem_iff_forall_not_accepting — the complement characterization coNL needs
• NTM.reachSet_eq_of_ncard_le — the counting certificate for the specification-level rounds
• NL_complement_characterization_internal — the complement of an NL language, as a universally quantified statement over the rounds of the search
• mem_NL_of_logWindow — an explicit logarithmic window suffices for NL
• NL_subset_coNL_of_counting_internal — the containment, modulo one machine

The rounds as growing finite sets

theorem Complexity.NTM.mem_reachCodes_succ_iff {k : ℕ} {tm : NTM k} {x : List Bool} {S : ℕ} (a₀ : Code tm.Q k x.length S) (i : ℕ) (a : Code tm.Q k x.length S) : a ∈ tm.reachCodes x S a₀ (i + 1) ↔ a ∈ tm.reachCodes x S a₀ i ∨ ∃ b ∈ tm.reachCodes x S a₀ i, a ∈ tm.codeSucc x S b

The round recursion, as a membership statement: a code is in the next round exactly when it is already present or is a successor of something present.

theorem Complexity.NTM.reachCodes_subset_succ {k : ℕ} {tm : NTM k} {x : List Bool} {S : ℕ} (a₀ : Code tm.Q k x.length S) (i : ℕ) : tm.reachCodes x S a₀ i ⊆ tm.reachCodes x S a₀ (i + 1)

Each round contains the previous one.

theorem Complexity.NTM.reachCodes_mono {k : ℕ} {tm : NTM k} {x : List Bool} {S : ℕ} (a₀ : Code tm.Q k x.length S) {i j : ℕ} (hij : i ≤ j) : tm.reachCodes x S a₀ i ⊆ tm.reachCodes x S a₀ j

The rounds only grow.

The counting certificate

theorem Complexity.NTM.eq_reachCodes_of_card_le {k : ℕ} {tm : NTM k} {x : List Bool} {S : ℕ} {a₀ : Code tm.Q k x.length S} {i : ℕ} {T : Finset (Code tm.Q k x.length S)} (hsub : T ⊆ tm.reachCodes x S a₀ i) (hcard : (tm.reachCodes x S a₀ i).card ≤ T.card) : T = tm.reachCodes x S a₀ i

The counting certificate. A subset of a round that is at least as large as the round is the whole round. This is what lets a machine that knows only the round's size conclude a negative fact from a successful count.

theorem Complexity.NTM.not_mem_reachCodes_of_card_le {k : ℕ} {tm : NTM k} {x : List Bool} {S : ℕ} {a₀ : Code tm.Q k x.length S} {i : ℕ} {T : Finset (Code tm.Q k x.length S)} (hsub : T ⊆ tm.reachCodes x S a₀ i) (hcard : (tm.reachCodes x S a₀ i).card ≤ T.card) {a : Code tm.Q k x.length S} (ha : a ∉ T) : a ∉ tm.reachCodes x S a₀ i

Non-membership certified by a count. Having verified as many members of round i as the round has, a code not among them is not in the round at all.

theorem Complexity.NTM.card_le_card_reachCodes {k : ℕ} {tm : NTM k} {x : List Bool} {S : ℕ} {a₀ : Code tm.Q k x.length S} {i : ℕ} {T : Finset (Code tm.Q k x.length S)} (hsub : T ⊆ tm.reachCodes x S a₀ i) : T.card ≤ (tm.reachCodes x S a₀ i).card

Conversely, a verified subset can never exceed the round it sits inside, so the count a machine accumulates is bounded by the true one.

theorem Complexity.NTM.reachSet_eq_of_ncard_le {k : ℕ} (tm : NTM k) (c₀ : Cfg k tm.Q) (i : ℕ) {T : Set (Cfg k tm.Q)} (hsub : T ⊆ tm.reachSet c₀ i) (hcard : (tm.reachSet c₀ i).ncard ≤ T.ncard) : T = tm.reachSet c₀ i

The counting certificate at the level of the specification rounds: a subset of a round that is at least as large is the whole round.

The complement characterization

theorem Complexity.NTM.not_mem_iff_forall_not_accepting {k : ℕ} {tm : NTM k} {L : Language} {Sf : ℕ → ℕ} (hdec : tm.DecidesInSpace L Sf) (x : List Bool) {N : ℕ} (hN : Fintype.card (Code tm.Q k x.length (Sf x.length)) ≤ N) : x ∉ L ↔ ∀ a ∈ tm.reachCodes x (Sf x.length) (cfgCode x.length (Sf x.length) (tm.initCfg x)) N, ¬((decodeCfg x (Sf x.length) a).state = tm.qhalt ∧ (decodeCfg x (Sf x.length) a).output.cells 1 = Γ.one)

What coNL has to certify. An input is outside the language exactly when no reachable configuration of the search is an accepting halted one — a universally quantified statement over a finite set, which is what inductive counting turns into a nondeterministic verification.

theorem Complexity.NL_complement_characterization_internal {L : Language} (hL : L ∈ NL) : ∃ (k : ℕ) (tm : NTM k) (A : ℕ) (B : ℕ), ∀ (x : List Bool), x ∉ L ↔ ∀ c ∈ tm.reachSet (tm.initCfg x) (A * (x.length + 1) ^ B), ¬(tm.halted c ∧ c.output.cells 1 = Γ.one)

The complement of an NL language, spelled out. An input is outside the language exactly when every configuration the bounded search reaches fails to be accepting. This is the universally quantified statement inductive counting has to certify nondeterministically.

theorem Complexity.mem_NL_of_logWindow {L : Language} {k : ℕ} (tm : NTM k) (C D : ℕ) (htrans : tm.IsTransducer) (hdec : tm.DecidesInSpace L (logWindow C D)) : L ∈ NL

A nondeterministic transducer respecting an explicit logarithmic window decides an NL language: the O(log n) side is discharged once, here.

theorem Complexity.NL_subset_coNL_of_counting_internal (h : ∀ (k : ℕ) (tm : NTM k) (S : ℕ → ℕ) (L₀ : Language) (A B : ℕ), tm.DecidesInSpace L₀ S → (BigO S fun (n : ℕ) => Nat.log 2 n) → ∃ (k' : ℕ) (M : NTM k') (C : ℕ) (D : ℕ), M.IsTransducer ∧ M.DecidesInSpace {x : List Bool | ∀ c ∈ tm.reachSet (tm.initCfg x) (A * (x.length + 1) ^ B), ¬(tm.halted c ∧ c.output.cells 1 = Γ.one)} (logWindow C D)) : NL ⊆ coNL

NL ⊆ coNL, reduced to the existence of one machine. The hypothesis carries the log-space witness for tm, without which the search language is not in NL at all.