Linear cover complexity of random bipartite graphs

Every graph on N vertices per side has an unrestricted pair cover of length N. In the uniform distribution over all 2^(N²) such graphs, covers of length at most N/16 have probability at most 2⁻ᴺ, for N ≥ 16. The proof counts inclusion-pattern descriptions; it makes no unproved assumption about graph encodability or incompressibility.

Main definitions

• Cslib.Circuits.Fusion.Graph.rowCover: a worst-case cover with one pair per row.
• Cslib.Circuits.Fusion.Graph.smallCoverProbability: uniform probability of a small cover.

Main results

• Cslib.Circuits.Fusion.Graph.pairCoverComplexity_le_card: the matching linear upper bound.
• Cslib.Circuits.Fusion.Graph.smallCoverProbability_le: the explicit finite counting bound.
• Cslib.Circuits.Fusion.Graph.random_cover_complexity: the quantitative high-probability bound.

References

• B. P. Cavalar and I. C. Oliveira, Boolean Circuit Complexity and Two-Dimensional Cover Problems, Theorem 37.

def Cslib.Circuits.Fusion.Graph.rowPairs {V : Type u_1} [Fintype V] (graph : Set (V × V)) : Fin (Fintype.card V) → Set ↑graphᶜ × Set ↑graphᶜ

Pair each row with the columns neighboring that row, restricted to the graph complement.

def Cslib.Circuits.Fusion.Graph.rowCover {V : Type u_1} [Fintype V] (graph : Set (V × V)) : PairCover graph sources

Every bipartite graph has a cover with one pair per row.

@[simp]

theorem Cslib.Circuits.Fusion.Graph.length_rowCover {V : Type u_1} [Fintype V] (graph : Set (V × V)) : ((rowCover graph).pairs fun (x : Semifilter ↑graphᶜ) => True).length = Fintype.card V

The row cover charges exactly one pair for each vertex on the left.

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

The worst-case graph cover complexity is at most the number of rows, including zero.

noncomputable def Cslib.Circuits.Fusion.Graph.smallCoverProbability (N t : ℕ) : ℝ

Probability that a uniformly chosen labelled bipartite graph has cover complexity at most t. All graphs are equally likely; the two vertex sets are both Fin N.

theorem Cslib.Circuits.Fusion.Graph.smallCoverProbability_le (N t : ℕ) : smallCoverProbability N t ≤ 2 ^ ((2 * t + 1) * (2 * N + t + 1)) / 2 ^ N ^ 2

Explicit finite counting bound for uniform labelled bipartite graphs.

theorem Cslib.Circuits.Fusion.Graph.smallCoverProbability_le_half_pow {N : ℕ} (hN : 16 ≤ N) : smallCoverProbability N (N / 16) ≤ (1 / 2) ^ N

A linear budget N/16 fails except with probability at most 2⁻ᴺ, once N ≥ 16.

theorem Cslib.Circuits.Fusion.Graph.random_cover_complexity {N : ℕ} (hN : 16 ≤ N) : 1 - (1 / 2) ^ N ≤ ((Probability.PMF.uniformOfFintype (Set (Fin N × Fin N))).toOuterMeasure {graph : Set (Fin N × Fin N) | ↑(N / 16) < pairCoverComplexity graph sources ∧ pairCoverComplexity graph sources ≤ ↑N}).toReal

Random graph cover complexity is linear. With probability at least 1 - 2⁻ᴺ, a uniform labelled N-by-N bipartite graph has cover complexity strictly above ⌊N/16⌋ and at most N. This is a finite quantitative form of Theorem 37.