+# Correctness and polynomial time of second-order verification

Arithmetic matrix evaluation agrees with semantic satisfaction when supplied canonical relation tables. Certificate consumption agrees with the existing decoder-based checker. Bounded bit access, quantification, and string slicing then give the polynomial-time verifier required by the NP witness construction.

theorem Complexity.DescriptiveComplexity.matrix_evalCode_sat_internal {V : Vocabulary} {rctx : List ℕ} {n : ℕ} (A : DecFinStruct V) (φ : SOFormula V rctx n) (h : φ.IsFOMatrix) (σ : Env A.card n) (ρ : DecREnv A.card rctx) : (SOFormula.evalMatrixCode A.card (encodeStruct A) φ h (fun (i : Fin n) => ↑(σ i)) fun (r : Fin rctx.length) => encodeRelC (ρ r)) = true ↔ SOFormula.Sat A.toFinStruct σ ρ.toREnv φ

theorem Complexity.DescriptiveComplexity.matrix_evalCode_eq_internal {V : Vocabulary} {rctx : List ℕ} {n : ℕ} (A : DecFinStruct V) (φ : SOFormula V rctx n) (h : φ.IsFOMatrix) (σ : Env A.card n) (ρ : DecREnv A.card rctx) : (SOFormula.evalMatrixCode A.card (encodeStruct A) φ h (fun (i : Fin n) => ↑(σ i)) fun (r : Fin rctx.length) => encodeRelC (ρ r)) = SOFormula.evalMatrixB A φ h σ ρ

theorem Complexity.DescriptiveComplexity.matrix_evalCode_fpPred_internal {V : Vocabulary} {rctx : List ℕ} {n : ℕ} (φ : SOFormula V rctx n) (h : φ.IsFOMatrix) (input : List Bool → List Bool) (card : List Bool → ℕ) (σ : List Bool → Fin n → ℕ) (tables : List Bool → Fin rctx.length → List Bool) : input ∈ FP → UnaryFn card → (∀ (i : Fin n), UnaryFn fun (z : List Bool) => σ z i) → (∀ (r : Fin rctx.length), (fun (z : List Bool) => tables z r) ∈ FP) → FPPred fun (z : List Bool) => SOFormula.evalMatrixCode (card z) (input z) φ h (σ z) (tables z) = true

theorem Complexity.DescriptiveComplexity.certificate_evalCode_eq_internal {V : Vocabulary} {rctx : List ℕ} {n : ℕ} (A : DecFinStruct V) (φ : SOFormula V rctx n) (h : φ.IsExistSO) (σ : Env A.card n) (ρ : DecREnv A.card rctx) (certificate : List Bool) : SOFormula.checkCertificateCode A.card (encodeStruct A) φ h (fun (i : Fin n) => ↑(σ i)) (fun (r : Fin rctx.length) => encodeRelC (ρ r)) certificate = SOFormula.checkCertificate A φ h σ ρ certificate

theorem Complexity.DescriptiveComplexity.certificate_evalCode_fpPred_internal {V : Vocabulary} {rctx : List ℕ} {n : ℕ} (φ : SOFormula V rctx n) (h : φ.IsExistSO) (input : List Bool → List Bool) (card : List Bool → ℕ) (σ : List Bool → Fin n → ℕ) (tables : List Bool → Fin rctx.length → List Bool) (certificate : List Bool → List Bool) : input ∈ FP → UnaryFn card → (∀ (i : Fin n), UnaryFn fun (z : List Bool) => σ z i) → (∀ (r : Fin rctx.length), (fun (z : List Bool) => tables z r) ∈ FP) → certificate ∈ FP → FPPred fun (z : List Bool) => SOFormula.checkCertificateCode (card z) (input z) φ h (σ z) (tables z) (certificate z) = true

theorem Complexity.DescriptiveComplexity.sentence_checkEncoded_code_iff_internal {V : Vocabulary} (φ : SOSentence V) (h : SOFormula.IsExistSO φ) (input certificate : List Bool) : φ.checkEncoded h input certificate = true ↔ (∃ (A : DecFinStruct V), encodeStruct A = input) ∧ SOFormula.checkCertificateCode (List.takeWhile id input).length input φ h Fin.elim0 Fin.elim0 certificate = true

theorem Complexity.DescriptiveComplexity.sentence_checkEncoded_fpPred_internal {V : Vocabulary} (φ : SOSentence V) (h : SOFormula.IsExistSO φ) {input certificate : List Bool → List Bool} (hinput : input ∈ FP) (hc : certificate ∈ FP) : FPPred fun (z : List Bool) => φ.checkEncoded h (input z) (certificate z) = true

theorem Complexity.DescriptiveComplexity.sentence_queryLanguage_mem_NP_internal {V : Vocabulary} (φ : SOSentence V) (h : SOFormula.IsExistSO φ) : (queryLanguage fun (A : FinStruct V) => SOSentence.Models A φ) ∈ NP