Generated semi-filter closure

Given a point and a list of fusion pairs, start with the full complement and the restricted generators true at the point, then close upward and apply every pair rule (left, right) ↦ left ∩ right. This is the least semi-filter-like family forced by the generators and the pair rules.

The empty set is derivable at exactly the target points when the pair list is a cover of all semi-filters. Outside the target, the corresponding complement point belongs to every derivable set. This closure characterization is the combinatorial kernel of the cover-to-cyclic direction of fusion completeness.

inductive Algebraic.Fusion.PairDerivation {Γ : Type u_1} (problem : SetProblem Γ) (pairs : List (Pair problem)) (point : Γ) : Set (Problem.Outside problem) → Prop

Sets forced into the semi-filter generated above point by a list of fusion pairs.

• univ {Γ : Type u_1} {problem : SetProblem Γ} {pairs : List (Pair problem)} {point : Γ} : PairDerivation problem pairs point Set.univ

  Every semi-filter contains the full set.

• generator {Γ : Type u_1} {problem : SetProblem Γ} {pairs : List (Pair problem)} {point : Γ} (input : Fin problem.inputCount) (present : point ∈ problem.inputs input) : PairDerivation problem pairs point (Problem.restrict problem (problem.inputs input))

  Restricted generators true at the reference point are forced.

• upward {Γ : Type u_1} {problem : SetProblem Γ} {pairs : List (Pair problem)} {point : Γ} {lower upper : Set (Problem.Outside problem)} (derived : PairDerivation problem pairs point lower) (subset : lower ⊆ upper) : PairDerivation problem pairs point upper

  Forced membership is upward closed.

• fusion {Γ : Type u_1} {problem : SetProblem Γ} {pairs : List (Pair problem)} {point : Γ} (pair : Pair problem) (present : pair ∈ pairs) (leftDerived : PairDerivation problem pairs point pair.1) (rightDerived : PairDerivation problem pairs point pair.2) : PairDerivation problem pairs point (pair.1 ∩ pair.2)

  Every listed fusion pair contributes its intersection rule.

def Algebraic.Fusion.PairDerivation.semifilter {Γ : Type u_1} {problem : SetProblem Γ} {pairs : List (Pair problem)} {point : Γ} (empty_not_derived : ¬PairDerivation problem pairs point ∅) : Semifilter (Problem.Outside problem)

If the generated closure avoids the empty set, it is a genuine semi-filter.

Equations

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

@[simp]

theorem Algebraic.Fusion.PairDerivation.mem_semifilter {Γ : Type u_1} {problem : SetProblem Γ} {pairs : List (Pair problem)} {point : Γ} (empty_not_derived : ¬PairDerivation problem pairs point ∅) (set : Set (Problem.Outside problem)) : set ∈ semifilter empty_not_derived ↔ PairDerivation problem pairs point set

theorem Algebraic.Fusion.PairDerivation.semifilter_above {Γ : Type u_1} {problem : SetProblem Γ} {pairs : List (Pair problem)} {point : Γ} (empty_not_derived : ¬PairDerivation problem pairs point ∅) : (semifilter empty_not_derived).Above point

The generated semi-filter is above its reference point.

theorem Algebraic.Fusion.PairDerivation.semifilter_preservesPair {Γ : Type u_1} {problem : SetProblem Γ} {pairs : List (Pair problem)} {point : Γ} (empty_not_derived : ¬PairDerivation problem pairs point ∅) (pair : Pair problem) (present : pair ∈ pairs) : (semifilter empty_not_derived).PreservesPair pair

The generated semi-filter preserves every pair used to generate it.

theorem Algebraic.Fusion.PairCover.derives_empty {Γ : Type u_1} {problem : SetProblem Γ} (cover : PairCover problem) (point : Γ) (pointMem : point ∈ problem.target) : PairDerivation problem (cover.pairs SemifilterClass.all) point ∅

A cover forces the empty set into the generated closure at every target point.

theorem Algebraic.Fusion.PairDerivation.counterexample_mem {Γ : Type u_1} {problem : SetProblem Γ} {pairs : List (Pair problem)} (counterexample : Problem.Outside problem) {set : Set (Problem.Outside problem)} (derived : PairDerivation problem pairs (↑counterexample) set) : counterexample ∈ set

An outside point belongs to every set derivable above its ambient value.

theorem Algebraic.Fusion.PairDerivation.empty_not_of_outside {Γ : Type u_1} {problem : SetProblem Γ} {pairs : List (Pair problem)} (counterexample : Problem.Outside problem) : ¬PairDerivation problem pairs ↑counterexample ∅

The empty set can never be derived at a point outside the target.

theorem Algebraic.Fusion.PairCover.derives_empty_iff {Γ : Type u_1} {problem : SetProblem Γ} (cover : PairCover problem) (point : Γ) : PairDerivation problem (cover.pairs SemifilterClass.all) point ∅ ↔ point ∈ problem.target

For a pair cover, generated closure derives the empty set exactly on the target.

structure Algebraic.Fusion.PairClosure.IsPrefixed {Γ : Type u_1} (problem : SetProblem Γ) (pairs : List (Pair problem)) (state : Set (Problem.Outside problem) → Set Γ) : Prop

A proposed state for all subset-indexed closure gates is pre-fixed when it contains the full-set seed, the generators, upward propagation, and every fusion rule.

• univ : Set.univ ⊆ state Set.univ

  The full complement is forced at every reference point.

• generator (input : Fin problem.inputCount) : problem.inputs input ⊆ state (Problem.restrict problem (problem.inputs input))

  Each generator feeds its corresponding restricted-set gate.

• upward {lower upper : Set (Problem.Outside problem)} : lower ⊆ upper → state lower ⊆ state upper

  Subset-indexed gates propagate upward.

• fusion (pair : Pair problem) : pair ∈ pairs → state pair.1 ∩ state pair.2 ⊆ state (pair.1 ∩ pair.2)

  Each fusion pair contributes one intersection rule.

def Algebraic.Fusion.PairClosure.generatedState {Γ : Type u_1} (problem : SetProblem Γ) (pairs : List (Pair problem)) : Set (Problem.Outside problem) → Set Γ

State generated by the inductive pair closure.

Equations

• Algebraic.Fusion.PairClosure.generatedState problem pairs set = {point : Γ | Algebraic.Fusion.PairDerivation problem pairs point set}

theorem Algebraic.Fusion.PairClosure.generatedState_prefixed {Γ : Type u_1} (problem : SetProblem Γ) (pairs : List (Pair problem)) : IsPrefixed problem pairs (generatedState problem pairs)

The generated state is closed under all pair-closure rules.

theorem Algebraic.Fusion.PairClosure.generatedState_least {Γ : Type u_1} (problem : SetProblem Γ) (pairs : List (Pair problem)) (state : Set (Problem.Outside problem) → Set Γ) (prefixed : IsPrefixed problem pairs state) (set : Set (Problem.Outside problem)) : generatedState problem pairs set ⊆ state set

Inductive pair closure is the least state closed under the four forcing rules.

theorem Algebraic.Fusion.PairCover.generatedState_empty {Γ : Type u_1} {problem : SetProblem Γ} (cover : PairCover problem) : PairClosure.generatedState problem (cover.pairs SemifilterClass.all) ∅ = problem.target

The empty-index gate of the generated closure state is exactly the target set when the pairs form a cover.