Pulling fusion covers back along a counterexample section

A semi-filter argument often studies a circuit over one ambient space while the combinatorial cover lives over the complement of a different target. A SemifilterPullback records the bridge:

• a section from source counterexamples into the circuit's ambient space;
• a reference point in the circuit space for each source witness;
• soundness of every circuit generator under pullback; and
• separation of the target from the image of the section.

Every target circuit then gives a pair cover of the source problem. The pair associated with an AND gate is obtained by pulling its two argument sets back along the section, and the cover cost is exactly the circuit's AND cost.

structure Algebraic.Fusion.SemifilterPullback {Γ : Type u_1} {Δ : Type u_2} (source : SetProblem Γ) (target : SetProblem Δ) (admissible : SemifilterClass source) : Type (max u_1 u_2)

Data transporting semi-filter witnesses from source to a set construction problem target.

• counterexampleMap : Problem.Outside source → Δ

  Embed each source counterexample into the target ambient space.

• referencePoint : SemifilterWitness source admissible → Δ

  Reference point used for a particular source witness.

• input_sound (witness : SemifilterWitness source admissible) (input : Fin target.inputCount) : self.referencePoint witness ∈ target.inputs input → self.counterexampleMap ⁻¹' target.inputs input ∈ witness.filter

  Reference-true target generators pull back to accepted source sets.

• target_reference (witness : SemifilterWitness source admissible) : self.referencePoint witness ∈ target.target

  Every reference point belongs to the target.

• section_avoids_target (counterexample : Problem.Outside source) : self.counterexampleMap counterexample ∉ target.target

  The counterexample section avoids the target.

def Algebraic.Fusion.SemifilterPullback.model {Γ : Type u_1} {Δ : Type u_2} {source : SetProblem Γ} {target : SetProblem Δ} {admissible : SemifilterClass source} (pullback : SemifilterPullback source target admissible) : Model AndOr.andCost (AndOr.setInterpretation Δ) target

Observation model induced by a semi-filter pullback.

Equations

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

def Algebraic.Fusion.Atom.pullbackPair? {Γ : Type u_1} {Δ : Type u_2} {source : SetProblem Γ} {target : SetProblem Δ} {admissible : SemifilterClass source} (pullback : SemifilterPullback source target admissible) (atom : Atom AndOr.signature (Set Δ)) : Option (Pair source)

The pulled-back pair contributed by an AND atom.

Equations

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

@[simp]

theorem Algebraic.Fusion.Atom.pullbackPair?_and {Γ : Type u_1} {Δ : Type u_2} {source : SetProblem Γ} {target : SetProblem Δ} {admissible : SemifilterClass source} (pullback : SemifilterPullback source target admissible) (arguments : Fin (AndOr.signature.Arity AndOr.Op.and) → Set Δ) : pullbackPair? pullback { op := AndOr.Op.and, arguments := arguments } = some (pullback.counterexampleMap ⁻¹' arguments ⟨0, pullbackPair?._proof_3⟩, pullback.counterexampleMap ⁻¹' arguments ⟨1, pullbackPair?._proof_4⟩)

@[simp]

theorem Algebraic.Fusion.Atom.pullbackPair?_or {Γ : Type u_1} {Δ : Type u_2} {source : SetProblem Γ} {target : SetProblem Δ} {admissible : SemifilterClass source} (pullback : SemifilterPullback source target admissible) (arguments : Fin (AndOr.signature.Arity AndOr.Op.or) → Set Δ) : pullbackPair? pullback { op := AndOr.Op.or, arguments := arguments } = none

def Algebraic.Fusion.SemifilterPullback.pairs {Γ : Type u_1} {Δ : Type u_2} {source : SetProblem Γ} {target : SetProblem Δ} {admissible : SemifilterClass source} (pullback : SemifilterPullback source target admissible) (atoms : List (Atom AndOr.signature (Set Δ))) : List (Pair source)

Pull back all intersection pairs from a list of target atoms.

Equations

• pullback.pairs atoms = List.filterMap (Algebraic.Fusion.Atom.pullbackPair? pullback) atoms

