Quadratic completeness of semifilter covers

A cover of length t yields an acyclic set circuit with exactly t² charged AND gates. Unions and constants are free. The construction works on arbitrary carriers: at each point, only the t pair coordinates can become true, so t synchronous rounds suffice.

Counting every gate instead, unions and constants included, the circuit over n supplied sets has at most 4 (t + 1)² (n + t + 1) gates: each round reads at most n + t seeds per argument through a union tree.

Main definitions

• Cslib.Circuits.Fusion.PairClosureCompiler.stages: synchronous pair propagation.
• Cslib.Circuits.Fusion.PairCover.toCircuit: an acyclic circuit realizing an unrestricted cover.

Main results

• Cslib.Circuits.Fusion.PairClosureCompiler.readState_stages: t rounds recover the closure.
• Cslib.Circuits.Fusion.PairCover.cost_toCircuit: exactly t² AND gates.
• Cslib.Circuits.Fusion.PairCover.size_toCircuit_le: at most 4 (t + 1)² (n + t + 1) gates.
• Cslib.Circuits.Fusion.PairCover.eval_toCircuit: evaluation gives the target.
• Cslib.Circuits.Fusion.ecomplexityFrom_le_pairCoverComplexity_sq: the minimum AND cost is at most the square of unrestricted cover complexity.

References

• B. P. Cavalar and I. C. Oliveira, Boolean Circuit Complexity and Two-Dimensional Cover Problems, Theorem 24. This formalization uses the native monotone basis with free bottom and top constants, and includes empty inputs and trivial targets.

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

Apply every listed intersection rule to the reconstructed state.

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

Pair values after k synchronous rounds, starting with all pair values empty.

theorem Cslib.Circuits.Fusion.PairClosureCompiler.readState_mono {U : Type u} {n : ℕ} (target : Set U) (input : Fin n → Set U) (pairs : List (Set ↑targetᶜ × Set ↑targetᶜ)) {s t : Fin pairs.length → Set U} (h : s ≤ t) : readState target input pairs s ≤ readState target input pairs t

Reconstruction is monotone in the supplied pair values.

theorem Cslib.Circuits.Fusion.PairClosureCompiler.step_mono {U : Type u} {n : ℕ} (target : Set U) (input : Fin n → Set U) (pairs : List (Set ↑targetᶜ × Set ↑targetᶜ)) : Monotone (step target input pairs)

Pair propagation is monotone.

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

Pair values only grow as rounds proceed.

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

Every point's pair state stabilizes within the number of listed pairs, independently of how many points the carrier contains.

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

All finite propagation stages are contained in the generated pair values.

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

After one round per pair, reconstruction is exactly the generated semifilter closure.

noncomputable def Cslib.Circuits.Fusion.PairClosureCompiler.roundCircuit {U : Type u} {n : ℕ} (target : Set U) (input : Fin n → Set U) (pairs : List (Set ↑targetᶜ × Set ↑targetᶜ)) : Circuit Monotone.signature (n + (pairs.length + 1)) (n + (pairs.length + 1))

Preserve the external inputs while performing one native circuit update.

def Cslib.Circuits.Fusion.PairClosureCompiler.initialCircuit {U : Type u} {n : ℕ} (target : Set U) (pairs : List (Set ↑targetᶜ × Set ↑targetᶜ)) : Circuit Monotone.signature n (n + (pairs.length + 1))

The initial state has the supplied inputs and empty pair coordinates.

noncomputable def Cslib.Circuits.Fusion.PairClosureCompiler.stageCircuit {U : Type u} {n : ℕ} (target : Set U) (input : Fin n → Set U) (pairs : List (Set ↑targetᶜ × Set ↑targetᶜ)) (k : ℕ) : Circuit Monotone.signature n (n + (pairs.length + 1))

Unroll the finite update program, retaining the input wires at every round.

theorem Cslib.Circuits.Fusion.PairClosureCompiler.cost_stageCircuit {U : Type u} {n : ℕ} (target : Set U) (input : Fin n → Set U) (pairs : List (Set ↑targetᶜ × Set ↑targetᶜ)) (k : ℕ) : (stageCircuit target input pairs k).program.cost Monotone.andCost = k * pairs.length

Each propagation round charges one conjunction per listed pair.

theorem Cslib.Circuits.Fusion.PairClosureCompiler.eval_stageCircuit {U : Type u} {n : ℕ} (target : Set U) (input : Fin n → Set U) (pairs : List (Set ↑targetᶜ × Set ↑targetᶜ)) (k : ℕ) : ∃ (output : Set U), (stageCircuit target input pairs k).eval (Monotone.setInterpretation U) input = Fin.append input fun (i : Fin (pairs.length + 1)) => Fin.lastCases output (stages target input pairs k) i

