Finite descriptions of semifilter covers

The quadratic compiler only needs inclusion flags, not the actual subsets in a pair cover. A t-pair cover over n inputs has a description of (2*t+1)*(n+t+1) bits. Decode the flags by synchronous propagation and the target is recovered. This gives an unconditional count of the sets having a small cover, for any fixed supplied input family.

Main definitions

• Cslib.Circuits.Fusion.CoverCode, Cslib.Circuits.Fusion.CoverCode.read, Cslib.Circuits.Fusion.CoverCode.stages, Cslib.Circuits.Fusion.CoverCode.decode: the finite inclusion-pattern description and its staged decoder.
• Cslib.Circuits.Fusion.PairClosureCompiler.coordinate, Cslib.Circuits.Fusion.PairClosureCompiler.encode: encode a pair list into a CoverCode.

Main results

• Cslib.Circuits.Fusion.PairCover.exists_code: every cover admits a finite description.
• Cslib.Circuits.Fusion.card_small_covers_le: a bound on all targets of small cover complexity.

References

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

@[reducible, inline]

abbrev Cslib.Circuits.Fusion.CoverCode (n t : ℕ) : Type

Each of the two operands per pair and the final output records a top flag, an input mask, and a pair-value mask. No ambient subsets occur in this finite description.

def Cslib.Circuits.Fusion.CoverCode.read {U : Type u} {n t : ℕ} (code : CoverCode n t) (input : Fin n → Set U) (state : Fin t → Set U) (i : Fin (t + t + 1)) : Set U

Read one coordinate from its top/input/pair inclusion flags.

def Cslib.Circuits.Fusion.CoverCode.stages {U : Type u} {n t : ℕ} (code : CoverCode n t) (input : Fin n → Set U) : ℕ → Fin t → Set U

Propagate the described pair values from the empty initial state.

def Cslib.Circuits.Fusion.CoverCode.decode {U : Type u} {n t : ℕ} (code : CoverCode n t) (input : Fin n → Set U) : Set U

Decode a description using one propagation round per pair and a final free read.

def Cslib.Circuits.Fusion.PairClosureCompiler.coordinate {U : Type u} (target : Set U) (pairs : List (Set ↑targetᶜ × Set ↑targetᶜ)) : Fin (pairs.length + pairs.length + 1) → Set ↑targetᶜ

The coordinates needed by the finite compiler: two operands per pair, then the empty set.

noncomputable def Cslib.Circuits.Fusion.PairClosureCompiler.encode {U : Type u} {n : ℕ} (target : Set U) (input : Fin n → Set U) (pairs : List (Set ↑targetᶜ × Set ↑targetᶜ)) : CoverCode n pairs.length

Record just the subset tests used in the quadratic compiler.

theorem Cslib.Circuits.Fusion.PairClosureCompiler.decode_encode {U : Type u} {n : ℕ} (target : Set U) (input : Fin n → Set U) (pairs : List (Set ↑targetᶜ × Set ↑targetᶜ)) : (encode target input pairs).decode input = (pairClosure target input pairs) ∅

Decode the original generated closure at its empty coordinate.

theorem Cslib.Circuits.Fusion.PairCover.exists_code {U : Type u} {n : ℕ} {target : Set U} {input : Fin n → Set U} (c : PairCover target input) : ∃ (code : CoverCode n (c.pairs fun (x : Semifilter ↑targetᶜ) => True).length), code.decode input = target

Every cover has a finite description recovering its target.

theorem Cslib.Circuits.Fusion.PairCover.exists_code_of_length_le {U : Type u} {n : ℕ} {target : Set U} {input : Fin n → Set U} (c : PairCover target input) {t : ℕ} (h : (c.pairs fun (x : Semifilter ↑targetᶜ) => True).length ≤ t) : ∃ (code : CoverCode n t), code.decode input = target

A cover fitting a budget has a description of the budget's fixed length.

theorem Cslib.Circuits.Fusion.card_small_covers_le {U : Type u} {n : ℕ} [Fintype U] (input : Fin n → Set U) (t : ℕ) : {target : Set U | pairCoverComplexity target input ≤ ↑t}.card ≤ 2 ^ ((2 * t + 1) * (n + t + 1))

The number of targets with a cover of at most t pairs is at most the number of inclusion-pattern descriptions; no hypothesis about the existence of such descriptions remains.