Arithmetic realization of tagged interpretations

Mathlib's tuple equivalence uses little-endian numerals, exactly as the structure encoder does. The product equivalence places the tag above the coordinate block. These identities identify arithmetic relation and constant generation with the existing interpreted structure. Fixed finite formula selection, table scanning, and encoding validation then give a polynomial-time string map.

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

theorem Complexity.DescriptiveComplexity.TaggedFOInterpretation.elementEquiv_coord_val_internal {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

theorem Complexity.DescriptiveComplexity.TaggedFOInterpretation.elementEquiv_symm_val_internal {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

theorem Complexity.DescriptiveComplexity.TaggedFOInterpretation.relationEnvCode_eq_internal {tags dim card arity : ℕ} (args : Fin arity → Fin (tags * card ^ dim)) : (relationEnvCode card dim fun (j : Fin arity) => ↑(args j)) = fun (k : Fin (arity * dim)) => ↑(relationEnv args k)

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

theorem Complexity.DescriptiveComplexity.TaggedFOInterpretation.relationBitCode_encodeStruct_internal {V W : Vocabulary} {tags dim : ℕ} (I : TaggedFOInterpretation V W tags dim) (A : DecFinStruct V) (r : Fin W.numRels) (args : Fin (W.relArity r) → Fin (tags * A.card ^ dim)) : (I.relationBitCode r A.card (encodeStruct A) fun (j : Fin (W.relArity r)) => ↑(args j)) = (I.applyDec A).rel r args

theorem Complexity.DescriptiveComplexity.TaggedFOInterpretation.relationTableCode_encodeStruct_internal {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)

theorem Complexity.DescriptiveComplexity.TaggedFOInterpretation.constantCode_encodeStruct_internal {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)

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

theorem Complexity.DescriptiveComplexity.TaggedFOInterpretation.rawEncoding_length_internal {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)