Lax Lean Archive

While this submission is a draft, it cannot be used by other submissions.

Proof of `Symmetric formulas for patterns of bounded treedepth`

groundedproofs/Lax461425Proofs/SymVFFormulasForPatterns.lean · lax-461425

What this proof establishes

no assumptions

thm✓Lax461425.FormulasForPatterns

Assuming the claims on the left, the claim on the right holds — checked by the archive's pipeline. Proof code is not displayed here.

Read the Lean proof on GitHub

Description

The homomorphism polynomial of a pattern of treedepth at most tt has a matrix-symmetric formula of orbit size at most nt≤n(t+2)n ^ t ≤ n ^ (t + 2): sum gates over the values of the vertices of an elimination forest, with tagged products of edge variables and child formulas.