Fusion atoms under circuit substitution

Atom extraction is compatible with causal program instantiation: the ambient atoms occur first, followed by the source atoms evaluated under the values of the supplied ambient wires. This is the semantic gate-list analogue of Program.instantiate_trace and is the reusable bridge for proving local Fusion restrictions after circuit compilation.

theorem Algebraic.Fusion.programAtoms_instantiate {σ : Signature} {n g n' h : ℕ} {U : Type u_2} (source : Program σ n g) (ambient : Program σ n' h) (inputWires : Fin n → Wire n' h) (interpretation : Interpretation σ U) (input : Fin n' → U) : programAtoms interpretation input (source.instantiate ambient inputWires) = programAtoms interpretation input ambient ++ programAtoms interpretation (ambient.trace interpretation input ∘ inputWires) source

Instantiating a source program appends exactly its semantic atoms after the ambient atoms, with source inputs interpreted by the supplied wires.

theorem Algebraic.Fusion.programAtoms_append {σ : Signature} {n' h n g : ℕ} {U : Type u_2} (ambient : Program σ n' h) (feed : Fin n → Wire n' h) (continuation : Program σ n g) (interpretation : Interpretation σ U) (input : Fin n' → U) : programAtoms interpretation input (ambient.append feed continuation) = programAtoms interpretation input ambient ++ programAtoms interpretation (ambient.trace interpretation input ∘ feed) continuation

Continuing a program by another appends exactly the continuation's semantic atoms, with its inputs interpreted by the feeding wires.

theorem Algebraic.Fusion.circuitAtoms_comp {σ : Signature} {m k n : ℕ} {U : Type u_2} (outer : Circuit σ m k) (inner : Circuit σ n m) (interpretation : Interpretation σ U) (input : Fin n → U) : circuitAtoms (outer.comp inner) interpretation input = circuitAtoms inner interpretation input ++ circuitAtoms outer interpretation (inner.eval interpretation input)

Sequential composition concatenates the inner atoms with the outer atoms evaluated on the inner circuit's outputs.