Proof of `Characterisation of matrix-symmetric skew circuits` (1st statement)
groundedproofs/Lax461425Proofs/Section6Characterisation.lean · lax-461425
What this proof establishes
Assuming the claims on the left, the claim on the right holds — checked by the archive's pipeline. Proof code is not displayed here.
Description
The forward direction is the pathwidth refinement of the support theorem, with finite exceptions absorbed by homomorphism spanning and the zero-dimensional index spanned by the empty pattern. The backward direction builds symmetric ABPs and converts them to skew circuits (Lemma 6.4).