Pulling circuit covers back to counterexamples

A map from counterexamples of one problem into the ambient space of a circuit, together with reference points for each witness, transports its AND pairs to a cover. Each reference point must belong to the circuit's target, every mapped counterexample must avoid that target, and reference-true inputs must be accepted by the pulled-back observation.

Main definitions

• Cslib.Circuits.Fusion.PairCover.ofCircuitPullback: pull a circuit's AND pairs back.

Main results

• Cslib.Circuits.Fusion.PairCover.length_ofCircuitPullback: exact preservation of AND count.

References

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

def Cslib.Circuits.Fusion.PairCover.ofCircuitPullback {U : Type u_1} {V : Type u_2} {n k m : ℕ} {target : Set U} {input : Fin n → Set U} {admissible : Semifilter ↑targetᶜ → Prop} {target' : Set V} (c : Circuit Monotone.signature k m) (input' : Fin k → Set V) (o : Fin m) (hc : c.eval (Monotone.setInterpretation V) input' o = target') (f : ↑targetᶜ → V) (reference : SemifilterWitness target input admissible → ↑target') (hin : ∀ (w : SemifilterWitness target input admissible) (i : Fin k), ↑(reference w) ∈ input' i → w.filter (f ⁻¹' input' i)) (hout : ∀ (x : ↑targetᶜ), f x ∉ target') : PairCover target input admissible

A circuit whose accepting references and rejecting counterexamples transport the input observations yields a pair cover of the original problem. No injectivity of the map is needed.

@[simp]

theorem Cslib.Circuits.Fusion.PairCover.length_ofCircuitPullback {U : Type u_1} {V : Type u_2} {n k m : ℕ} {target : Set U} {input : Fin n → Set U} {admissible : Semifilter ↑targetᶜ → Prop} {target' : Set V} (c : Circuit Monotone.signature k m) (input' : Fin k → Set V) (o : Fin m) (hc : c.eval (Monotone.setInterpretation V) input' o = target') (f : ↑targetᶜ → V) (reference : SemifilterWitness target input admissible → ↑target') (hin : ∀ (w : SemifilterWitness target input admissible) (i : Fin k), ↑(reference w) ∈ input' i → w.filter (f ⁻¹' input' i)) (hout : ∀ (x : ↑targetᶜ), f x ∉ target') : (ofCircuitPullback c input' o hc f reference hin hout).pairs.length = c.program.cost Monotone.andCost

Pullback retains one pair for every AND gate, including repeated or unused gates.