A logarithmic ceiling for canonical graph semi-filters

For a bipartite graph G, the canonical semi-filter at an edge (u, v) is the upward closure of its complementary row and complementary column. Both must be nonempty. A random pair consisting of a union of rows and a union of columns violates this semi-filter with probability at least 1 / 16.

Consequently, on 2 ^ n vertices per side, 32 * n pairs cover every canonical semi-filter. This is an upper bound for this restricted witness class, not for full Fusion cover complexity or circuit size. In particular, canonical graph semi-filters cannot establish the super-logarithmic graph cover bound needed for a superlinear Boolean circuit lower bound.

The definition of canonical semi-filters is from Section 4.2 of:

• B. Cavalar and I. C. Oliveira, Boolean Circuit Complexity and Two-Dimensional Cover Problems (2025), https://arxiv.org/abs/2503.14117.

The probabilistic upper bound below is proved here; no priority claim is made.

@[reducible, inline]

abbrev Algebraic.Fusion.Graph.problem {N : ℕ} (graph : Set (Fin N × Fin N)) : SetProblem (Fin N × Fin N)

A graph construction problem with all rows and columns as generators.

Equations

• One or more equations did not get rendered due to their size.

def Algebraic.Fusion.Graph.outsideRow {N : ℕ} (graph : Set (Fin N × Fin N)) (row : Fin N) : Set (Problem.Outside (problem graph))

The part of a row outside the graph.

Equations

• Algebraic.Fusion.Graph.outsideRow graph row = {edge : Algebraic.Fusion.Problem.Outside (Algebraic.Fusion.Graph.problem graph) | (↑edge).1 = row}

def Algebraic.Fusion.Graph.outsideColumn {N : ℕ} (graph : Set (Fin N × Fin N)) (column : Fin N) : Set (Problem.Outside (problem graph))

The part of a column outside the graph.

Equations

• Algebraic.Fusion.Graph.outsideColumn graph column = {edge : Algebraic.Fusion.Problem.Outside (Algebraic.Fusion.Graph.problem graph) | (↑edge).2 = column}

def Algebraic.Fusion.Graph.CanonicalEdge {N : ℕ} (graph : Set (Fin N × Fin N)) : Type

Edges whose complementary row and column are both nonempty.

Equations

