Lax Lean Archive

Proof of `Monadically dependent classes exclude large φ-patterns`

groundedproofs/Lax185574Proofs/ForbiddenPhiPatterns.lean · lax-185574

What this proof establishes

cor✓Lax185574.ForbiddenPhiPatterns

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 23 of this submission's paper

Description

A φφ-pattern is a (φ,E)(φ, E)-pattern or a (φ,¬E)(φ, ¬E)-pattern. Take the larger of the two bounds of the lemma on (φ,ψ)(φ, ψ)-patterns, and use that a pattern contains patterns of all smaller orders.

The argument is carried out for the graph classes of the archive and their monadic dependence, and transferred to the graph classes used here.