First-order model checking on encoded inputs

Decode a structure and evaluate the sentence, rejecting every malformed string. Correctness refers to the existing queryLanguage, so it includes all binary inputs. ModelChecking.PolynomialTime proves that its one-bit verdict belongs to the machine class FP for each fixed sentence.

def Complexity.DescriptiveComplexity.Sentence.evalEncoded {V : Vocabulary} (φ : Sentence V) (bits : List Bool) : Bool

Evaluate a sentence on an encoded structure, returning false on malformed input.

Equations

• φ.evalEncoded bits = match Complexity.DescriptiveComplexity.decodeStruct V bits with | none => false | some A => Complexity.DescriptiveComplexity.Sentence.evalB A φ

@[simp]

theorem Complexity.DescriptiveComplexity.Sentence.evalEncoded_nil {V : Vocabulary} (φ : Sentence V) : φ.evalEncoded [] = false

The encoded evaluator rejects the unique length-zero input.

theorem Complexity.DescriptiveComplexity.Sentence.evalEncoded_eq_queryLanguage {V : Vocabulary} (φ : Sentence V) (bits : List Bool) : φ.evalEncoded bits = true ↔ bits ∈ queryLanguage fun (A : FinStruct V) => Models A φ

The encoded evaluator recognizes exactly the sentence's induced binary language.

@[simp]

theorem Complexity.DescriptiveComplexity.Sentence.evalEncoded_encodeStruct {V : Vocabulary} (φ : Sentence V) (A : DecFinStruct V) : φ.evalEncoded (encodeStruct A) = evalB A φ

On a valid encoding, encoded evaluation agrees with structure-level evaluation.