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: the finite inclusion-pattern description.
• Cslib.Circuits.Fusion.CoverCode.decode: recover the output set from a description.

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.

theorem Cslib.Circuits.Fusion.CoverCode.card (n t : ℕ) : Fintype.card (CoverCode n t) = 2 ^ ((2 * t + 1) * (n + t + 1))

The description has exactly (2*t+1)*(n+t+1) independent bits.

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.read_encode {U : Type u} {n : ℕ} (target : Set U) (input : Fin n → Set U) (pairs : List (Set ↑targetᶜ × Set ↑targetᶜ)) (state : Fin pairs.length → Set U) (i : Fin (pairs.length + pairs.length + 1)) : (encode target input pairs).read input state i = (readState target input pairs state) (coordinate target pairs i)

Encoded reads are the original compiler's reconstructed closure coordinates.

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

Encoded propagation agrees with the original compiler at every stage.

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.