• Algebraic.Fusion.Graph.CanonicalEdge graph = { edge : Fin N × Fin N // edge ∈ graph ∧ (∃ (column : Fin N), (edge.1, column) ∉ graph) ∧ ∃ (row : Fin N), (row, edge.2) ∉ graph }

@[instance_reducible]

noncomputable instance Algebraic.Fusion.Graph.instFintypeCanonicalEdge {N : ℕ} (graph : Set (Fin N × Fin N)) : Fintype (CanonicalEdge graph)

Equations

• Algebraic.Fusion.Graph.instFintypeCanonicalEdge graph = id inferInstance

noncomputable def Algebraic.Fusion.Graph.CanonicalEdge.rowWitness {N : ℕ} {graph : Set (Fin N × Fin N)} (edge : CanonicalEdge graph) : Fin N

A canonical edge supplies a nonedge in its row.

Equations

• edge.rowWitness = ⋯.choose

noncomputable def Algebraic.Fusion.Graph.CanonicalEdge.columnWitness {N : ℕ} {graph : Set (Fin N × Fin N)} (edge : CanonicalEdge graph) : Fin N

A canonical edge supplies a nonedge in its column.

Equations

• edge.columnWitness = ⋯.choose

def Algebraic.Fusion.Graph.canonicalFilter {N : ℕ} (graph : Set (Fin N × Fin N)) (edge : CanonicalEdge graph) : Semifilter (Problem.Outside (problem graph))

Upward closure of the complementary row and column of a graph edge.

Equations

• One or more equations did not get rendered due to their size.

theorem Algebraic.Fusion.Graph.canonicalFilter_above {N : ℕ} (graph : Set (Fin N × Fin N)) (edge : CanonicalEdge graph) : (canonicalFilter graph edge).Above ↑edge

The canonical semi-filter is above the edge that defines it.

def Algebraic.Fusion.Graph.canonicalClass {N : ℕ} (graph : Set (Fin N × Fin N)) : SemifilterClass (problem graph)

Restrict admissible witnesses to canonical graph semi-filters.

Equations

• Algebraic.Fusion.Graph.canonicalClass graph filter = ∃ (edge : Algebraic.Fusion.Graph.CanonicalEdge graph), filter = Algebraic.Fusion.Graph.canonicalFilter graph edge

@[reducible, inline]

abbrev Algebraic.Fusion.Graph.Coloring (N : ℕ) : Type

Independently choose a set of row labels and a set of column labels.

Equations

• Algebraic.Fusion.Graph.Coloring N = ((Fin N → Bool) × (Fin N → Bool))

def Algebraic.Fusion.Graph.colorPair {N : ℕ} (graph : Set (Fin N × Fin N)) (color : Coloring N) : Pair (problem graph)

The fusion pair associated with a row/column coloring.

Equations

• One or more equations did not get rendered due to their size.

def Algebraic.Fusion.Graph.hits {N : ℕ} (graph : Set (Fin N × Fin N)) (color : Coloring N) (edge : CanonicalEdge graph) : Prop

Four prescribed color bits suffice to violate a canonical semi-filter.

Equations

• Algebraic.Fusion.Graph.hits graph color edge = (color.1 (↑edge).1 = true ∧ color.1 edge.columnWitness = false ∧ color.2 (↑edge).2 = true ∧ color.2 edge.rowWitness = false)

@[instance_reducible]

noncomputable instance Algebraic.Fusion.Graph.instDecidableRelColoringCanonicalEdgeHits {N : ℕ} (graph : Set (Fin N × Fin N)) : DecidableRel (hits graph)

Equations

• Algebraic.Fusion.Graph.instDecidableRelColoringCanonicalEdgeHits graph color edge = id inferInstance

theorem Algebraic.Fusion.Graph.not_preservesPair_of_hits {N : ℕ} (graph : Set (Fin N × Fin N)) (color : Coloring N) (edge : CanonicalEdge graph) (hit : hits graph color edge) : ¬(canonicalFilter graph edge).PreservesPair (colorPair graph color)

A hit makes both members accepted but their intersection rejected.

theorem Algebraic.Fusion.Graph.sixteen_mul_misses_le {N : ℕ} (graph : Set (Fin N × Fin N)) (edge : CanonicalEdge graph) : 16 * Fintype.card { color : Coloring N // ¬hits graph color edge } ≤ 15 * Fintype.card (Coloring N)

At most fifteen sixteenths of all row/column colorings miss a fixed edge.

theorem Algebraic.Fusion.Graph.sampling_bound {n : ℕ} (positive : 0 < n) : (2 ^ n) ^ 2 * 15 ^ (32 * n) < 16 ^ (32 * n)

32 * n independent samples suffice for at most (2 ^ n)^2 obligations.

theorem Algebraic.Fusion.Graph.exists_canonical_cover {n : ℕ} (positive : 0 < n) (graph : Set (Fin (2 ^ n) × Fin (2 ^ n))) : ∃ (cover : PairCover (problem graph) (canonicalClass graph)), cover.cost = 32 * n

Every graph has a logarithmic cover of all its canonical semi-filters.

theorem Algebraic.Fusion.Graph.canonical_coverComplexity_le {n : ℕ} (positive : 0 < n) (graph : Set (Fin (2 ^ n) × Fin (2 ^ n))) : pairCoverComplexity (problem graph) (canonicalClass graph) ≤ ↑(32 * n)

Restricted canonical cover complexity is at most linear in the binary label length, uniformly over the graph. This does not bound full cover complexity.