Documentation

Complexity.Computability.Circuit.Fusion.Cyclic.Closure

Closure generated by semifilter pairs #

At a reference point, force the full target complement and the restricted inputs containing that point, close upward, and apply the intersection rule of each listed pair. These are exactly the facts forced in every semifilter above the point that preserves the pairs. If the empty set is not derivable, the derivable sets themselves form such a semifilter.

For a cover of all semifilters, the empty set is derivable exactly at the target points. The generated closure, viewed as a monotone map from complement subsets to ambient subsets, therefore recovers the target at the empty set. This is the semantic closure argument for the converse to the cyclic lower bound; no finite circuit compiler or execution bound is supplied here. The carrier may be infinite, inputs need not cover it, and the pair list may be empty. Restriction to an arbitrary admissible class of semifilters does not supply the converse.

Main definitions #

Main results #

References #

source
inductive Cslib.Circuits.Fusion.PairDerivation {U : Type u} {n : ℕ} (target : Set U) (input : Fin n → Set U) (pairs : List (Set ↑targetᶜ × Set ↑targetᶜ)) (point : U) :
Set ↑targetᶜ → Prop

Sets forced by the inputs true at a point, upward closure, and the listed intersection rules.

Instances For
    source
    theorem Cslib.Circuits.Fusion.PairDerivation.le {U : Type u} {n : ℕ} {target : Set U} {input : Fin n → Set U} {pairs : List (Set ↑targetᶜ × Set ↑targetᶜ)} {point : U} {P : Set ↑targetᶜ → Prop} (huniv : P Set.univ) (hinput : ∀ (i : Fin n), point ∈ input i → P (Subtype.val ⁻¹' input i)) (hmono : Monotone P) (hpairs : ∀ p ∈ pairs, P p.1 → P p.2 → P (p.1 ∩ p.2)) :
    PairDerivation target input pairs point ≤ P

    The derivable sets form the least predicate closed under the four rules.

    source
    def Cslib.Circuits.Fusion.PairDerivation.semifilter {U : Type u} {n : ℕ} {target : Set U} {input : Fin n → Set U} {pairs : List (Set ↑targetᶜ × Set ↑targetᶜ)} {point : U} (h : ¬PairDerivation target input pairs point ∅) :
    Semifilter ↑targetᶜ

    A closure that avoids the empty set is a semifilter preserving every listed pair.

    Instances For
      source
      @[simp]
      theorem Cslib.Circuits.Fusion.PairDerivation.apply_semifilter {U : Type u} {n : ℕ} {target : Set U} {input : Fin n → Set U} {pairs : List (Set ↑targetᶜ × Set ↑targetᶜ)} {point : U} (h : ¬PairDerivation target input pairs point ∅) (s : Set ↑targetᶜ) :
      (semifilter h) s ↔ PairDerivation target input pairs point s

      The canonical semifilter accepts precisely the derivable sets.

      source
      theorem Cslib.Circuits.Fusion.PairDerivation.mem_of_outside {U : Type u} {n : ℕ} {target : Set U} {input : Fin n → Set U} {pairs : List (Set ↑targetᶜ × Set ↑targetᶜ)} {s : Set ↑targetᶜ} (x : ↑targetᶜ) (h : PairDerivation target input pairs (↑x) s) :
      x ∈ s

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

      source
      theorem Cslib.Circuits.Fusion.PairCover.derives_empty {U : Type u} {n : ℕ} {target : Set U} {input : Fin n → Set U} {point : U} (c : PairCover target input) (hpoint : point ∈ target) :
      PairDerivation target input (c.pairs fun (x : Semifilter ↑targetᶜ) => True) point ∅

      An unrestricted cover forces the empty set at each target point.

      source
      theorem Cslib.Circuits.Fusion.PairCover.derives_empty_iff {U : Type u} {n : ℕ} {target : Set U} {input : Fin n → Set U} (c : PairCover target input) (point : U) :
      PairDerivation target input (c.pairs fun (x : Semifilter ↑targetᶜ) => True) point ∅ ↔ point ∈ target

      Deriving the empty set characterizes the target for covers of all semifilters.

      source
      def Cslib.Circuits.Fusion.PairCover.ofDerivesEmpty {U : Type u} {n : ℕ} {target : Set U} {input : Fin n → Set U} (pairs : List (Set ↑targetᶜ × Set ↑targetᶜ)) (h : ∀ point ∈ target, PairDerivation target input pairs point ∅) :
      PairCover target input

      Target-point derivations suffice to defeat every semifilter witness.

      Instances For
        source
        @[simp]
        theorem Cslib.Circuits.Fusion.PairCover.pairs_ofDerivesEmpty {U : Type u} {n : ℕ} {target : Set U} {input : Fin n → Set U} (pairs : List (Set ↑targetᶜ × Set ↑targetᶜ)) (h : ∀ point ∈ target, PairDerivation target input pairs point ∅) :
        ((ofDerivesEmpty pairs h).pairs fun (x : Semifilter ↑targetᶜ) => True) = pairs

        Constructing a cover from derivations leaves the pair list unchanged.

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

        The points deriving each complement subset, ordered monotonically by that subset.

        Instances For
          source
          theorem Cslib.Circuits.Fusion.pairClosure_le {U : Type u} {n : ℕ} {target : Set U} {input : Fin n → Set U} {pairs : List (Set ↑targetᶜ × Set ↑targetᶜ)} (state : Set ↑targetᶜ →o Set U) (huniv : Set.univ ⊆ state Set.univ) (hinput : ∀ (i : Fin n), input i ⊆ state (Subtype.val ⁻¹' input i)) (hpairs : ∀ p ∈ pairs, state p.1 ∩ state p.2 ⊆ state (p.1 ∩ p.2)) :
          pairClosure target input pairs ≤ state

          The generated state lies below every monotone state containing the seeds and pair rules.

          source
          @[simp]
          theorem Cslib.Circuits.Fusion.PairCover.pairClosure_empty {U : Type u} {n : ℕ} {target : Set U} {input : Fin n → Set U} (c : PairCover target input) :
          (pairClosure target input (c.pairs fun (x : Semifilter ↑targetᶜ) => True)) ∅ = target

          The empty-index state of an unrestricted cover is exactly its target.