First-order queries belong to machine polynomial time

Arithmetic evaluation agrees with the original semantics on encoded structures. For each fixed formula it is polynomial-time when the input string, cardinality, and free-variable values are polynomial-time. Combining this result with exact encoding validation proves FODefinable.queryLanguage_mem_P for the existing machine class P, including every malformed input. The original encoded Boolean evaluator itself has an FP one-bit verdict. For open formulas, Formula.tableCode also writes the complete assignment truth table in polynomial time, with exactly card ^ n bits for n free variables.

This is the standard fixed-formula model-checking argument from Immerman's Descriptive Complexity, implemented using the library's machine-backed Cobham closure rules. Logarithmic space is not established. SecondOrder.PolynomialTime extends arithmetic evaluation to existential second-order certificate checking.

theorem Complexity.DescriptiveComplexity.Term.evalCode_encodeStruct {V : Vocabulary} {n : ℕ} (A : DecFinStruct V) (t : Term V n) (σ : Env A.card n) : evalCode A.card (encodeStruct A) (fun (i : Fin n) => ↑(σ i)) t = ↑(eval A.toFinStruct σ t)

Arithmetic term evaluation on an encoding recovers the semantic element's value.

theorem Complexity.DescriptiveComplexity.Term.evalCode_unary {V : Vocabulary} {n : ℕ} (t : Term V n) {bits : List Bool → List Bool} {card : List Bool → ℕ} {σ : List Bool → Fin n → ℕ} (hbits : bits ∈ FP) (hcard : UnaryFn card) (hσ : ∀ (i : Fin n), UnaryFn fun (z : List Bool) => σ z i) : UnaryFn fun (z : List Bool) => evalCode (card z) (bits z) (σ z) t

Term evaluation is polynomial-time on polynomial-time numeric inputs.

theorem Complexity.DescriptiveComplexity.Formula.evalCode_encodeStruct {V : Vocabulary} {n : ℕ} (A : DecFinStruct V) (φ : Formula V n) (σ : Env A.card n) : (evalCode A.card (encodeStruct A) φ fun (i : Fin n) => ↑(σ i)) = true ↔ Sat A.toFinStruct σ φ

Arithmetic formula evaluation on an encoding agrees with first-order satisfaction.

theorem Complexity.DescriptiveComplexity.Formula.evalCode_fpPred {V : Vocabulary} {n : ℕ} (φ : Formula V n) {bits : List Bool → List Bool} {card : List Bool → ℕ} {σ : List Bool → Fin n → ℕ} (hbits : bits ∈ FP) (hcard : UnaryFn card) (hσ : ∀ (i : Fin n), UnaryFn fun (z : List Bool) => σ z i) : FPPred fun (z : List Bool) => evalCode (card z) (bits z) φ (σ z) = true

A fixed formula gives a polynomial-time predicate on polynomial-time numeric inputs.

theorem Complexity.DescriptiveComplexity.Formula.evalCode_mem_FP {V : Vocabulary} {n : ℕ} (φ : Formula V n) {bits : List Bool → List Bool} {card : List Bool → ℕ} {σ : List Bool → Fin n → ℕ} (hbits : bits ∈ FP) (hcard : UnaryFn card) (hσ : ∀ (i : Fin n), UnaryFn fun (z : List Bool) => σ z i) : (fun (z : List Bool) => [evalCode (card z) (bits z) φ (σ z)]) ∈ FP

The arithmetic evaluator's one-bit verdict is a polynomial-time string function.

@[simp]

theorem Complexity.DescriptiveComplexity.Formula.tableCode_length {V : Vocabulary} {n : ℕ} (φ : Formula V n) (card : ℕ) (bits : List Bool) : (φ.tableCode card bits).length = card ^ n

A formula's assignment truth table has one bit for each tuple of variable values.

theorem Complexity.DescriptiveComplexity.Formula.tableCode_encodeStruct {V : Vocabulary} {n : ℕ} (A : DecFinStruct V) (φ : Formula V n) : φ.tableCode A.card (encodeStruct A) = encodeRelC fun (σ : Fin n → Fin A.card) => evalB A σ φ

Formula truth-table generation agrees with the canonical relation-table encoding.

theorem Complexity.DescriptiveComplexity.Formula.tableCode_mem_FP {V : Vocabulary} {n : ℕ} (φ : Formula V n) {bits : List Bool → List Bool} {card : List Bool → ℕ} (hbits : bits ∈ FP) (hcard : UnaryFn card) : (fun (z : List Bool) => φ.tableCode (card z) (bits z)) ∈ FP

Writing the full truth table of a fixed formula is polynomial-time.

theorem Complexity.DescriptiveComplexity.Sentence.evalCode_encodeStruct {V : Vocabulary} (A : DecFinStruct V) (φ : Sentence V) : Formula.evalCode A.card (encodeStruct A) φ Fin.elim0 = true ↔ Models A.toFinStruct φ

Closed arithmetic evaluation agrees with the original sentence semantics.

theorem Complexity.DescriptiveComplexity.Sentence.queryLanguage_fpPred {V : Vocabulary} (φ : Sentence V) : FPPred fun (input : List Bool) => input ∈ queryLanguage fun (A : FinStruct V) => Models A φ

Sentence truth on arbitrary encoded input is a polynomial-time predicate.

theorem Complexity.DescriptiveComplexity.Sentence.queryLanguage_mem_P {V : Vocabulary} (φ : Sentence V) : (queryLanguage fun (A : FinStruct V) => Models A φ) ∈ P

Every fixed first-order sentence defines a binary language in machine P.

theorem Complexity.DescriptiveComplexity.Sentence.evalEncoded_mem_FP {V : Vocabulary} (φ : Sentence V) : (fun (input : List Bool) => [φ.evalEncoded input]) ∈ FP

The existing decoder-based Boolean sentence evaluator has a polynomial-time verdict.

theorem Complexity.DescriptiveComplexity.FODefinable.queryLanguage_mem_P {V : Vocabulary} {Q : BooleanQuery V} (hQ : FODefinable Q) : queryLanguage Q ∈ P

First-order definability implies polynomial-time membership of the induced binary language.