@[simp]

theorem Algebraic.Fusion.SemifilterPullback.pairs_cons_and {Γ : Type u_1} {Δ : Type u_2} {source : SetProblem Γ} {target : SetProblem Δ} {admissible : SemifilterClass source} (pullback : SemifilterPullback source target admissible) (arguments : Fin (AndOr.signature.Arity AndOr.Op.and) → Set Δ) (atoms : List (Atom AndOr.signature (Set Δ))) : pullback.pairs ({ op := AndOr.Op.and, arguments := arguments } :: atoms) = (pullback.counterexampleMap ⁻¹' arguments ⟨0, Atom.pullbackPair?._proof_3⟩, pullback.counterexampleMap ⁻¹' arguments ⟨1, Atom.pullbackPair?._proof_4⟩) :: pullback.pairs atoms

@[simp]

theorem Algebraic.Fusion.SemifilterPullback.pairs_cons_or {Γ : Type u_1} {Δ : Type u_2} {source : SetProblem Γ} {target : SetProblem Δ} {admissible : SemifilterClass source} (pullback : SemifilterPullback source target admissible) (arguments : Fin (AndOr.signature.Arity AndOr.Op.or) → Set Δ) (atoms : List (Atom AndOr.signature (Set Δ))) : pullback.pairs ({ op := AndOr.Op.or, arguments := arguments } :: atoms) = pullback.pairs atoms

theorem Algebraic.Fusion.SemifilterPullback.pairs_length {Γ : Type u_1} {Δ : Type u_2} {source : SetProblem Γ} {target : SetProblem Δ} {admissible : SemifilterClass source} (pullback : SemifilterPullback source target admissible) (atoms : List (Atom AndOr.signature (Set Δ))) : (pullback.pairs atoms).length = Atom.listCost atoms AndOr.andCost

Pulled-back pair count is the AND weight of the atoms.

theorem Algebraic.Fusion.Atom.preservedBy_pullbackModel {Γ : Type u_1} {Δ : Type u_2} {source : SetProblem Γ} {target : SetProblem Δ} {admissible : SemifilterClass source} (pullback : SemifilterPullback source target admissible) (atom : Atom AndOr.signature (Set Δ)) (witness : SemifilterWitness source admissible) (pairPreserved : ∀ (pair : Pair source), pullbackPair? pullback atom = some pair → witness.filter.PreservesPair pair) : atom.PreservedBy pullback.model witness

Preserving an atom's pulled-back pair is enough to preserve the atom in the pullback observation model.

def Algebraic.Fusion.SemifilterPullback.pairCoverOfCircuit {Γ : Type u_1} {Δ : Type u_2} {source : SetProblem Γ} {target : SetProblem Δ} {admissible : SemifilterClass source} (pullback : SemifilterPullback source target admissible) (circuit : Circuit AndOr.signature target.inputCount 1) (constructs : Problem.Constructs target circuit (AndOr.setInterpretation Δ)) : PairCover source admissible

A constructing target circuit yields a pair cover of the source problem.

Equations

• pullback.pairCoverOfCircuit circuit constructs = { pairs := pullback.pairs (Algebraic.Fusion.circuitAtoms circuit (Algebraic.AndOr.setInterpretation Δ) target.inputs), isCover := ⋯ }

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

Pullback preserves the exact AND cost of a constructing circuit.

theorem Algebraic.Fusion.SemifilterPullback.lowerBound {Γ : Type u_1} {Δ : Type u_2} {source : SetProblem Γ} {target : SetProblem Δ} {admissible : SemifilterClass source} {L : ℕ} (pullback : SemifilterPullback source target admissible) (coverLowerBound : ∀ (cover : PairCover source admissible), L ≤ cover.cost) (circuit : Circuit AndOr.signature target.inputCount 1) (constructs : Problem.Constructs target circuit (AndOr.setInterpretation Δ)) : L ≤ circuit.cost AndOr.andCost

A lower bound for source pair covers transfers across a pullback to every constructing target circuit.