Verified binary certificates for existential second-order logic

An existential-SO formula is true exactly when its certificate checker accepts some bit string. Every accepted certificate has exactly the sum of the truth table sizes of the prefix relations. For sentences, the encoded checker gives the same characterization of the existing query language, rejects malformed structure encodings, and bounds certificate length by a fixed polynomial in input length. SecondOrder.PolynomialTime proves that a polynomial-time machine computes the checker's verdict, giving the upper direction of Fagin's theorem.

theorem Complexity.DescriptiveComplexity.SOFormula.witnessArities_of_isFOMatrix {V : Vocabulary} {rctx : List ℕ} {n : ℕ} (φ : SOFormula V rctx n) (h : φ.IsFOMatrix) : φ.witnessArities = []

An FO matrix has no relation-witness prefix.

@[simp]

theorem Complexity.DescriptiveComplexity.SOFormula.witnessPolynomial_eval {V : Vocabulary} {rctx : List ℕ} {n : ℕ} (φ : SOFormula V rctx n) (card : ℕ) : Polynomial.eval card φ.witnessPolynomial = DecREnv.encodingLength card φ.witnessArities

The witness polynomial evaluates to the exact sum of relation-table sizes.

theorem Complexity.DescriptiveComplexity.SOFormula.checkCertificate_matrix {V : Vocabulary} {rctx : List ℕ} {n : ℕ} (A : DecFinStruct V) (φ : SOFormula V rctx n) (h : φ.IsExistSO) (hm : φ.IsFOMatrix) (σ : Env A.card n) (ρ : DecREnv A.card rctx) (bits : List Bool) : checkCertificate A φ h σ ρ bits = (bits.isEmpty && evalMatrixB A φ hm σ ρ)

A matrix consumes no witness bits and uses the existing matrix evaluator.

theorem Complexity.DescriptiveComplexity.SOFormula.checkCertificate_ofFormula {V : Vocabulary} {rctx : List ℕ} {n : ℕ} (A : DecFinStruct V) (φ : Formula V n) (σ : Env A.card n) (ρ : DecREnv A.card rctx) (bits : List Bool) : checkCertificate A (ofFormula φ rctx) ⋯ σ ρ bits = (bits.isEmpty && Formula.evalB A σ φ)

An embedded FO formula needs the empty certificate and runs the FO evaluator.

theorem Complexity.DescriptiveComplexity.SOFormula.checkCertificate_soExist_append {V : Vocabulary} {rctx : List ℕ} {n : ℕ} (A : DecFinStruct V) {k : ℕ} (φ : SOFormula V (k :: rctx) n) (h : φ.IsExistSO) (σ : Env A.card n) (ρ : DecREnv A.card rctx) (τ : DecREnv A.card [k]) (bits : List Bool) : checkCertificate A (soExist k φ) h σ ρ (τ.encode ++ bits) = checkCertificate A φ h σ (DecREnv.cons (τ 0) ρ) bits

An encoded prefix table is consumed exactly, leaving the next relation environment.

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

An accepted certificate proves satisfaction of the existential-SO formula.

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

Every accepted certificate has exactly the prescribed truth-table length.

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

Binary certificates are sound and complete for existential-SO satisfaction.

@[simp]

theorem Complexity.DescriptiveComplexity.SOSentence.checkEncoded_encodeStruct {V : Vocabulary} (φ : SOSentence V) (h : SOFormula.IsExistSO φ) (A : DecFinStruct V) (certificate : List Bool) : φ.checkEncoded h (encodeStruct A) certificate = SOFormula.checkCertificate A φ h (emptyEnv A.card) (DecREnv.empty A.card) certificate

Checking on a valid structure encoding agrees with structure-level certificate checking.

theorem Complexity.DescriptiveComplexity.SOSentence.checkEncoded_of_decode_eq_none {V : Vocabulary} (φ : SOSentence V) (h : SOFormula.IsExistSO φ) (input certificate : List Bool) (hinput : decodeStruct V input = none) : φ.checkEncoded h input certificate = false

A malformed structure encoding is rejected with every certificate.

theorem Complexity.DescriptiveComplexity.SOSentence.exists_checkEncoded_iff {V : Vocabulary} (φ : SOSentence V) (h : SOFormula.IsExistSO φ) (input : List Bool) : (∃ (certificate : List Bool), φ.checkEncoded h input certificate = true) ↔ input ∈ queryLanguage fun (A : FinStruct V) => Models A φ

The encoded checker has a witness exactly on the sentence's induced language.

theorem Complexity.DescriptiveComplexity.SOSentence.checkEncoded_certificate_length {V : Vocabulary} (φ : SOSentence V) (h : SOFormula.IsExistSO φ) (input certificate : List Bool) (haccept : φ.checkEncoded h input certificate = true) : certificate.length = DecREnv.encodingLength (List.takeWhile id input).length (SOFormula.witnessArities φ)

An accepted certificate has exactly the table size determined by the input cardinality.

theorem Complexity.DescriptiveComplexity.SOSentence.checkEncoded_length_le {V : Vocabulary} (φ : SOSentence V) (h : SOFormula.IsExistSO φ) (input certificate : List Bool) (haccept : φ.checkEncoded h input certificate = true) : certificate.length ≤ Polynomial.eval input.length (SOFormula.witnessPolynomial φ)

Accepted certificates are polynomially bounded in the encoded input length.

theorem Complexity.DescriptiveComplexity.SOSentence.exists_checkEncoded_bounded_iff {V : Vocabulary} (φ : SOSentence V) (h : SOFormula.IsExistSO φ) (input : List Bool) : (∃ (certificate : List Bool), certificate.length ≤ Polynomial.eval input.length (SOFormula.witnessPolynomial φ) ∧ φ.checkEncoded h input certificate = true) ↔ input ∈ queryLanguage fun (A : FinStruct V) => Models A φ

Adding the polynomial certificate bound preserves the exact language characterization.