Correctness of certified-row inductive counting

This is the machine-independent, space-bounded form of the Immerman--Szelepcsényi theorem. The protocol in Construction.lean streams canonical enumerations and bounded path witnesses; no complete reachable set is stored in a row.

The construction follows:

• Neil Immerman, Nondeterministic space is closed under complementation (1988).
• Róbert Szelepcsényi, The method of forced enumeration for nondeterministic automata (1988).

Context-sensitive closure under complement is only a downstream corollary obtained by presenting an LBA computation graph as a certified row system.

def CertifiedRowSystem.Complement.SourceRejects {I : Type u_1} {A : Type u_2} {C : Type u_3} {Q : Type u_4} {F : Type u_5} (S : CertifiedRowSystem I A C Q F) (input : List I) : Prop

The source system has no reachable final row from this concrete input row.

Equations

• CertifiedRowSystem.Complement.SourceRejects S input = ¬∃ (row : List A), Relation.ReflTransGen S.RowStep (List.map S.inputCell input) row ∧ S.Final row

theorem CertifiedRowSystem.Complement.sourceRejects_iff_not_mem {I : Type u_1} {A : Type u_2} {C : Type u_3} {Q : Type u_4} {F : Type u_5} (S : CertifiedRowSystem I A C Q F) {input : List I} (hne : input ≠ []) : SourceRejects S input ↔ input ∉ S.rowReachLanguage

Rejection is exactly nonmembership on a nonempty input.

def CertifiedRowSystem.Complement.ProtocolAccepts {I : Type u_1} {A : Type u_2} {Q : Type u_4} {F : Type u_5} [Fintype A] [Nonempty A] [DecidableEq A] (D : CertifiedRowSystem I A Unit Q F) (input : List I) : Prop

The integrated protocol reaches a uniformly accepting row.

Equations

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

def CertifiedRowSystem.Complement.CompiledProtocolAccepts {I : Type u_1} {A : Type u_2} {Q : Type u_4} {F : Type u_5} [Fintype A] [Nonempty A] [DecidableEq A] [Fintype Q] [Fintype F] (D : CertifiedRowSystem I A Unit Q F) (input : List I) : Prop

Reachability in the compiled protocol system, stated before replacing its certified row relation by the semantic union ProtocolStep.

Equations

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

theorem CertifiedRowSystem.Complement.mem_deterministicComplementSystem_iff {I : Type u_1} {A : Type u_2} {Q : Type u_4} {F : Type u_5} [Fintype A] [Nonempty A] [DecidableEq A] [Fintype Q] [Fintype F] (D : CertifiedRowSystem I A Unit Q F) (input : List I) : input ∈ (deterministicComplementSystem D).rowReachLanguage ↔ input ≠ [] ∧ CompiledProtocolAccepts D input

Membership in the constructed row language is compiled protocol acceptance together with the model's intrinsic nonempty-input condition.