Proofs for encoding validation

Literal tests characterize the header and one-hot blocks. Encoding reconstruction proves completeness of these tests; finite connective laws account for size and depth.

theorem Complexity.DescriptiveComplexity.encodingHeaderFormula_eval_internal (V : Vocabulary) (card : ℕ) (input : BitString (encodingLength V card)) : AC0Formula.eval input (encodingHeaderFormula V card) = true ↔ ∀ (i : Fin (card + 1)), input ⟨↑i, ⋯⟩ = decide (↑i < card)

theorem Complexity.DescriptiveComplexity.constantValueFormula_eval_internal (V : Vocabulary) (card : ℕ) (c : Fin V.numConsts) (a : Fin card) (input : BitString (encodingLength V card)) : AC0Formula.eval input (constantValueFormula V card c a) = true ↔ ∀ (b : Fin card), input ((encodingLayout V card).const c b) = decide (a = b)

theorem Complexity.DescriptiveComplexity.encodingValidityFormula_eval_internal (V : Vocabulary) (card : ℕ) (input : BitString (encodingLength V card)) : AC0Formula.eval input (encodingValidityFormula V card) = true ↔ 2 ≤ card ∧ (∀ (i : Fin (card + 1)), input ⟨↑i, ⋯⟩ = decide (↑i < card)) ∧ ∀ (c : Fin V.numConsts), ∃ (a : Fin card), ∀ (b : Fin card), input ((encodingLayout V card).const c b) = decide (a = b)

theorem Complexity.DescriptiveComplexity.encodingValidityFormula_encoded_internal {V : Vocabulary} (A : DecFinStruct V) : AC0Formula.eval (encodedInput A) (encodingValidityFormula V A.card) = true

theorem Complexity.DescriptiveComplexity.encodingValidityFormula_correct_internal (V : Vocabulary) (card : ℕ) (input : BitString (encodingLength V card)) : AC0Formula.eval input (encodingValidityFormula V card) = true ↔ ∃ (A : DecFinStruct V), encodeStruct A = List.ofFn input

theorem Complexity.DescriptiveComplexity.encodingValidityFormula_size_internal (V : Vocabulary) (card : ℕ) : (encodingValidityFormula V card).size = Polynomial.eval card (encodingValidityPolynomial V)

theorem Complexity.DescriptiveComplexity.encodingValidityFormula_depth_internal (V : Vocabulary) (card : ℕ) : (encodingValidityFormula V card).depth ≤ 3

theorem Complexity.DescriptiveComplexity.validatedExpansion_correct_internal {V : Vocabulary} (φ : Sentence V) (card : ℕ) (input : BitString (encodingLength V card)) : AC0Formula.eval input (φ.validatedExpansion card) = true ↔ List.ofFn input ∈ queryLanguage fun (A : FinStruct V) => Sentence.Models A φ

theorem Complexity.DescriptiveComplexity.validatedExpansion_size_internal {V : Vocabulary} (φ : Sentence V) (card : ℕ) : (φ.validatedExpansion card).size = Polynomial.eval card φ.validatedPolynomial

theorem Complexity.DescriptiveComplexity.validatedExpansion_depth_internal {V : Vocabulary} (φ : Sentence V) (card : ℕ) : (φ.validatedExpansion card).depth ≤ Formula.size φ + 4