Local Fusion properties under circuit simulation #
A property holds at every compiled atom exactly when it holds at every atom of each operation gadget, evaluated at the source gate's actual arguments. This includes unused source gates and all gates of each gadget, whether or not its output uses them. Zero-gate implementations add no atoms. The simulation is CSLib's native gate replacement.
Main results #
Cslib.Circuits.Fusion.forall_programAtoms_simulate_iff: reduce a property of all compiled atoms to the actual operation gadgets.Cslib.Circuits.Fusion.forall_programAtoms_simulate: circuit-level local property transfer.
References #
- Generalizes the transport argument in LowerBound/Fusion/Contextual.lean in S. Schlesinger, Algebraic circuit formalizations in Complexitylib.
theorem Cslib.Circuits.Fusion.forall_programAtoms_simulate_iff {σ : Signature} {τ : Signature} {U : Type w} {n g : ℕ} (p : Program σ n g) (impl : (op : σ.Op) → Circuit τ (σ.Arity op) 1) {I : Interpretation σ U} {J : Interpretation τ U} (himpl : ∀ (op : σ.Op), (impl op).Computes J (single (I op))) (input : Fin n → U) (P : Atom τ U → Prop) :
(∀ (j : Fin (p.cost fun (op : σ.Op) => (impl op).size)), P (programAtoms (p.simulateProgram impl) J input j)) ↔ ∀ (k : Fin g),
have a := programAtoms p I input k;
∀ (j : Fin (impl a.op).size), P (programAtoms (impl a.op).program J a.arguments j)
Every compiled atom has a property exactly when all actual gadget atoms do. The gadget assumptions are needed only at the arguments of source gates.
theorem Cslib.Circuits.Fusion.forall_programAtoms_simulate {σ : Signature} {τ : Signature} {U : Type w} {n m : ℕ} (c : Circuit σ n m) (impl : (op : σ.Op) → Circuit τ (σ.Arity op) 1) {I : Interpretation σ U} {J : Interpretation τ U} (himpl : ∀ (op : σ.Op), (impl op).Computes J (single (I op))) (input : Fin n → U) (P : Atom τ U → Prop) (hlocal :
∀ (k : Fin c.size),
have a := programAtoms c.program I input k;
∀ (j : Fin (impl a.op).size), P (programAtoms (impl a.op).program J a.arguments j)) (j : Fin (c.simulate impl).size) :
P (programAtoms (c.simulate impl).program J input j)
Local gadget properties transfer to every atom of the simulated circuit.