Set-theoretic fusion with semi-filters

This file instantiates the algebra-generic fusion engine with the classical set-theoretic framework. A construction problem consists of generator subsets of an ambient type and a target subset. Witnesses are target points equipped with semi-filters over the complement of the target.

The public combinatorial objects are lists of pairs of subsets. Such a list is a cover when no admissible semi-filter above a target point preserves every pair. Every AND/OR circuit constructing the target yields a cover whose length is exactly its number of AND gates.

structure Algebraic.Fusion.Semifilter (U : Type u) : Type u

A nontrivial upward-closed family of subsets.

• carrier : Set (Set U)

  Subsets accepted by the semi-filter.

• nonempty : self.carrier.Nonempty

  At least one subset is accepted.

• upward {lower upper : Set U} : lower ∈ self.carrier → lower ⊆ upper → upper ∈ self.carrier

  Acceptance is upward closed.

• empty_not_mem : ∅ ∉ self.carrier

  The empty set is not accepted.

@[instance_reducible]

instance Algebraic.Fusion.instSetLikeSemifilterSet {U : Type u_1} : SetLike (Semifilter U) (Set U)

Equations

• Algebraic.Fusion.instSetLikeSemifilterSet = { coe := Algebraic.Fusion.Semifilter.carrier, coe_injective := ⋯ }

theorem Algebraic.Fusion.Semifilter.ext {U : Type u_1} {left right : Semifilter U} (equal : ∀ (set : Set U), set ∈ left ↔ set ∈ right) : left = right

theorem Algebraic.Fusion.Semifilter.ext_iff {U : Type u_1} {left right : Semifilter U} : left = right ↔ ∀ (set : Set U), set ∈ left ↔ set ∈ right

theorem Algebraic.Fusion.Semifilter.univ_mem {U : Type u_1} (filter : Semifilter U) : Set.univ ∈ filter

Every semi-filter contains the full set.

theorem Algebraic.Fusion.Semifilter.union_right {U : Type u_1} (filter : Semifilter U) {left : Set U} (right : Set U) (present : left ∈ filter) : left ∪ right ∈ filter

Acceptance of a set implies acceptance after union on the right.

theorem Algebraic.Fusion.Semifilter.union_left {U : Type u_1} (filter : Semifilter U) (left : Set U) {right : Set U} (present : right ∈ filter) : left ∪ right ∈ filter

Acceptance of a set implies acceptance after union on the left.

@[reducible, inline]

abbrev Algebraic.Fusion.SetProblem (Γ : Type u) : Type u

A set-valued fusion problem is a discrete construction problem.

Equations

• Algebraic.Fusion.SetProblem Γ = Algebraic.Fusion.Problem (Set Γ)

@[reducible, inline]

abbrev Algebraic.Fusion.Problem.Outside {Γ : Type u_1} (problem : SetProblem Γ) : Type u_1

The complement of a set problem's target, as an ambient subtype.

Equations

