Semifilter covers of monotone set constructions

A semifilter is a monotone predicate on sets accepting the full set and rejecting the empty set. Mathlib's BoundedOrderHom (Set U) Prop supplies exactly this structure. Intersection closure is not required: accepting two sets need not imply accepting their intersection.

For a target set and supplied input sets, witnesses consist of a target point and an admissible semifilter on the target complement. The semifilter accepts every restricted input containing the point. A pair cover defeats all such witnesses: each witness accepts both members of some pair but rejects their intersection. The admissibility predicate supports both unrestricted semifilters and the complementary-set condition Semifilter.IsUltra.

Every native monotone circuit producing the target at a designated output yields a pair cover whose length is exactly its number of AND gates. Constants and OR gates contribute no pairs; repeated and unused AND gates remain charged. The circuit may have other outputs. Empty witness classes admit empty covers, so positive lower bounds require a nontrivial combinatorial argument. The set interpretation and cover extraction are mathematical constructions, with no claim of efficient execution on an encoding of arbitrary sets.

Main definitions

• Cslib.Circuits.Fusion.Semifilter: a bounded order map from sets to propositions.
• Cslib.Circuits.Fusion.SemifilterWitness: an admissible observation of a target point.
• Cslib.Circuits.Fusion.PairCover: a list of intersection pairs defeating all witnesses.
• Cslib.Circuits.Fusion.pairCoverComplexity: the minimum pair count, or infinity.

Main results

• Cslib.Circuits.Fusion.PairCover.length_ofCircuit: extraction preserves the exact AND count.
• Cslib.Circuits.Fusion.pairCoverComplexity_le_of_sourceRefinement: pointwise source refinement transfers cover lower bounds without changing the pair list.
• Cslib.Circuits.Fusion.pairCoverComplexity_le_cost: cover complexity bounds every construction.
• Cslib.Circuits.Fusion.pairCoverComplexity_le_ecomplexityFrom: the bound for native source complexity.

References

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

@[reducible, inline]

abbrev Cslib.Circuits.Fusion.Semifilter (U : Type u) : Type u

A nontrivial upward-closed family of sets, written as its membership predicate. This imposes no intersection-closure condition.

@[simp]

theorem Cslib.Circuits.Fusion.Semifilter.apply_univ {U : Type u} (F : Semifilter U) : F Set.univ

@[simp]

theorem Cslib.Circuits.Fusion.Semifilter.not_apply_empty {U : Type u} (F : Semifilter U) : ¬F ∅

def Cslib.Circuits.Fusion.Semifilter.IsUltra {U : Type u} (F : Semifilter U) : Prop

Every set or its complement is accepted. At least one is required; both may be accepted.

def Cslib.Circuits.Fusion.Semifilter.PreservesPair {U : Type u} (F : Semifilter U) (p : Set U × Set U) : Prop

Accepting both members of this pair implies accepting their intersection.

def Cslib.Circuits.Fusion.Atom.andPair? {U : Type u} {V : Type v} (a : Atom Monotone.signature (Set U)) (f : V → U) : Option (Set V × Set V)

Restrict the two arguments of an AND atom along a carrier map. Other gates yield no pair.

