Correctness and polynomial time of arithmetic first-order evaluation

Constant lookup recovers the unique marked entry. Arithmetic reads and bounded quantifiers then support structural induction on the formula, both for semantic correctness and for the machine-level polynomial-time proof.

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

theorem Complexity.DescriptiveComplexity.term_evalCode_unary_internal {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) => Term.evalCode (card z) (bits z) (σ z) t

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

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

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

theorem Complexity.DescriptiveComplexity.sentence_validatedCode_internal {V : Vocabulary} (φ : Sentence V) (input : List Bool) : (∃ (A : DecFinStruct V), encodeStruct A = input) ∧ Formula.evalCode (List.takeWhile id input).length input φ Fin.elim0 = true ↔ input ∈ queryLanguage fun (A : FinStruct V) => Sentence.Models A φ

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

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

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