Structural first-order reductions give polynomial-time many-one reductions

The computable interpretation agrees exactly with the original structure map. Its encoded map belongs to FP, outputs the complete target truth tables and constant blocks, and sends malformed source strings to the non-encoding []. Consequently FOReduces induces the library's existing MapReducesPoly relation on binary query languages, with no promise restricting the input strings.

Combining this bridge with Fagin's upper direction gives a completeness criterion: an existential-SO target query is NP-complete if an NP-hard encoded query reduces to it by an existing universe-preserving FO interpretation. This implements the structural reduction method of Immerman's Descriptive Complexity, Chapter 3. The tagged tuple encoding bridge and exact first-order projections remain separate.

@[simp]

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

Computable interpretation represents the original propositional structure map exactly.

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

Arithmetic generation yields precisely the interpreted structure's encoding.

@[simp]

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

The raw output includes the header, every target relation table, and every constant block.

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

Arithmetic table generation is polynomial-time on polynomial-time supplied input and size.

@[simp]

theorem Complexity.DescriptiveComplexity.FOInterpretation.mapEncoding_encodeStruct {V W : Vocabulary} (I : FOInterpretation V W) (A : DecFinStruct V) : I.mapEncoding (encodeStruct A) = encodeStruct (I.applyDec A)

On valid encodings, the binary map applies the interpretation and re-encodes its output.

theorem Complexity.DescriptiveComplexity.FOInterpretation.mapEncoding_of_decode_eq_none {V W : Vocabulary} (I : FOInterpretation V W) (input : List Bool) (h : decodeStruct V input = none) : I.mapEncoding input = []

Every malformed source encoding maps to the empty string.

@[simp]

theorem Complexity.DescriptiveComplexity.FOInterpretation.mapEncoding_nil {V W : Vocabulary} (I : FOInterpretation V W) : I.mapEncoding [] = []

In particular, an interpretation's binary map preserves the fixed malformed input [].

theorem Complexity.DescriptiveComplexity.FOInterpretation.mapEncoding_length_encodeStruct {V W : Vocabulary} (I : FOInterpretation V W) (A : DecFinStruct V) : (I.mapEncoding (encodeStruct A)).length = encodingLength W A.card

A valid input produces the full encoded target length at the same universe cardinality.

theorem Complexity.DescriptiveComplexity.FOInterpretation.mapEncoding_length_le {V W : Vocabulary} (I : FOInterpretation V W) (input : List Bool) : (I.mapEncoding input).length ≤ encodingLength W input.length

The full output length is bounded by the target encoding polynomial in input length.

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

Every fixed universe-preserving FO interpretation gives an actual polynomial-time string map.

theorem Complexity.DescriptiveComplexity.FOInterpretation.mapEncoding_mem_queryLanguage_iff {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)

The binary map pulls query languages back exactly, including every malformed input.

theorem Complexity.DescriptiveComplexity.FOReduces.mapReducesPoly {V W : Vocabulary} {Q₁ : BooleanQuery V} {Q₂ : BooleanQuery W} (h : FOReduces Q₁ Q₂) : queryLanguage Q₁ ≤ₚ queryLanguage Q₂

Structural FO reducibility induces polynomial-time many-one reducibility on binary languages.

theorem Complexity.DescriptiveComplexity.FOProjReduces.mapReducesPoly {V W : Vocabulary} {Q₁ : BooleanQuery V} {Q₂ : BooleanQuery W} (h : FOProjReduces Q₁ Q₂) : queryLanguage Q₁ ≤ₚ queryLanguage Q₂

The legacy quantifier-free interpretation reductions also induce polynomial-time reductions.

theorem Complexity.DescriptiveComplexity.FOReduces.queryLanguage_mem_P {V W : Vocabulary} {Q₁ : BooleanQuery V} {Q₂ : BooleanQuery W} (h : FOReduces Q₁ Q₂) (hQ₂ : queryLanguage Q₂ ∈ P) : queryLanguage Q₁ ∈ P

Machine P membership transports backward along structural FO reductions.

theorem Complexity.DescriptiveComplexity.FOReduces.queryLanguage_mem_NP {V W : Vocabulary} {Q₁ : BooleanQuery V} {Q₂ : BooleanQuery W} (h : FOReduces Q₁ Q₂) (hQ₂ : queryLanguage Q₂ ∈ NP) : queryLanguage Q₁ ∈ NP

Machine NP membership transports backward along structural FO reductions.

theorem Complexity.DescriptiveComplexity.ExistSODefinable.npComplete_of_foReduces {V W : Vocabulary} {Q₁ : BooleanQuery V} {Q₂ : BooleanQuery W} (hQ₂ : ExistSODefinable Q₂) (hhard : NPHard (queryLanguage Q₁)) (hred : FOReduces Q₁ Q₂) : NPComplete (queryLanguage Q₂)

An ESO target is NP-complete when an NP-hard encoded query FO-reduces to it.