Structure-encoding validation belongs to P

The explicit header, length, and one-hot conditions characterize exactly the encoder's image. They are polynomial-time predicates by bounded quantification over the arithmetic bit-access primitives. Thus recognizing valid encodings and testing successful decoding belong to the existing machine class P.

This proves the validation part of the descriptive-complexity machine bridge. ModelChecking.PolynomialTime combines it with fixed-formula evaluation to prove first-order query languages belong to P. SecondOrder.PolynomialTime uses the same validation predicate for its existential-SO certificate verifier.

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

Every encoded structure satisfies the explicit wire-format conditions.

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

Wire-format validation is equivalent to encoding a structure of the specified size.

theorem Complexity.DescriptiveComplexity.isValidEncoding_parsed_iff (V : Vocabulary) (bits : List Bool) : IsValidEncoding V (List.takeWhile id bits).length bits ↔ ∃ (A : DecFinStruct V), encodeStruct A = bits

Validation at the parsed universe size recognizes exactly all structure encodings.

theorem Complexity.DescriptiveComplexity.isValidEncoding_fpPred (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)

Wire-format validation is polynomial-time when the string and universe size are.

theorem Complexity.DescriptiveComplexity.encodable_fpPred (V : Vocabulary) : FPPred fun (bits : List Bool) => ∃ (A : DecFinStruct V), encodeStruct A = bits

Membership in the encoder's image is a polynomial-time predicate on every bit string.

theorem Complexity.DescriptiveComplexity.decodable_fpPred (V : Vocabulary) : FPPred fun (bits : List Bool) => ∃ (A : DecFinStruct V), decodeStruct V bits = some A

Whether the existing exact decoder succeeds can be tested in polynomial time.

theorem Complexity.DescriptiveComplexity.validEncodings_mem_P (V : Vocabulary) : {bits : List Bool | ∃ (A : DecFinStruct V), encodeStruct A = bits} ∈ P

The binary language of valid encodings belongs to the actual deterministic machine class P.