A fusion lower bound for the inequality graph

Let N = 2 ^ n. View the inequality relation on Fin N × Fin N as a set generated by its rows and columns. The canonical semi-filter above an unequal pair (u, v) accepts a subset of the diagonal when it contains (u, u) or (v, v).

Every pair in a fusion cover supplies one Boolean bit for each vertex: whether its diagonal point belongs to the left member of the pair. If two vertices had the same complete code, their canonical semi-filter would preserve every pair. Consequently the code is injective, so N ≤ 2 ^ cover.cost. At N = 2 ^ n this gives a lower bound of n AND gates, even when OR gates are free. The matching construction from the literature is not formalized here.

This is the coding form of the canonical-semi-filter argument for the inequality graph in Cavalar--Oliveira, Proposition 40.

def Algebraic.Fusion.Semifilter.twoPoint {U : Type u_1} (left right : U) : Semifilter U

The upward-closed family of sets containing at least one of two points.

Equations

• Algebraic.Fusion.Semifilter.twoPoint left right = { carrier := {set : Set U | left ∈ set ∨ right ∈ set}, nonempty := ⋯, upward := ⋯, empty_not_mem := ⋯ }

@[simp]

theorem Algebraic.Fusion.Semifilter.mem_twoPoint {U : Type u_1} (left right : U) (set : Set U) : set ∈ twoPoint left right ↔ left ∈ set ∨ right ∈ set

theorem Algebraic.Fusion.Semifilter.twoPoint_preservesPair_of_left_iff {U : Type u_1} (left right : U) (pair : Set U × Set U) (same : left ∈ pair.1 ↔ right ∈ pair.1) : (twoPoint left right).PreservesPair pair

If the left member of a pair does not distinguish two points, their two-point semi-filter preserves the pair.

theorem Algebraic.Fusion.Semifilter.twoPoint_isUltra {U : Type u_1} (left right : U) : (twoPoint left right).IsUltra

Every two-point semi-filter is already a semi-ultrafilter: membership of the first point decides between a set and its complement.

@[reducible, inline]

abbrev Algebraic.Fusion.Neq.Ground (N : ℕ) : Type

Ambient space for an N by N bipartite graph.

Equations

• Algebraic.Fusion.Neq.Ground N = (Fin N × Fin N)

def Algebraic.Fusion.Neq.row {N : ℕ} (vertex : Fin N) : Set (Ground N)

The star consisting of one row.

Equations

• Algebraic.Fusion.Neq.row vertex = {edge : Algebraic.Fusion.Neq.Ground N | edge.1 = vertex}

def Algebraic.Fusion.Neq.column {N : ℕ} (vertex : Fin N) : Set (Ground N)

The star consisting of one column.

Equations

• Algebraic.Fusion.Neq.column vertex = {edge : Algebraic.Fusion.Neq.Ground N | edge.2 = vertex}

def Algebraic.Fusion.Neq.target (N : ℕ) : Set (Ground N)

The bipartite inequality graph.

Equations

• Algebraic.Fusion.Neq.target N = {edge : Algebraic.Fusion.Neq.Ground N | edge.1 ≠ edge.2}

@[reducible, inline]

abbrev Algebraic.Fusion.Neq.problem (N : ℕ) : SetProblem (Ground N)

Construct the inequality graph from all row and column stars.

Equations

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

theorem Algebraic.Fusion.Neq.problem_inputs_natAdd {N : ℕ} (vertex : Fin N) : (problem N).inputs (Fin.natAdd N vertex) = column vertex

def Algebraic.Fusion.Neq.diagonal {N : ℕ} (vertex : Fin N) : Problem.Outside (problem N)

A diagonal point, regarded as a point outside the inequality graph.

Equations

• Algebraic.Fusion.Neq.diagonal vertex = ⟨(vertex, vertex), ⋯⟩

@[simp]

theorem Algebraic.Fusion.Neq.diagonal_value {N : ℕ} (vertex : Fin N) : ↑(diagonal vertex) = (vertex, vertex)

@[reducible, inline]

abbrev Algebraic.Fusion.Neq.canonicalFilter {N : ℕ} (left right : Fin N) : Semifilter (Problem.Outside (problem N))

The canonical semi-filter associated with the unequal edge (left, right).

