Tagged interpretations on binary encodings

The decidable structure map uses the same finite product and tuple equivalences as the original interpretation. Arithmetic generation recovers tags by division and coordinates by base expansion. Each relation chooses among the fixed finite family of defining formulas; constants pack tuples of source constants.

The full output has universe size tags * card ^ dim. Its binary map decodes, interprets, and re-encodes, with the fixed non-encoding [] for malformed input. This extends the structural reduction method of Immerman, Chapter 3, to the tagged full-product interpretation design of Senellart and Gnatenko (2026).

def Complexity.DescriptiveComplexity.TaggedFOInterpretation.applyDec {V W : Vocabulary} {tags dim : ℕ} (I : TaggedFOInterpretation V W tags dim) (A : DecFinStruct V) : DecFinStruct W

Evaluate the defining formulas on the exact tagged tuple universe.

Equations

• One or more equations did not get rendered due to their size.

def Complexity.DescriptiveComplexity.TaggedFOInterpretation.relationEnvCode (card dim : ℕ) {arity : ℕ} (args : Fin arity → ℕ) : Fin (arity * dim) → ℕ

Recover the flattened source coordinates from numeric target-element indices.

Equations

• One or more equations did not get rendered due to their size.

def Complexity.DescriptiveComplexity.TaggedFOInterpretation.relationBitCode {V W : Vocabulary} {tags dim : ℕ} (I : TaggedFOInterpretation V W tags dim) (r : Fin W.numRels) (card : ℕ) (input : List Bool) (args : Fin (W.relArity r) → ℕ) : Bool

Select a defining formula by its tag tuple and evaluate its source coordinates.

Equations

• One or more equations did not get rendered due to their size.

def Complexity.DescriptiveComplexity.TaggedFOInterpretation.relationTableCode {V W : Vocabulary} {tags dim : ℕ} (I : TaggedFOInterpretation V W tags dim) (r : Fin W.numRels) (card : ℕ) (input : List Bool) : List Bool

Write the complete target relation table in canonical tuple order.

Equations

• One or more equations did not get rendered due to their size.

def Complexity.DescriptiveComplexity.TaggedFOInterpretation.constantCode {V W : Vocabulary} {tags dim : ℕ} (I : TaggedFOInterpretation V W tags dim) (c : Fin W.numConsts) (card : ℕ) (input : List Bool) : ℕ

Pack the fixed tag and source-constant coordinates of a target constant.

Equations

• One or more equations did not get rendered due to their size.

def Complexity.DescriptiveComplexity.TaggedFOInterpretation.rawEncoding {V W : Vocabulary} {tags dim : ℕ} (I : TaggedFOInterpretation V W tags dim) (card : ℕ) (input : List Bool) : List Bool

Generate all target tables and constant blocks at a supplied source size.

Equations

• One or more equations did not get rendered due to their size.

def Complexity.DescriptiveComplexity.TaggedFOInterpretation.mapEncoding {V W : Vocabulary} {tags dim : ℕ} (I : TaggedFOInterpretation V W tags dim) (input : List Bool) : List Bool

Decode, interpret, and re-encode, sending malformed inputs to the non-encoding [].

Equations

• I.mapEncoding input = match Complexity.DescriptiveComplexity.decodeStruct V input with | none => [] | some A => Complexity.DescriptiveComplexity.encodeStruct (I.applyDec A)