Fusion atoms under circuit composition

Continuing a native program concatenates its semantic atoms with those of the continuation, evaluated on the values supplied by the feeding wires. The identity keeps gate order and multiplicity, including unused gates. No separate substitution operation is needed.

Main results

• Cslib.Circuits.Fusion.programAtoms_append: exact atom extraction under program continuation.
• Cslib.Circuits.Fusion.programAtoms_comp: exact atom extraction under circuit composition.

References

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

theorem Cslib.Circuits.Fusion.programAtoms_append {σ : Signature} {U : Type v} {n m g h : ℕ} (p : Program σ n g) (feed : Fin m → Wire n g) (q : Program σ m h) (I : Interpretation σ U) (input : Fin n → U) : programAtoms (p.append feed q) I input = Fin.append (programAtoms p I input) (programAtoms q I (p.trace I input ∘ feed))

Continuing a program appends the continuation's atoms, evaluated at its supplied inputs.

theorem Cslib.Circuits.Fusion.programAtoms_comp {σ : Signature} {U : Type v} {n m k : ℕ} (outer : Circuit σ m k) (inner : Circuit σ n m) (I : Interpretation σ U) (input : Fin n → U) : programAtoms (outer.comp inner).program I input = Fin.append (programAtoms inner.program I input) (programAtoms outer.program I (inner.eval I input))

Composition lists the inner circuit's atoms first, then the outer circuit's atoms evaluated on the inner outputs.