• Algebraic.Fusion.Problem.Outside problem = { point : Γ // point ∉ problem.target }

def Algebraic.Fusion.Problem.restrict {Γ : Type u_1} (problem : SetProblem Γ) (set : Set Γ) : Set (Outside problem)

Restrict a subset of the ambient type to the target complement.

Equations

• Algebraic.Fusion.Problem.restrict problem set = Subtype.val ⁻¹' set

@[simp]

theorem Algebraic.Fusion.Problem.mem_restrict {Γ : Type u_1} (problem : SetProblem Γ) (set : Set Γ) (point : Outside problem) : point ∈ restrict problem set ↔ ↑point ∈ set

@[simp]

theorem Algebraic.Fusion.Problem.restrict_empty {Γ : Type u_1} (problem : SetProblem Γ) : restrict problem ∅ = ∅

@[simp]

theorem Algebraic.Fusion.Problem.restrict_union {Γ : Type u_1} (problem : SetProblem Γ) (left right : Set Γ) : restrict problem (left ∪ right) = restrict problem left ∪ restrict problem right

@[simp]

theorem Algebraic.Fusion.Problem.restrict_inter {Γ : Type u_1} (problem : SetProblem Γ) (left right : Set Γ) : restrict problem (left ∩ right) = restrict problem left ∩ restrict problem right

@[simp]

theorem Algebraic.Fusion.Problem.restrict_target {Γ : Type u_1} (problem : SetProblem Γ) : restrict problem problem.target = ∅

def Algebraic.Fusion.Semifilter.Above {Γ : Type u_1} {problem : SetProblem Γ} (filter : Semifilter (Problem.Outside problem)) (point : Γ) : Prop

A semi-filter is above a point when it accepts every generator containing it.

Equations

• filter.Above point = ∀ (input : Fin problem.inputCount), point ∈ problem.inputs input → Algebraic.Fusion.Problem.restrict problem (problem.inputs input) ∈ filter

@[reducible, inline]

abbrev Algebraic.Fusion.SemifilterClass {Γ : Type u_1} (problem : SetProblem Γ) : Type u_1

A selectable class of semi-filters for variants of cover complexity.

Equations

• Algebraic.Fusion.SemifilterClass problem = (Algebraic.Fusion.Semifilter (Algebraic.Fusion.Problem.Outside problem) → Prop)

def Algebraic.Fusion.SemifilterClass.all {Γ✝ : Type u_1} {problem : SetProblem Γ✝} : Semifilter (Problem.Outside problem) → Prop

The unrestricted class of all semi-filters.

Equations

• Algebraic.Fusion.SemifilterClass.all x✝ = True

def Algebraic.Fusion.Semifilter.IsUltra {U : Type u_1} (filter : Semifilter U) : Prop

A semi-ultrafilter accepts either a set or its complement. Unlike an ultrafilter, it is not required to be closed under intersections.

Equations

• filter.IsUltra = ∀ (set : Set U), set ∈ filter ∨ setᶜ ∈ filter

def Algebraic.Fusion.SemifilterClass.ultra {Γ✝ : Type u_1} {problem : SetProblem Γ✝} (filter : Semifilter (Problem.Outside problem)) : Prop

The selectable class of all semi-ultrafilters.

Equations

• Algebraic.Fusion.SemifilterClass.ultra filter = filter.IsUltra

structure Algebraic.Fusion.SemifilterWitness {Γ : Type u_1} (problem : SetProblem Γ) (admissible : SemifilterClass problem) : Type u_1

A target point and an admissible semi-filter above that point.

• point : Γ

  Point of the target set being fused.

• point_mem : self.point ∈ problem.target

  The distinguished point belongs to the target.

• filter : Semifilter (Problem.Outside problem)

  Semi-filter over the target complement.

• admissible_filter : admissible self.filter

  This semi-filter belongs to the selected witness class.

• above : self.filter.Above self.point

  This semi-filter lies above the distinguished target point.

def Algebraic.Fusion.semifilterModel {Γ : Type u_1} (problem : SetProblem Γ) (admissible : SemifilterClass problem := SemifilterClass.all) : Model AndOr.andCost (AndOr.setInterpretation Γ) problem

The standard semi-filter observation model for set-theoretic fusion.

Equations

• One or more equations did not get rendered due to their size.

@[reducible, inline]

abbrev Algebraic.Fusion.Pair {Γ : Type u_1} (problem : SetProblem Γ) : Type u_1

A local fusion pair consists of two subsets of the target complement.

Equations

• Algebraic.Fusion.Pair problem = (Set (Algebraic.Fusion.Problem.Outside problem) × Set (Algebraic.Fusion.Problem.Outside problem))

def Algebraic.Fusion.Semifilter.PreservesPair {U : Type u_1} (filter : Semifilter U) (pair : Set U × Set U) : Prop

A semi-filter preserves a pair when it accepts their intersection whenever it accepts both members.

Equations

• filter.PreservesPair pair = (pair.1 ∈ filter → pair.2 ∈ filter → pair.1 ∩ pair.2 ∈ filter)

def Algebraic.Fusion.Problem.IsPairCover {Γ : Type u_1} (problem : SetProblem Γ) (admissible : SemifilterClass problem) (pairs : List (Pair problem)) : Prop

A list of pairs covers every admissible semi-filter above a target point.

Equations

• One or more equations did not get rendered due to their size.

structure Algebraic.Fusion.PairCover {Γ : Type u_1} (problem : SetProblem Γ) (admissible : SemifilterClass problem := SemifilterClass.all) : Type u_1

A proof-carrying set-theoretic fusion cover.

• pairs : List (Pair problem)

  Pairs of subsets in the cover.

• isCover : Problem.IsPairCover problem admissible self.pairs

  No admissible semi-filter above the target preserves every pair.

def Algebraic.Fusion.PairCover.cost {Γ✝ : Type u_1} {problem : SetProblem Γ✝} {admissible : SemifilterClass problem} (cover : PairCover problem admissible) : ℕ

The number of pairs in a set-theoretic fusion cover.

Equations

• cover.cost = cover.pairs.length

noncomputable def Algebraic.Fusion.pairCoverComplexity {Γ : Type u_1} (problem : SetProblem Γ) (admissible : SemifilterClass problem := SemifilterClass.all) : ℕ∞

Classical set-theoretic cover complexity ρ.

Equations

• Algebraic.Fusion.pairCoverComplexity problem admissible = ⨅ (cover : Algebraic.Fusion.PairCover problem admissible), ↑cover.cost

theorem Algebraic.Fusion.pairCoverComplexity_le {Γ : Type u_1} (problem : SetProblem Γ) (admissible : SemifilterClass problem) (cover : PairCover problem admissible) : pairCoverComplexity problem admissible ≤ ↑cover.cost

Every concrete pair cover upper-bounds pair-cover complexity.

def Algebraic.Fusion.Atom.andPair? {Γ : Type u_1} (problem : SetProblem Γ) (atom : Atom AndOr.signature (Set Γ)) : Option (Pair problem)

The pair contributed by an AND atom; OR atoms contribute no pair.

Equations

• One or more equations did not get rendered due to their size.
• Algebraic.Fusion.Atom.andPair? problem { op := Algebraic.AndOr.Op.or, arguments := arguments } = none

@[simp]

theorem Algebraic.Fusion.Atom.andPair?_and {Γ : Type u_1} (problem : SetProblem Γ) (arguments : Fin (AndOr.signature.Arity AndOr.Op.and) → Set Γ) : andPair? problem { op := AndOr.Op.and, arguments := arguments } = some (Problem.restrict problem (arguments ⟨0, andPair?._proof_3⟩), Problem.restrict problem (arguments ⟨1, andPair?._proof_4⟩))

@[simp]

theorem Algebraic.Fusion.Atom.andPair?_or {Γ : Type u_1} (problem : SetProblem Γ) (arguments : Fin (AndOr.signature.Arity AndOr.Op.or) → Set Γ) : andPair? problem { op := AndOr.Op.or, arguments := arguments } = none

def Algebraic.Fusion.intersectionPairs {Γ : Type u_1} (problem : SetProblem Γ) (atoms : List (Atom AndOr.signature (Set Γ))) : List (Pair problem)

Keep the intersection pairs from a list of AND/OR atoms.

Equations

• Algebraic.Fusion.intersectionPairs problem atoms = List.filterMap (Algebraic.Fusion.Atom.andPair? problem) atoms

@[simp]

theorem Algebraic.Fusion.intersectionPairs_cons_and {Γ : Type u_1} (problem : SetProblem Γ) (arguments : Fin (AndOr.signature.Arity AndOr.Op.and) → Set Γ) (atoms : List (Atom AndOr.signature (Set Γ))) : intersectionPairs problem ({ op := AndOr.Op.and, arguments := arguments } :: atoms) = (Problem.restrict problem (arguments ⟨0, Atom.andPair?._proof_3⟩), Problem.restrict problem (arguments ⟨1, Atom.andPair?._proof_4⟩)) :: intersectionPairs problem atoms

@[simp]

theorem Algebraic.Fusion.intersectionPairs_cons_or {Γ : Type u_1} (problem : SetProblem Γ) (arguments : Fin (AndOr.signature.Arity AndOr.Op.or) → Set Γ) (atoms : List (Atom AndOr.signature (Set Γ))) : intersectionPairs problem ({ op := AndOr.Op.or, arguments := arguments } :: atoms) = intersectionPairs problem atoms

theorem Algebraic.Fusion.intersectionPairs_length {Γ : Type u_1} (problem : SetProblem Γ) (atoms : List (Atom AndOr.signature (Set Γ))) : (intersectionPairs problem atoms).length = Atom.listCost atoms AndOr.andCost

The number of extracted pairs is exactly the AND weight of the atoms.

theorem Algebraic.Fusion.Atom.preservedBy_semifilterModel {Γ : Type u_1} (problem : SetProblem Γ) (admissible : SemifilterClass problem) (atom : Atom AndOr.signature (Set Γ)) (witness : SemifilterWitness problem admissible) (pairPreserved : ∀ (pair : Pair problem), andPair? problem atom = some pair → witness.filter.PreservesPair pair) : atom.PreservedBy (semifilterModel problem admissible) witness

Semi-filters automatically preserve union atoms; preservation of the associated pair is sufficient for an intersection atom.

def Algebraic.Fusion.pairCoverOfCircuit {Γ : Type u_1} (problem : SetProblem Γ) (admissible : SemifilterClass problem) (circuit : Circuit AndOr.signature problem.inputCount 1) (constructs : Problem.Constructs problem circuit (AndOr.setInterpretation Γ)) : PairCover problem admissible

Every constructing AND/OR circuit yields its classical semi-filter cover.

Equations

• One or more equations did not get rendered due to their size.

theorem Algebraic.Fusion.pairCoverOfCircuit_cost {Γ : Type u_1} (problem : SetProblem Γ) (admissible : SemifilterClass problem) (circuit : Circuit AndOr.signature problem.inputCount 1) (constructs : Problem.Constructs problem circuit (AndOr.setInterpretation Γ)) : (pairCoverOfCircuit problem admissible circuit constructs).cost = circuit.cost AndOr.andCost

The extracted pair cover has exactly the circuit's number of AND gates.

theorem Algebraic.Fusion.pairCover_lowerBound {Γ : Type u_1} {L : ℕ} (problem : SetProblem Γ) (admissible : SemifilterClass problem) (coverLowerBound : ∀ (cover : PairCover problem admissible), L ≤ cover.cost) (circuit : Circuit AndOr.signature problem.inputCount 1) (constructs : Problem.Constructs problem circuit (AndOr.setInterpretation Γ)) : L ≤ circuit.cost AndOr.andCost

A lower bound for all semi-filter pair covers is an AND-circuit lower bound.

theorem Algebraic.Fusion.pairCoverComplexity_le_cost {Γ : Type u_1} (problem : SetProblem Γ) (admissible : SemifilterClass problem) (circuit : Circuit AndOr.signature problem.inputCount 1) (constructs : Problem.Constructs problem circuit (AndOr.setInterpretation Γ)) : pairCoverComplexity problem admissible ≤ ↑(circuit.cost AndOr.andCost)

Set-theoretic cover complexity lower-bounds every AND/OR construction.