Equations

• Algebraic.Fusion.Neq.canonicalFilter left right = Algebraic.Fusion.Semifilter.twoPoint (Algebraic.Fusion.Neq.diagonal left) (Algebraic.Fusion.Neq.diagonal right)

theorem Algebraic.Fusion.Neq.canonicalFilter_above {N : ℕ} (left right : Fin N) : (canonicalFilter left right).Above (left, right)

The canonical semi-filter is above its corresponding edge.

noncomputable def Algebraic.Fusion.Neq.coverCode {N : ℕ} {admissible : SemifilterClass (problem N)} (cover : PairCover (problem N) admissible) (vertex : Fin N) : Fin cover.pairs.length → Bool

Boolean membership code assigned to a vertex by a pair cover.

Equations

• Algebraic.Fusion.Neq.coverCode cover vertex index = Algebraic.AndOr.membership (Algebraic.Fusion.Neq.diagonal vertex) (cover.pairs.get index).1

theorem Algebraic.Fusion.Neq.coverCode_injective {N : ℕ} {admissible : SemifilterClass (problem N)} (canonicalAdmissible : ∀ (left right : Fin N), left ≠ right → admissible (canonicalFilter left right)) (cover : PairCover (problem N) admissible) : Function.Injective (coverCode cover)

A cover of all semi-filters assigns distinct codes to distinct vertices.

theorem Algebraic.Fusion.Neq.card_le_two_pow_cost_of_canonical {N : ℕ} {admissible : SemifilterClass (problem N)} (canonicalAdmissible : ∀ (left right : Fin N), left ≠ right → admissible (canonicalFilter left right)) (cover : PairCover (problem N) admissible) : N ≤ 2 ^ cover.cost

Information-theoretic lower bound for every witness class containing the canonical semi-filters.

theorem Algebraic.Fusion.Neq.card_le_two_pow_cost {N : ℕ} (cover : PairCover (problem N)) : N ≤ 2 ^ cover.cost

Information-theoretic form of the full semi-filter lower bound.

theorem Algebraic.Fusion.Neq.canonicalFilter_isUltra {N : ℕ} (left right : Fin N) : (canonicalFilter left right).IsUltra

Every canonical semi-filter for the inequality graph is a semi-ultrafilter.

theorem Algebraic.Fusion.Neq.pairCover_cost_lowerBound {n : ℕ} (cover : PairCover (problem (2 ^ n))) : n ≤ cover.cost

Every pair cover of the 2 ^ n-vertex inequality graph has at least n pairs.

theorem Algebraic.Fusion.Neq.ultraPairCover_cost_lowerBound {n : ℕ} (cover : PairCover (problem (2 ^ n)) SemifilterClass.ultra) : n ≤ cover.cost

The same lower bound already holds when covers only need to exclude semi-ultrafilters.

theorem Algebraic.Fusion.Neq.le_pairCoverComplexity (n : ℕ) : ↑n ≤ pairCoverComplexity (problem (2 ^ n))

The full semi-filter cover complexity of the inequality graph is at least n.

theorem Algebraic.Fusion.Neq.le_ultraPairCoverComplexity (n : ℕ) : ↑n ≤ pairCoverComplexity (problem (2 ^ n)) SemifilterClass.ultra

Semi-ultrafilter cover complexity of the inequality graph is also at least n.

theorem Algebraic.Fusion.Neq.and_lowerBound {n : ℕ} (circuit : Circuit AndOr.signature (2 ^ n + 2 ^ n) 1) (constructs : Problem.Constructs (problem (2 ^ n)) circuit (AndOr.setInterpretation (Ground (2 ^ n)))) : n ≤ circuit.cost AndOr.andCost

Any row/column construction of the 2 ^ n-vertex inequality graph uses at least n AND gates, even with free OR gates.

theorem Algebraic.Fusion.Neq.and_lowerBound_via_ultra {n : ℕ} (circuit : Circuit AndOr.signature (2 ^ n + 2 ^ n) 1) (constructs : Problem.Constructs (problem (2 ^ n)) circuit (AndOr.setInterpretation (Ground (2 ^ n)))) : n ≤ circuit.cost AndOr.andCost

The n-AND lower bound can be proved using only semi-ultrafilter witnesses.