Correctness and polynomial time of encoded interpretations

Generate each defining formula's truth table in the canonical tuple order and copy each designated constant's one-hot block. The resulting string is exactly the encoding of the interpreted structure. Polynomial-time validation guards this table generator and maps every malformed input to the empty string.

theorem Complexity.DescriptiveComplexity.applyDec_toFinStruct_internal {V W : Vocabulary} (I : FOInterpretation V W) (A : DecFinStruct V) : (I.applyDec A).toFinStruct = I.apply A.toFinStruct

theorem Complexity.DescriptiveComplexity.rawEncoding_encodeStruct_internal {V W : Vocabulary} (I : FOInterpretation V W) (A : DecFinStruct V) : I.rawEncoding A.card (encodeStruct A) = encodeStruct (I.applyDec A)

theorem Complexity.DescriptiveComplexity.rawEncoding_length_internal {V W : Vocabulary} (I : FOInterpretation V W) (card : ℕ) (input : List Bool) : (I.rawEncoding card input).length = encodingLength W card

theorem Complexity.DescriptiveComplexity.rawEncoding_mem_FP_internal {V W : Vocabulary} (I : FOInterpretation V W) {input : List Bool → List Bool} {card : List Bool → ℕ} (hinput : input ∈ FP) (hcard : UnaryFn card) : (fun (z : List Bool) => I.rawEncoding (card z) (input z)) ∈ FP

theorem Complexity.DescriptiveComplexity.mapEncoding_mem_FP_internal {V W : Vocabulary} (I : FOInterpretation V W) : I.mapEncoding ∈ FP

theorem Complexity.DescriptiveComplexity.mapEncoding_mem_queryLanguage_iff_internal {V W : Vocabulary} (I : FOInterpretation V W) (Q : BooleanQuery W) (input : List Bool) : I.mapEncoding input ∈ queryLanguage Q ↔ input ∈ queryLanguage fun (A : FinStruct V) => Q (I.apply A)