Exact cover complexity of the inequality graph

The complement of the inequality graph is its diagonal. Its canonical semifilter at (u,v) accepts a set exactly when it contains (u,u) or (v,v). Any pair defeating this semifilter distinguishes these diagonal points by membership in its first component. Thus a cover of length k injectively labels the vertices by k bits. For n-bit vertices this forces n ≤ k.

Main definitions

• Cslib.Circuits.Fusion.Graph.inequality: the bipartite graph of unequal vertex labels.
• Cslib.Circuits.Fusion.Graph.diagonal: a diagonal point of its complement.

Main results

• Cslib.Circuits.Fusion.Graph.le_length_inequality: every canonical cover has at least n pairs.
• Cslib.Circuits.Fusion.Graph.exists_inequality_circuit: a native circuit with n AND gates.
• Cslib.Circuits.Fusion.Graph.inequality_complexities: all three complexities equal n, including the empty graph at n = 0.

References

• B. P. Cavalar and I. C. Oliveira, Boolean Circuit Complexity and Two-Dimensional Cover Problems, Proposition 40. The injective-label proof below is an equivalent counting argument on the diagonal.

def Cslib.Circuits.Fusion.Graph.inequality (V : Type u_2) : Set (V × V)

The bipartite inequality graph.

def Cslib.Circuits.Fusion.Graph.diagonal {V : Type u_1} (v : V) : ↑(inequality V)ᶜ

A diagonal pair is outside the inequality graph.

def Cslib.Circuits.Fusion.Graph.inequalityEdge {V : Type u_1} (u v : V) (h : u ≠ v) : CanonicalEdge (inequality V)

Every inequality edge has nonempty complementary row and column.

theorem Cslib.Circuits.Fusion.Graph.canonicalFilter_inequality {V : Type u_1} (u v : V) (h : u ≠ v) (s : Set ↑(inequality V)ᶜ) : (canonicalFilter (inequality V) (inequalityEdge u v h)) s ↔ diagonal u ∈ s ∨ diagonal v ∈ s

On the diagonal, canonical semifilters accept membership of either endpoint.

theorem Cslib.Circuits.Fusion.Graph.canonicalFilter_inequality_isUltra {V : Type u_1} (u v : V) (h : u ≠ v) : (canonicalFilter (inequality V) (inequalityEdge u v h)).IsUltra

Canonical inequality semifilters are semi-ultrafilters (Proposition 47's witness fact).

theorem Cslib.Circuits.Fusion.Graph.inequality_signature_injective {V : Type u_1} [Fintype V] (c : PairCover (inequality V) sources (canonicalClass (inequality V))) : Function.Injective fun (v : V) (i : Fin c.pairs.length) => c.pairs[↑i].1.boolIndicator (diagonal v)

The first components of a canonical cover give distinct bit signatures to distinct vertices.

theorem Cslib.Circuits.Fusion.Graph.card_le_two_pow_length_inequality {V : Type u_1} [Fintype V] (c : PairCover (inequality V) sources (canonicalClass (inequality V))) : Fintype.card V ≤ 2 ^ c.pairs.length

A canonical cover needs enough bit signatures to label all vertices.

theorem Cslib.Circuits.Fusion.Graph.le_length_inequality {n : ℕ} (c : PairCover (inequality (Fin n → Bool)) sources (canonicalClass (inequality (Fin n → Bool)))) : n ≤ c.pairs.length

Every canonical cover of inequality on 2^n vertices has at least n pairs.

theorem Cslib.Circuits.Fusion.Graph.exists_inequality_circuit (n : ℕ) : ∃ (c : Circuit Monotone.signature (Fintype.card (Fin n → Bool) + Fintype.card (Fin n → Bool)) 1), c.eval (Monotone.setInterpretation ((Fin n → Bool) × (Fin n → Bool))) sources 0 = inequality (Fin n → Bool) ∧ c.program.cost Monotone.andCost = n

Inequality of two n-bit vertices is constructed with exactly n AND gates. All supplied rows/columns, constants and OR gates are free for this cost. Includes n = 0.

theorem Cslib.Circuits.Fusion.Graph.inequality_complexities (n : ℕ) : pairCoverComplexity (inequality (Fin n → Bool)) sources (canonicalClass (inequality (Fin n → Bool))) = ↑n ∧ pairCoverComplexity (inequality (Fin n → Bool)) sources = ↑n ∧ (ecomplexityFrom (Monotone.setInterpretation ((Fin n → Bool) × (Fin n → Bool))) Monotone.andCost (fun (x : Unit) (x_1 : Fin 1) => inequality (Fin n → Bool)) fun (x : Unit) => sources) = ↑n

Proposition 40: canonical cover, full cover, and intersection complexity of inequality on 2^n vertices per side all equal n.