Correctness and polynomial time of encoding validation

Construct a structure from unrestricted relation bits and one-hot constant blocks. The arithmetic-access theorems recover the original string. Bounded quantifiers over polynomial-time bit reads implement every validation condition.

theorem Complexity.DescriptiveComplexity.isValidEncoding_encodeStruct_internal {V : Vocabulary} (A : DecFinStruct V) : IsValidEncoding V A.card (encodeStruct A)

theorem Complexity.DescriptiveComplexity.isValidEncoding_iff_internal (V : Vocabulary) (card : ℕ) (bits : List Bool) : IsValidEncoding V card bits ↔ ∃ (A : DecFinStruct V), A.card = card ∧ encodeStruct A = bits

theorem Complexity.DescriptiveComplexity.isValidEncoding_fpPred_internal (V : Vocabulary) {bits : List Bool → List Bool} {card : List Bool → ℕ} (hbits : bits ∈ FP) (hcard : UnaryFn card) : FPPred fun (z : List Bool) => IsValidEncoding V (card z) (bits z)