Documentation

Complexitylib.Classes.Containments.Internal.CountingCert

The certificate Immerman–Szelepcsényi's machine guesses #

⚠️ Unreviewed by Bolton

Complexitylib.Classes.Containments.Internal.InductiveCounting isolates the counting principle: a subset of a round as large as the round is the round. This file turns that principle into the shape a machine can verify, which is what stands between it and NL ⊆ coNL.

Two things have to be checkable with only logarithmically many bits in hand.

Membership in a round becomes a walk: a code lies in round i exactly when there is a sequence of i steps from the start, each of which either stays put or moves to a successor (Complexity.NTM.mem_reachCodes_iff_walk). A machine verifies such a walk holding only the current code and the step index — never the walk itself.

Non-membership becomes a round list: a list of distinct members of the round, at least as long as the round (Complexity.NTM.RoundList). A machine never holds the list either; it guesses the entries one at a time, checks each against a walk, counts them, and compares the count against the round's size. Complexity.NTM.not_mem_of_roundList is what licenses the negative conclusion, and Complexity.NTM.roundList_exists is what says an honest prover can always supply one.

Main definitions #

Main results #

Membership is a walk #

source
theorem Complexity.NTM.mem_reachCodes_iff_walk {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 ↔ ∃ (f : ℕ → Code tm.Q k x.length S), f 0 = a₀ ∧ f i = a ∧ ∀ j < i, f (j + 1) = f j ∨ f (j + 1) ∈ tm.codeSucc x S (f j)

Membership in a round is a walk. A code lies in round i exactly when some sequence of i steps from the start reaches it, each step either staying put or moving to a successor. This is the form a machine verifies: it holds only the current code and the step index.

A round as a list #

source
def Complexity.NTM.RoundList {k : ℕ} (tm : NTM k) (x : List Bool) (S : ℕ) (a₀ : Code tm.Q k x.length S) (i : ℕ) (l : List (Code tm.Q k x.length S)) :
Prop

A list that exhausts a round: distinct members, at least as many as the round has. The machine never holds such a list — it guesses the entries one at a time and counts them.

Equations
Instances For
    source
    theorem Complexity.NTM.roundList_exists {k : ℕ} (tm : NTM k) (x : List Bool) (S : ℕ) (a₀ : Code tm.Q k x.length S) (i : ℕ) :
    ∃ (l : List (Code tm.Q k x.length S)), tm.RoundList x S a₀ i l

    A round can always be listed, so an honest prover can supply the certificate.

    source
    theorem Complexity.NTM.roundList_toFinset {k : ℕ} {tm : NTM k} {x : List Bool} {S : ℕ} {a₀ : Code tm.Q k x.length S} {i : ℕ} {l : List (Code tm.Q k x.length S)} (h : tm.RoundList x S a₀ i l) :
    l.toFinset = tm.reachCodes x S a₀ i
    source
    theorem Complexity.NTM.not_mem_of_roundList {k : ℕ} {tm : NTM k} {x : List Bool} {S : ℕ} {a₀ : Code tm.Q k x.length S} {i : ℕ} {l : List (Code tm.Q k x.length S)} (h : tm.RoundList x S a₀ i l) {a : Code tm.Q k x.length S} (ha : a ∉ l) :
    a ∉ tm.reachCodes x S a₀ i

    What a round list decides, negatively. A code absent from a list that exhausts the round is not in the round — a negative fact, certified by a count.

    source
    theorem Complexity.NTM.mem_of_roundList {k : ℕ} {tm : NTM k} {x : List Bool} {S : ℕ} {a₀ : Code tm.Q k x.length S} {i : ℕ} {l : List (Code tm.Q k x.length S)} (h : tm.RoundList x S a₀ i l) {a : Code tm.Q k x.length S} (ha : a ∈ tm.reachCodes x S a₀ i) :
    a ∈ l

    And positively: every member of the round appears.

    source
    theorem Complexity.NTM.roundList_length {k : ℕ} {tm : NTM k} {x : List Bool} {S : ℕ} {a₀ : Code tm.Q k x.length S} {i : ℕ} {l : List (Code tm.Q k x.length S)} (h : tm.RoundList x S a₀ i l) :
    l.length = (tm.reachCodes x S a₀ i).card

    The list is exactly as long as the round, so the count a machine accumulates is the round's size.

    The count the machine starts from #

    source
    @[simp]
    theorem Complexity.NTM.card_reachCodes_zero {k : ℕ} (tm : NTM k) (x : List Bool) (S : ℕ) (a₀ : Code tm.Q k x.length S) :
    (tm.reachCodes x S a₀ 0).card = 1

    The complement, as a certificate #

    source
    theorem Complexity.NL_complement_certificate_internal {L : Language} (hL : L ∈ NL) :
    ∃ (k : ℕ) (tm : NTM k) (C : ℕ) (D : ℕ) (A : ℕ) (B : ℕ), ∀ (x : List Bool), x ∉ L ↔ ∃ (l : List (Code tm.Q k x.length (logWindow C D x.length))), tm.RoundList x (logWindow C D x.length) (cfgCode x.length (logWindow C D x.length) (tm.initCfg x)) (A * (x.length + 1) ^ B) l ∧ ∀ a ∈ l, ¬((decodeCfg x (logWindow C D x.length) a).state = tm.qhalt ∧ (decodeCfg x (logWindow C D x.length) a).output.cells 1 = Γ.one)

    The complement of an NL language is a certificate a machine can guess. An input is outside the language exactly when the last round of the search can be listed with none of its members accepting. Every quantity here is an explicit arithmetic function of the input length, and the list is only ever consumed one entry at a time: the machine guesses an entry, verifies it by a walk (Complexity.NTM.mem_reachCodes_iff_walk), checks it is not accepting, counts it, and at the end compares the count against the round's size. That comparison is what makes the absence of an accepting code a positive certificate.