Proof of `Definable flips preserve monadic dependence`
groundedproofs/Lax185574Proofs/FlipsMonadicallyDependent.lean · lax-185574
What this proof establishes
no assumptions
Assuming the claims on the left, the claim on the right holds — checked by the archive's pipeline. Proof code is not displayed here.
In the paper
- page 20 of this submission's paper
Description
A flip for a partition into at most parts is obtained from the original graph by a fixed transduction: color the parts with unary predicates and flip the adjacency between the chosen pairs of colors. This bounded-flip image of a class is transduced by it, and monadic dependence is preserved under transductions. Every -definable flip is a flip for the partition into atomic types over at most vertices, which has at most parts.
The argument is carried out for the graph classes of the archive and their monadic dependence, and transferred to the graph classes used here.