The unrolled program carries the intended pair values; the extra output is a free read from the preceding round and is ignored by all subsequent pair updates.

theorem Cslib.Circuits.Fusion.PairClosureCompiler.size_joinFormula {r : ℕ} (seed : Bool) (fs : List (Formula Monotone.signature r)) : (joinFormula seed fs).size = (List.map (fun (x : Formula Monotone.signature r) => x.size) fs).sum + fs.length + 1

A union tree has one disjunction per argument and its seed constant.

theorem Cslib.Circuits.Fusion.PairClosureCompiler.size_readFormula_le {U : Type u} {n : ℕ} (target : Set U) (input : Fin n → Set U) (pairs : List (Set ↑targetᶜ × Set ↑targetᶜ)) (s : Set ↑targetᶜ) : (readFormula target input pairs s).size ≤ 2 * (n + pairs.length) + 1

Reading a closure coordinate uses at most two gates per input seed and pair value.

theorem Cslib.Circuits.Fusion.PairClosureCompiler.size_updateCircuit_le {U : Type u} {n : ℕ} (target : Set U) (input : Fin n → Set U) (pairs : List (Set ↑targetᶜ × Set ↑targetᶜ)) : (updateCircuit target input pairs).size ≤ (pairs.length + 1) * (4 * (n + pairs.length) + 3)

The update circuit has at most (t + 1) (4 (n + t) + 3) gates for t pairs.

theorem Cslib.Circuits.Fusion.PairClosureCompiler.size_stageCircuit {U : Type u} {n : ℕ} (target : Set U) (input : Fin n → Set U) (pairs : List (Set ↑targetᶜ × Set ↑targetᶜ)) (k : ℕ) : (stageCircuit target input pairs k).size = pairs.length + 1 + k * (updateCircuit target input pairs).size

Each propagation round charges the gates of one update circuit.

noncomputable def Cslib.Circuits.Fusion.PairCover.toCircuit {U : Type u} {n : ℕ} {target : Set U} {input : Fin n → Set U} (c : PairCover target input) : Circuit Monotone.signature n 1

Compile an unrestricted pair cover to an ordinary acyclic set circuit, using one propagation round per pair. Constants and binary unions are free.

@[simp]

theorem Cslib.Circuits.Fusion.PairCover.cost_toCircuit {U : Type u} {n : ℕ} {target : Set U} {input : Fin n → Set U} (c : PairCover target input) : c.toCircuit.program.cost Monotone.andCost = (c.pairs fun (x : Semifilter ↑targetᶜ) => True).length ^ 2

The unrolled cover compiler uses exactly the square of the pair count in AND gates.

@[simp]

theorem Cslib.Circuits.Fusion.PairCover.eval_toCircuit {U : Type u} {n : ℕ} {target : Set U} {input : Fin n → Set U} (c : PairCover target input) : c.toCircuit.eval (Monotone.setInterpretation U) input = fun (x : Fin 1) => target

The acyclic circuit compiled from an unrestricted cover computes its target set.

theorem Cslib.Circuits.Fusion.PairCover.size_toCircuit_le {U : Type u} {n : ℕ} {target : Set U} {input : Fin n → Set U} (c : PairCover target input) : c.toCircuit.size ≤ 4 * ((c.pairs fun (x : Semifilter ↑targetᶜ) => True).length + 1) ^ 2 * (n + (c.pairs fun (x : Semifilter ↑targetᶜ) => True).length + 1)

The compiled circuit of a t-pair cover over n inputs has at most 4 (t + 1)² (n + t + 1) gates in total, counting unions and constants.

theorem Cslib.Circuits.Fusion.PairCover.ecomplexityFrom_le_sq {U : Type u} {n : ℕ} {target : Set U} {input : Fin n → Set U} (c : PairCover target input) : (ecomplexityFrom (Monotone.setInterpretation U) Monotone.andCost (fun (x : Unit) (x_1 : Fin 1) => target) fun (x : Unit) => input) ≤ ↑(c.pairs fun (x : Semifilter ↑targetᶜ) => True).length ^ 2

Every unrestricted pair cover yields a quadratic upper bound for native AND complexity.

theorem Cslib.Circuits.Fusion.ecomplexityFrom_le_pairCoverComplexity_sq {U : Type u} {n : ℕ} (target : Set U) (input : Fin n → Set U) : (ecomplexityFrom (Monotone.setInterpretation U) Monotone.andCost (fun (x : Unit) (x_1 : Fin 1) => target) fun (x : Unit) => input) ≤ pairCoverComplexity target input ^ 2

Quadratic completeness of Fusion, in the native basis with free constants and unions. No assumption on the carrier, target, or input-family size is needed with this convention.