theorem Cslib.Circuits.Fusion.Atom.semifilter_of_mem {U : Type u} {V : Type v} (a : Atom Monotone.signature (Set U)) (f : V → U) (x : U) (F : Semifilter V) (hp : ∀ (p : Set V × Set V), a.andPair? f = some p → F.PreservesPair p) (args : Fin (Monotone.signature.Arity a.op) → Set U) (hs : ∀ (i : Fin (Monotone.signature.Arity a.op)), x ∈ args i → F (f ⁻¹' a.arguments i)) : x ∈ Monotone.setInterpretation U a.op args → F (f ⁻¹' Monotone.setInterpretation U a.op a.arguments)

Reference membership in one tuple implies observation of the result on another tuple, provided the observation preserves its AND pair. No subset relation between tuples is needed.

theorem Cslib.Circuits.Fusion.Atom.preserves_semifilter {U : Type u} {V : Type v} (a : Atom Monotone.signature (Set U)) (f : V → U) (x : U) (F : Semifilter V) (hp : ∀ (p : Set V × Set V), a.andPair? f = some p → F.PreservesPair p) : a.Preserves (Monotone.setInterpretation U) fun (s : Set U) => x ∈ s → F (f ⁻¹' s)

A semifilter preserves the reference-to-observation predicate when it preserves the AND pair. Constants and unions preserve that predicate without any extra assumption.

structure Cslib.Circuits.Fusion.SemifilterWitness {U : Type u} {n : ℕ} (target : Set U) (input : Fin n → Set U) (admissible : Semifilter ↑targetᶜ → Prop := fun (x : Semifilter ↑targetᶜ) => True) : Type u

A target point and an admissible semifilter accepting the inputs containing that point.

• point : ↑target

  Distinguished target point.

• filter : Semifilter ↑targetᶜ

  Observation of sets outside the target.

• admissible_filter : admissible self.filter

  The observation belongs to the chosen class.

• above (i : Fin n) : ↑self.point ∈ input i → self.filter (Subtype.val ⁻¹' input i)

  Every supplied set containing the point is accepted after restriction.

def Cslib.Circuits.Fusion.SemifilterWitness.predicate {U : Type u} {n : ℕ} {target : Set U} {input : Fin n → Set U} {admissible : Semifilter ↑targetᶜ → Prop} (w : SemifilterWitness target input admissible) (s : Set U) : Prop

Reference membership implies acceptance by the observation outside the target.

theorem Cslib.Circuits.Fusion.SemifilterWitness.not_predicate_target {U : Type u} {n : ℕ} {target : Set U} {input : Fin n → Set U} {admissible : Semifilter ↑targetᶜ → Prop} (w : SemifilterWitness target input admissible) : ¬w.predicate target

The target contains the reference point but has empty restriction to its complement.

structure Cslib.Circuits.Fusion.PairCover {U : Type u} {n : ℕ} (target : Set U) (input : Fin n → Set U) (admissible : Semifilter ↑targetᶜ → Prop := fun (x : Semifilter ↑targetᶜ) => True) : Type u

A finite list of pairs defeating every admissible observation of a target point. Repetitions are retained and charged separately.

• pairs : List (Set ↑targetᶜ × Set ↑targetᶜ)

  The intersection pairs, all over the target complement.

• isCover (w : SemifilterWitness target input admissible) : ¬∀ p ∈ self.pairs, w.filter.PreservesPair p

  Every witness fails to preserve some listed pair.

def Cslib.Circuits.Fusion.PairCover.pad {U : Type u} {n : ℕ} {target : Set U} {input : Fin n → Set U} {admissible : Semifilter ↑targetᶜ → Prop} (c : PairCover target input admissible) (t : ℕ) : PairCover target input admissible

Padding by empty pairs preserves a cover.

theorem Cslib.Circuits.Fusion.PairCover.length_pad {U : Type u} {n : ℕ} {target : Set U} {input : Fin n → Set U} {admissible : Semifilter ↑targetᶜ → Prop} (c : PairCover target input admissible) {t : ℕ} (h : c.pairs.length ≤ t) : (c.pad t).pairs.length = t

Padding reaches any requested larger length exactly.

def Cslib.Circuits.Fusion.PairCover.ofCircuit {U : Type u} {n m : ℕ} {target : Set U} (c : Circuit 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) : PairCover target input admissible

Extract the AND pairs from a native circuit producing the target at a chosen output.

theorem Cslib.Circuits.Fusion.length_andPairs {U : Type u} {V : Type v} (atoms : List (Atom Monotone.signature (Set U))) (f : V → U) : (List.filterMap (fun (a : Atom Monotone.signature (Set U)) => a.andPair? f) atoms).length = (List.map (fun (a : Atom Monotone.signature (Set U)) => Monotone.andCost a.op) atoms).sum

Filtering semantic atoms for AND pairs preserves their total AND weight.

@[simp]

theorem Cslib.Circuits.Fusion.PairCover.length_ofCircuit {U : Type u} {n m : ℕ} {target : Set U} (c : Circuit 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) : (ofCircuit c input o hc admissible).pairs.length = c.program.cost Monotone.andCost

The extracted pair count is exactly the AND-gate count, including unused gates.

noncomputable def Cslib.Circuits.Fusion.pairCoverComplexity {U : Type u} {n : ℕ} (target : Set U) (input : Fin n → Set U) (admissible : Semifilter ↑targetᶜ → Prop := fun (x : Semifilter ↑targetᶜ) => True) : ℕ∞

The minimum pair-cover length, or infinity if no finite cover exists.

theorem Cslib.Circuits.Fusion.pairCoverComplexity_le {U : Type u} {n : ℕ} {target : Set U} {input : Fin n → Set U} {admissible : Semifilter ↑targetᶜ → Prop} (c : PairCover target input admissible) : pairCoverComplexity target input admissible ≤ ↑c.pairs.length

Every cover gives an upper bound on minimum pair-cover complexity.

theorem Cslib.Circuits.Fusion.le_pairCoverComplexity_iff {U : Type u} {n : ℕ} {target : Set U} {input : Fin n → Set U} {admissible : Semifilter ↑targetᶜ → Prop} {k : ℕ∞} : k ≤ pairCoverComplexity target input admissible ↔ ∀ (c : PairCover target input admissible), k ≤ ↑c.pairs.length

A lower bound on cover complexity is exactly a bound for every finite pair cover.

theorem Cslib.Circuits.Fusion.pairCoverComplexity_le_iff {U : Type u} {n : ℕ} {target : Set U} {input : Fin n → Set U} {admissible : Semifilter ↑targetᶜ → Prop} {t : ℕ} : pairCoverComplexity target input admissible ≤ ↑t ↔ ∃ (c : PairCover target input admissible), c.pairs.length ≤ t

Every finite bound on the cover infimum is attained by a cover within that bound.

theorem Cslib.Circuits.Fusion.pairCover_lowerBound {U : Type u} {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 : Circuit Monotone.signature n m) (o : Fin m) (hc : c.eval (Monotone.setInterpretation U) input o = target) : k ≤ c.program.cost Monotone.andCost

Any lower bound on pair-cover length transfers to the AND count of a constructing circuit.

theorem Cslib.Circuits.Fusion.pairCoverComplexity_le_cost {U : Type u} {n m : ℕ} {target : Set U} (c : Circuit 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.program.cost Monotone.andCost)

Pair-cover complexity lower-bounds the AND count of every constructing circuit.

theorem Cslib.Circuits.Fusion.pairCoverComplexity_le_ecomplexityFrom {U : Type u} {n m : ℕ} {X : Type v} (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 ≤ ecomplexityFrom (Monotone.setInterpretation U) Monotone.andCost target sources

A pair-cover bound at an actual source assignment bounds native supplied-source complexity.

def Cslib.Circuits.Fusion.PairCover.ofSourceRefinement {U : Type u_1} {n m : ℕ} {target : Set U} {input : Fin n → Set U} {input' : Fin m → Set U} {admissible : Semifilter ↑targetᶜ → Prop} (c : PairCover target input admissible) (h : ∀ x ∈ target, ∀ (i : Fin n), x ∈ input i → ∃ (j : Fin m), x ∈ input' j ∧ input' j ⊆ input i) : PairCover target input' admissible

A cover remains a cover when every accepted source of the old problem contains an accepted source of the new problem. The pair list and admissibility predicate are unchanged.

theorem Cslib.Circuits.Fusion.pairCoverComplexity_le_of_sourceRefinement {U : Type u_1} {n m : ℕ} {target : Set U} {input : Fin n → Set U} {input' : Fin m → Set U} (admissible : Semifilter ↑targetᶜ → Prop) (h : ∀ x ∈ target, ∀ (i : Fin n), x ∈ input i → ∃ (j : Fin m), x ∈ input' j ∧ input' j ⊆ input i) : pairCoverComplexity target input' admissible ≤ pairCoverComplexity target input admissible

Pointwise source refinement gives a lower bound on pair-cover complexity.