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.

Read the Lean proof on GitHub

In the paper

  • page 20 of this submission's paper

Description

A flip for a partition into at most pp parts is obtained from the original graph by a fixed transduction: color the parts with pp 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 ss-definable flip is a flip for the partition into atomic types over at most ss vertices, which has at most 3s3^s 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.