Compiling semifilter covers to binary cyclic circuits

The generated closure of a finite pair list can be reconstructed from the input sets and the listed pair intersections. Compile their update equations as ordinary native formulas, then close the state inputs with Circuit.feedback. Each pair occurrence contributes exactly one AND gate; all other operations are free binary ORs and constants. The final output reconstructs the empty-index closure, hence the target of an unrestricted cover.

This finite presentation works on arbitrary carriers, including infinite ones. It does not enumerate the subsets of the target complement or require the input sets to cover the carrier: the monotone basis already supplies a free top constant. Selecting the active seeds uses classical subset tests, so this is a noncomputable construction with least-fixed-point semantics, not an efficient compiler or an iteration bound. The converse concerns unrestricted semifilters; the forward lower bound also allows restricted witness classes.

Main definitions

• Cslib.Circuits.Fusion.PairClosureCompiler.readState: reconstruct a closure coordinate from finitely many input and pair values.
• Cslib.Circuits.Fusion.PairCover.toCyclic: a finite binary circuit realizing a pair cover.

Main results

• Cslib.Circuits.Fusion.PairCover.eval_toCyclic: the circuit's least solution is its target.
• Cslib.Circuits.Fusion.PairCover.cost_toCyclic: its AND cost is exactly the pair-list length.
• Cslib.Circuits.Fusion.pairCoverComplexity_eq_cyclic_ecomplexityFrom: unrestricted pair-cover complexity equals cyclic AND complexity from the supplied inputs, with free ORs and constants.

References

• Reworks the finite compiler, binary lowering and completeness argument in LowerBound/Fusion/Cyclic/{Compiler,LowerJoinMeet,Complete}.lean of S. Schlesinger, Algebraic circuit formalizations in Complexitylib. The finite presentation here uses only pair values, instead of all complement subsets.

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

Reconstruct a closure state from the finite input seeds and listed pair intersections.

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

The intended pair values are intersections in the generated closure.

theorem Cslib.Circuits.Fusion.PairClosureCompiler.pairClosure_le_readState {U : Type u} {n : ℕ} (target : Set U) (input : Fin n → Set U) (pairs : List (Set ↑targetᶜ × Set ↑targetᶜ)) (state : Fin pairs.length → Set U) (hstate : ∀ (j : Fin pairs.length), (readState target input pairs state) (pairs.get j).1 ∩ (readState target input pairs state) (pairs.get j).2 ⊆ state j) : pairClosure target input pairs ≤ readState target input pairs state

A pair state closed under its reconstructed intersections contains all derivations.

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

Only the listed pair values are needed to reconstruct the whole generated closure.

def Cslib.Circuits.Fusion.PairClosureCompiler.joinFormula {r : ℕ} (seed : Bool) : List (Formula Monotone.signature r) → Formula Monotone.signature r

A binary union tree with a constant seed; it contains no charged conjunctions of its own.

theorem Cslib.Circuits.Fusion.PairClosureCompiler.cost_joinFormula {r : ℕ} (seed : Bool) (fs : List (Formula Monotone.signature r)) : Formula.cost Monotone.andCost (joinFormula seed fs) = (List.map (fun (x : Formula Monotone.signature r) => Formula.cost Monotone.andCost x) fs).sum

The union tree charges exactly the conjunctions in its arguments.

theorem Cslib.Circuits.Fusion.PairClosureCompiler.mem_eval_joinFormula {U : Type u} {r : ℕ} (seed : Bool) (fs : List (Formula Monotone.signature r)) (values : Fin r → Set U) (point : U) : point ∈ (joinFormula seed fs).eval (Monotone.setInterpretation U) values ↔ seed = true ∨ ∃ f ∈ fs, point ∈ f.eval (Monotone.setInterpretation U) values

Membership in a union tree is membership in its seed or one of its arguments.

theorem Cslib.Circuits.Fusion.PairClosureCompiler.joinFormula_isGate {r : ℕ} (seed : Bool) (fs : List (Formula Monotone.signature r)) : ∃ (op : Monotone.signature.Op) (args : Fin (Monotone.signature.Arity op) → Formula Monotone.signature r), joinFormula seed fs = Formula.gate op args

