Canonical graph semifilters

A canonical semifilter is the upward closure of a complementary row and complementary column at an edge. Both complementary sets must be nonempty. This restricted witness class gives a lower bound on unrestricted graph cover complexity.

Main definitions

• Cslib.Circuits.Fusion.Graph.CanonicalEdge: edges with nonempty complementary row and column.
• Cslib.Circuits.Fusion.Graph.canonicalFilter: the corresponding semifilter.
• Cslib.Circuits.Fusion.Graph.canonicalClass: the class of canonical semifilters.

Main results

• Cslib.Circuits.Fusion.Graph.canonicalWitness: a canonical semifilter is a graph witness.
• Cslib.Circuits.Fusion.Graph.canonical_pairCoverComplexity_le: restricting witnesses lowers cover complexity.

References

• B. P. Cavalar and I. C. Oliveira, Boolean Circuit Complexity and Two-Dimensional Cover Problems, Section 4.2.
• Adapted from LowerBound/Fusion/Graph/Canonical.lean in S. Schlesinger, Algebraic circuit formalizations in Complexitylib.

def Cslib.Circuits.Fusion.Graph.outsideRow {V : Type u_1} (graph : Set (V × V)) (v : V) : Set ↑graphᶜ

The part of a row outside the graph.

def Cslib.Circuits.Fusion.Graph.outsideColumn {V : Type u_1} (graph : Set (V × V)) (v : V) : Set ↑graphᶜ

The part of a column outside the graph.

def Cslib.Circuits.Fusion.Graph.CanonicalEdge {V : Type u_1} (graph : Set (V × V)) : Type u_1

Edges whose complementary row and column are both nonempty.

def Cslib.Circuits.Fusion.Graph.canonicalFilter {V : Type u_1} (graph : Set (V × V)) (e : CanonicalEdge graph) : Semifilter ↑graphᶜ

Upward closure of the complementary row and column at an edge.

def Cslib.Circuits.Fusion.Graph.canonicalClass {V : Type u_1} (graph : Set (V × V)) (F : Semifilter ↑graphᶜ) : Prop

Restrict witnesses to canonical graph semifilters.

def Cslib.Circuits.Fusion.Graph.canonicalWitness {V : Type u_1} [Fintype V] (graph : Set (V × V)) (e : CanonicalEdge graph) : SemifilterWitness graph sources (canonicalClass graph)

A canonical semifilter lies above the edge defining it.

theorem Cslib.Circuits.Fusion.Graph.canonical_pairCoverComplexity_le {V : Type u_1} [Fintype V] (graph : Set (V × V)) : pairCoverComplexity graph sources (canonicalClass graph) ≤ pairCoverComplexity graph sources

Canonical witnesses form a subclass of unrestricted graph witnesses.