Lax Lean Archive

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

Proof of `Symmetric skew circuits from symmetric ABPs`

groundedproofs/Lax461425Proofs/Section6ABPToSkewFamily.lean · lax-461425

What this proof establishes

no assumptions

thm✓Lax461425.SkewFromABP

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

Lemma 6.4. The explicit conversion preserves computation and symmetry, and its gate orbits are bounded by B+B2(n2+1)+1B + B² (n² + 1) + 1 whenever the ABP vertex orbits are bounded by BB.