+# Existential second-order queries belong to NP

For each fixed existential-SO sentence, the existing binary certificate checker has a polynomial-time one-bit verdict. Arithmetic table reads, bounded first-order quantifiers, and polynomial-time certificate slicing establish the machine bound. Validation rejects malformed structures; the existing checker also rejects missing or trailing certificate bits.

Combining this verifier with its proved polynomial witness bound and the library's guess-and-verify NTM proves ExistSODefinable.queryLanguage_mem_NP. This is the upper direction of Fagin's theorem, following Immerman's Descriptive Complexity, Section 7.1, Proposition 7.6. The converse tableau construction is not asserted. Formulas and vocabularies are fixed parameters.

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

Arithmetic matrix evaluation agrees with semantics on canonical structure and relation bits.

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

Arithmetic matrix evaluation gives exactly the existing Boolean matrix evaluator's verdict.

theorem Complexity.DescriptiveComplexity.SOFormula.evalMatrixCode_fpPred {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} (hinput : input ∈ FP) (hcard : UnaryFn card) (hσ : ∀ (i : Fin n), UnaryFn fun (z : List Bool) => σ z i) (ht : ∀ (r : Fin rctx.length), (fun (z : List Bool) => tables z r) ∈ FP) : FPPred fun (z : List Bool) => evalMatrixCode (card z) (input z) φ h (σ z) (tables z) = true

A fixed matrix is polynomial-time on polynomial-time structure bits, values, and tables.

theorem Complexity.DescriptiveComplexity.SOFormula.checkCertificateCode_encodeStruct {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) : checkCertificateCode A.card (encodeStruct A) φ h (fun (i : Fin n) => ↑(σ i)) (fun (r : Fin rctx.length) => encodeRelC (ρ r)) certificate = checkCertificate A φ h σ ρ certificate

Arithmetic certificate consumption agrees with the existing checker on encoded structures.

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

Checking a fixed existential prefix is polynomial-time on polynomial-time supplied data.

theorem Complexity.DescriptiveComplexity.SOSentence.checkEncoded_fpPred {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

The existing encoded certificate checker is a polynomial-time predicate.

theorem Complexity.DescriptiveComplexity.SOSentence.checkEncoded_mem_FP {V : Vocabulary} (φ : SOSentence V) (h : SOFormula.IsExistSO φ) : (fun (z : List Bool) => [φ.checkEncoded h (pairFst z) (pairSnd z)]) ∈ FP

A polynomial-time machine computes the existing encoded checker's one-bit verdict.

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

Fagin's upper direction: every fixed existential-SO sentence induces a language in NP.

theorem Complexity.DescriptiveComplexity.ExistSODefinable.queryLanguage_mem_NP {V : Vocabulary} {Q : BooleanQuery V} (hQ : ExistSODefinable Q) : queryLanguage Q ∈ NP

An existential-SO witness places the induced binary query language in machine NP.