End-to-end correctness of certified-row complementation

This file combines the finite-graph counting semantics with the executable protocol. The central theorem is machine independent: for every deterministic certified row system and every nonempty encoded input, the protocol accepts exactly when the source system has no accepting run.

Soundness

theorem CertifiedRowSystem.Complement.protocolInvariant_step {I : Type u_1} {A : Type u_2} {Q : Type u_3} {F : Type u_4} [Fintype A] [Nonempty A] [DecidableEq A] {D : CertifiedRowSystem I A Unit Q F} {input : List I} {old new : ProtocolRow A} (hinput : input ≠ []) (hinv : ProtocolInvariant D input old) (hstep : ProtocolStep D old new) : ProtocolInvariant D input new

Every semantic protocol step preserves the appropriate exact counting invariant.

theorem CertifiedRowSystem.Complement.protocolAccepts_sound {I : Type u_1} {A : Type u_2} {Q : Type u_3} {F : Type u_4} [Fintype A] [Nonempty A] [DecidableEq A] (D : CertifiedRowSystem I A Unit Q F) {input : List I} (hinput : input ≠ []) : ProtocolAccepts D input → SourceRejects D input

The semantic protocol cannot falsely accept a source input.

Completeness

theorem CertifiedRowSystem.Complement.protocolAccepts_complete {I : Type u_1} {A : Type u_2} {Q : Type u_3} {F : Type u_4} [Fintype A] [Nonempty A] [DecidableEq A] (D : CertifiedRowSystem I A Unit Q F) {input : List I} (hinput : input ≠ []) : SourceRejects D input → ProtocolAccepts D input

If the source rejects, the canonical inductive-counting choices form an accepting protocol run.

theorem CertifiedRowSystem.Complement.protocolAccepts_iff_sourceRejects {I : Type u_1} {A : Type u_2} {Q : Type u_3} {F : Type u_4} [Fintype A] [Nonempty A] [DecidableEq A] (D : CertifiedRowSystem I A Unit Q F) {input : List I} (hinput : input ≠ []) : ProtocolAccepts D input ↔ SourceRejects D input

The machine-independent certified-row complement protocol accepts exactly the inputs rejected by its deterministic source system.

Language correctness

theorem CertifiedRowSystem.Complement.rowReachLanguage_deterministicComplementSystem {I : Type u_1} {A : Type u_2} {Q : Type u_3} {F : Type u_4} [Fintype A] [Nonempty A] [DecidableEq A] [Fintype Q] [Fintype F] (D : CertifiedRowSystem I A Unit Q F) : (deterministicComplementSystem D).rowReachLanguage = D.rowReachLanguageᶜ \ {[]}

The compiled deterministic-source system recognizes the complement of the source row language, relative to nonempty inputs.

theorem CertifiedRowSystem.rowReachLanguage_complementSystem {I : Type u_1} {A : Type u_2} {C : Type u_3} {Q : Type u_4} {F : Type u_5} [Fintype A] [Nonempty A] [DecidableEq A] [Fintype C] [Fintype Q] [DecidableEq Q] [Fintype F] (S : CertifiedRowSystem I A C Q F) : (Complement.complementSystem S).rowReachLanguage = S.rowReachLanguageᶜ \ {[]}

Machine-independent complementation for an arbitrary finite certified row system. The certificate alphabet is determinized before the counting protocol is installed.