Semifilter bounds for cyclic set circuits

The AND pairs at a cyclic circuit's least solution form a semifilter cover of each designated output. The proof uses fixed-point induction: reference membership at an intermediate state implies observation of the corresponding final value. This predicate is closed under arbitrary unions, while the final AND pairs provide its induction step. Leastness prevents unsupported feedback from manufacturing target points.

Extraction charges every AND equation exactly once, including unused cycles and repeated gates. Constants and OR equations contribute no pairs. Outputs may share a gate or read inputs directly. The bounds support any admissible class of semifilters and transfer to minimum cyclic complexity from arbitrary supplied source functions. This is a semantic construction over sets, with no execution or convergence-time claim. A converse construction from covers is not asserted here.

Main results

• Cslib.Circuits.Fusion.PairCover.ofCyclicCircuit: a cover from a least-fixed-point construction.
• Cslib.Circuits.Fusion.PairCover.length_ofCyclicCircuit: exact preservation of AND cost.
• Cslib.Circuits.Fusion.pairCoverComplexity_le_cyclic_ecomplexityFrom: the minimum-cost bound.

References

• Adapted from LowerBound/Fusion/Cyclic.lean in S. Schlesinger, Algebraic circuit formalizations in Complexitylib.

def Cslib.Circuits.Fusion.cyclicAtoms {σ : Signature} {U : Type v} {n m : ℕ} (c : CyclicCircuit σ n m) (input : Fin n → U) (state : Fin c.size → U) (i : Fin c.size) : Atom σ U

The semantic atoms of the equations at a proposed state.

def Cslib.Circuits.Fusion.PairCover.ofCyclicCircuit {U : Type v} {n m : ℕ} (c : CyclicCircuit Monotone.signature n m) (input : Fin n → Set U) (o : Fin m) {target : Set U} (hc : c.eval (Monotone.setInterpretation U) ⋯ input o = target) (admissible : Semifilter ↑targetᶜ → Prop := fun (x : Semifilter ↑targetᶜ) => True) : PairCover target input admissible

The AND pairs at the least solution defeat every admissible semifilter witness.

@[simp]

theorem Cslib.Circuits.Fusion.PairCover.length_ofCyclicCircuit {U : Type v} {n m : ℕ} (c : CyclicCircuit Monotone.signature n m) (input : Fin n → Set U) (o : Fin m) {target : Set U} (hc : c.eval (Monotone.setInterpretation U) ⋯ input o = target) (admissible : Semifilter ↑targetᶜ → Prop := fun (x : Semifilter ↑targetᶜ) => True) : (ofCyclicCircuit c input o hc admissible).pairs.length = c.cost Monotone.andCost

Extraction retains the exact AND count, including unused cyclic components.

theorem Cslib.Circuits.Fusion.pairCover_lowerBound_cyclic {U : Type v} {n m : ℕ} {target : Set U} {input : Fin n → Set U} {admissible : Semifilter ↑targetᶜ → Prop} {k : ℕ} (hbound : ∀ (c : PairCover target input admissible), k ≤ c.pairs.length) (c : CyclicCircuit Monotone.signature n m) (o : Fin m) (hc : c.eval (Monotone.setInterpretation U) ⋯ input o = target) : k ≤ c.cost Monotone.andCost

A combinatorial pair-cover bound applies to every cyclic construction of the target.

theorem Cslib.Circuits.Fusion.pairCoverComplexity_le_cyclic_cost {U : Type v} {n m : ℕ} {target : Set U} (c : CyclicCircuit Monotone.signature n m) (input : Fin n → Set U) (o : Fin m) (hc : c.eval (Monotone.setInterpretation U) ⋯ input o = target) (admissible : Semifilter ↑targetᶜ → Prop := fun (x : Semifilter ↑targetᶜ) => True) : pairCoverComplexity target input admissible ≤ ↑(c.cost Monotone.andCost)

The minimum pair-cover length bounds the AND cost of any cyclic construction.

theorem Cslib.Circuits.Fusion.pairCoverComplexity_le_cyclic_ecomplexityFrom {U : Type v} {n m : ℕ} {X : Type u_1} (sources : X → Fin n → Set U) (target : X → Fin m → Set U) (x : X) (o : Fin m) (admissible : Semifilter ↑(target x o)ᶜ → Prop := fun (x : Semifilter ↑(target x o)ᶜ) => True) : pairCoverComplexity (target x o) (sources x) admissible ≤ CyclicCircuit.ecomplexityFrom (Monotone.setInterpretation U) ⋯ Monotone.andCost target sources

A cover bound at a supplied source assignment bounds minimum cyclic source complexity.