Exact encoded semantics for tagged interpretations

Arithmetic tag and coordinate extraction agrees with the original finite equivalences. Generating the relation tables and packed constants therefore produces exactly the interpreted structure's encoding, of length encodingLength W (tags * card ^ dim).

The decoder-based map rejects malformed inputs. Its polynomial-time machine bound remains to be proved; this module is the semantic checkpoint for that bridge.

theorem Complexity.DescriptiveComplexity.TaggedFOInterpretation.elementEquiv_tag_val {tags dim card : ℕ} (x : Fin (tags * card ^ dim)) : ↑((elementEquiv card tags dim) x).1 = ↑x / card ^ dim

The tag occupies the quotient above the full tuple block.

theorem Complexity.DescriptiveComplexity.TaggedFOInterpretation.elementEquiv_coord_val {tags dim card : ℕ} (x : Fin (tags * card ^ dim)) (j : Fin dim) : ↑(((elementEquiv card tags dim) x).2 j) = tupleDigits card dim (↑x % card ^ dim) j

Coordinates are the base-card digits of the tuple-block remainder.

theorem Complexity.DescriptiveComplexity.TaggedFOInterpretation.elementEquiv_symm_val {tags dim card : ℕ} (tag : Fin tags) (coords : Fin dim → Fin card) : ↑((elementEquiv card tags dim).symm (tag, coords)) = (tupleIndex card fun (j : Fin dim) => ↑(coords j)) + card ^ dim * ↑tag

Packing a tagged tuple adds its positional numeral to its tag block's offset.

@[simp]

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

The Boolean structure map represents the original interpretation exactly.

theorem Complexity.DescriptiveComplexity.TaggedFOInterpretation.relationTableCode_encodeStruct {V W : Vocabulary} {tags dim : ℕ} (I : TaggedFOInterpretation V W tags dim) (A : DecFinStruct V) (r : Fin W.numRels) : I.relationTableCode r A.card (encodeStruct A) = encodeRelC ((I.applyDec A).rel r)

Arithmetic relation generation writes the interpreted relation's exact truth table.

theorem Complexity.DescriptiveComplexity.TaggedFOInterpretation.constantCode_encodeStruct {V W : Vocabulary} {tags dim : ℕ} (I : TaggedFOInterpretation V W tags dim) (A : DecFinStruct V) (c : Fin W.numConsts) : I.constantCode c A.card (encodeStruct A) = ↑((I.applyDec A).const c)

Arithmetic constant generation recovers the exact packed distinguished element.

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

The arithmetic generator produces exactly the interpreted structure's binary encoding.

@[simp]

theorem Complexity.DescriptiveComplexity.TaggedFOInterpretation.rawEncoding_length {V W : Vocabulary} {tags dim : ℕ} (I : TaggedFOInterpretation V W tags dim) (card : ℕ) (input : List Bool) : (I.rawEncoding card input).length = encodingLength W (tags * card ^ dim)

The full output includes all target relation tables and one-hot constant blocks.

@[simp]

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

A valid input maps to the encoding of its interpreted structure.

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

Every malformed input maps to the fixed non-encoding [].