Constant-depth validation of structure encodings

Check the unary header and express each one-hot constant block as a disjunction of its possible values. Relation bits are unrestricted. The outer conjunction also checks the minimum universe size of two. The depth is at most three and the size is quadratic in universe size for a fixed vocabulary.

def Complexity.DescriptiveComplexity.encodingHeaderFormula (V : Vocabulary) (card : ℕ) : AC0Formula (encodingLength V card)

Check the unary cardinality header, including its false terminator.

Equations

• One or more equations did not get rendered due to their size.

def Complexity.DescriptiveComplexity.constantValueFormula (V : Vocabulary) (card : ℕ) (c : Fin V.numConsts) (a : Fin card) : AC0Formula (encodingLength V card)

Assert that a constant block encodes exactly the specified element.

Equations

• One or more equations did not get rendered due to their size.

def Complexity.DescriptiveComplexity.encodingValidityFormula (V : Vocabulary) (card : ℕ) : AC0Formula (encodingLength V card)

Validate the header, minimum universe size, and every one-hot constant block.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def Complexity.DescriptiveComplexity.encodingValidityPolynomial (V : Vocabulary) : Polynomial ℕ

The exact tree size of the encoding validator as a natural-coefficient polynomial.

Equations

• Complexity.DescriptiveComplexity.encodingValidityPolynomial V = Polynomial.X + Polynomial.C 4 + Polynomial.C V.numConsts * (1 + Polynomial.X * (1 + Polynomial.X))

def Complexity.DescriptiveComplexity.Sentence.validatedExpansion {V : Vocabulary} (φ : Sentence V) (card : ℕ) : AC0Formula (encodingLength V card)

Combine encoding validation with the finite expansion of a sentence.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def Complexity.DescriptiveComplexity.Sentence.validatedPolynomial {V : Vocabulary} (φ : Sentence V) : Polynomial ℕ

Exact size polynomial for validation followed by sentence expansion.

Equations

• φ.validatedPolynomial = 1 + Complexity.DescriptiveComplexity.encodingValidityPolynomial V + Complexity.DescriptiveComplexity.Formula.expansionPolynomial φ