+# Arithmetic checking of second-order certificates

Represent each free relation by its truth-table string. Matrix evaluation reads these strings at arithmetic tuple indices. Each existential relation quantifier consumes the next table from the certificate and prepends it to the environment; short tables and trailing certificate bits are rejected.

These total functions implement the verifier in Immerman's Descriptive Complexity, Section 7.1, Proposition 7.6. The surface module proves agreement with the existing checker and polynomial time against the machine definitions.

def Complexity.DescriptiveComplexity.SOFormula.evalMatrixCode {V : Vocabulary} (card : ℕ) (input : List Bool) {rctx : List ℕ} {n : ℕ} (φ : SOFormula V rctx n) : φ.IsFOMatrix → (Fin n → ℕ) → (Fin rctx.length → List Bool) → Bool

Evaluate an FO matrix directly on structure bits and supplied relation-table strings.

Equations

• One or more equations did not get rendered due to their size.
• Complexity.DescriptiveComplexity.SOFormula.evalMatrixCode card input φ.neg h x_2 x_3 = !Complexity.DescriptiveComplexity.SOFormula.evalMatrixCode card input φ h x_2 x_3
• Complexity.DescriptiveComplexity.SOFormula.evalMatrixCode card input (Complexity.DescriptiveComplexity.SOFormula.soExist k a) h x_2 x_3 = False.elim h
• Complexity.DescriptiveComplexity.SOFormula.evalMatrixCode card input (Complexity.DescriptiveComplexity.SOFormula.soAll k a) h x_2 x_3 = False.elim h

def Complexity.DescriptiveComplexity.SOFormula.checkCertificateCode {V : Vocabulary} (card : ℕ) (input : List Bool) {rctx : List ℕ} {n : ℕ} (φ : SOFormula V rctx n) : φ.IsExistSO → (Fin n → ℕ) → (Fin rctx.length → List Bool) → List Bool → Bool

Consume the existential prefix's truth tables, then run arithmetic matrix evaluation.

Equations

• One or more equations did not get rendered due to their size.
• Complexity.DescriptiveComplexity.SOFormula.checkCertificateCode card input (Complexity.DescriptiveComplexity.SOFormula.soAll k a) h x_2 x_3 x_4 = False.elim h