Every union tree has an operation at its root, including the empty tree.

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

A free union of the active input seeds and pair values at a requested complement subset.

theorem Cslib.Circuits.Fusion.PairClosureCompiler.cost_readFormula {U : Type u} {n : ℕ} (target : Set U) (input : Fin n → Set U) (pairs : List (Set ↑targetᶜ × Set ↑targetᶜ)) (s : Set ↑targetᶜ) : Formula.cost Monotone.andCost (readFormula target input pairs s) = 0

Reading a closure coordinate needs only free union and constant gates.

theorem Cslib.Circuits.Fusion.PairClosureCompiler.eval_readFormula {U : Type u} {n : ℕ} (target : Set U) (input : Fin n → Set U) (pairs : List (Set ↑targetᶜ × Set ↑targetᶜ)) (s : Set ↑targetᶜ) (state : Fin (pairs.length + 1) → Set U) : (readFormula target input pairs s).eval (Monotone.setInterpretation U) (Fin.append input state) = (readState target input pairs (state ∘ Fin.castSucc)) s

The ordinary formula evaluates to the finite presentation of the closure state.

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

One conjunction for each pair, followed by the reconstructed empty-index output.

noncomputable def Cslib.Circuits.Fusion.PairClosureCompiler.updateCircuit {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)) (pairs.length + 1)

Compile each update formula using the existing native formula compiler.

theorem Cslib.Circuits.Fusion.PairClosureCompiler.updateCircuit_outputs {U : Type u} {n : ℕ} (target : Set U) (input : Fin n → Set U) (pairs : List (Set ↑targetᶜ × Set ↑targetᶜ)) (i : Fin (pairs.length + 1)) : ∃ (j : Fin (updateCircuit target input pairs).size), (updateCircuit target input pairs).outputs i = Wire.gate j

Every compiled update output is an internal gate, so closing feedback adds no operations.

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

The update uses exactly one charged conjunction per listed pair occurrence.

theorem Cslib.Circuits.Fusion.PairClosureCompiler.eval_updateCircuit {U : Type u} {n : ℕ} (target : Set U) (input : Fin n → Set U) (pairs : List (Set ↑targetᶜ × Set ↑targetᶜ)) (state : Fin (pairs.length + 1) → Set U) : (updateCircuit target input pairs).eval (Monotone.setInterpretation U) (Fin.append input state) = fun (i : Fin (pairs.length + 1)) => Fin.lastCases ((readState target input pairs (state ∘ Fin.castSucc)) ∅) (fun (j : Fin pairs.length) => (readState target input pairs (state ∘ Fin.castSucc)) (pairs.get j).1 ∩ (readState target input pairs (state ∘ Fin.castSucc)) (pairs.get j).2) i

The native update program computes the finite closure equations.

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

Close the finite update program by feeding its outputs back into its state inputs.

@[simp]

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

Closing feedback preserves the exact number of listed pair occurrences.

theorem Cslib.Circuits.Fusion.PairClosureCompiler.eval_circuit {U : Type u} {n : ℕ} (target : Set U) (input : Fin n → Set U) (pairs : List (Set ↑targetᶜ × Set ↑targetᶜ)) : (circuit target input pairs).eval (Monotone.setInterpretation U) ⋯ input = fun (i : Fin (pairs.length + 1)) => Fin.lastCases ((pairClosure target input pairs) ∅) (pairValues target input pairs) i

The finite circuit reconstructs every listed pair value and the empty-index closure.

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

Realize an unrestricted pair cover by a finite binary cyclic circuit. The subset tests selecting its free unions are noncomputable on arbitrary carriers.

@[simp]

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

The compiled cover charges exactly one conjunction per pair occurrence.

@[simp]

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

The least solution of the compiled unrestricted cover is exactly its target.

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

Unrestricted semifilter cover complexity is exactly binary cyclic AND complexity, with free unions and constants, on arbitrary carriers and supplied input sets.