Soundness, completeness, and length of existential-SO certificates

Induct along the existential prefix. Each decoded table supplies one semantic relation; conversely, its characteristic function supplies a certificate block. At the matrix, acceptance requires that no certificate bits remain.

theorem Complexity.DescriptiveComplexity.SOFormula.checkCertificate_sound_internal {V : Vocabulary} (A : DecFinStruct V) {rctx : List ℕ} {n : ℕ} (φ : SOFormula V rctx n) (h : φ.IsExistSO) (σ : Env A.card n) (ρ : DecREnv A.card rctx) (bits : List Bool) : checkCertificate A φ h σ ρ bits = true → bits.length = DecREnv.encodingLength A.card φ.witnessArities ∧ Sat A.toFinStruct σ ρ.toREnv φ

theorem Complexity.DescriptiveComplexity.SOFormula.checkCertificate_complete_internal {V : Vocabulary} (A : DecFinStruct V) {rctx : List ℕ} {n : ℕ} (φ : SOFormula V rctx n) (h : φ.IsExistSO) (σ : Env A.card n) (ρ : DecREnv A.card rctx) : Sat A.toFinStruct σ ρ.toREnv φ → ∃ (bits : List Bool), checkCertificate A φ h σ ρ bits = true