Local Fusion properties under contextual compilation

If every atom in every contextual operation gadget satisfies a semantic property, then every atom in the compiled target circuit satisfies it. The proof combines atom extraction under instantiation with contextual trace preservation, so gadget inputs are rewritten to the shared context followed by the actual source-operation arguments.

theorem Algebraic.Fusion.ContextualTranslation.forall_atoms_compileProgram {σ : Signature} {τ : Signature} {q n g : ℕ} {U : Type u_3} (translation : ContextualTranslation σ τ q) (source : Program σ n g) (interpretation : Interpretation τ U) (context : Fin q → U) (input : Fin n → U) (property : Atom τ U → Prop) (gadget : ∀ (operation : σ.Op) (arguments : Fin (σ.Arity operation) → U), ∀ atom ∈ circuitAtoms (translation.operation operation) interpretation (ContextualTranslation.appendInputs context arguments), property atom) (atom : Atom τ U) (present : atom ∈ programAtoms interpretation (ContextualTranslation.appendInputs context input) (translation.compileProgram source).program) : property atom

A local target-atom property verified for every contextual gadget is preserved by compilation of an entire source program.

theorem Algebraic.Fusion.ContextualTranslation.forall_atoms_compile {σ : Signature} {τ : Signature} {q n m : ℕ} {U : Type u_3} (translation : ContextualTranslation σ τ q) (circuit : Circuit σ n m) (interpretation : Interpretation τ U) (context : Fin q → U) (input : Fin n → U) (property : Atom τ U → Prop) (gadget : ∀ (operation : σ.Op) (arguments : Fin (σ.Arity operation) → U), ∀ atom ∈ circuitAtoms (translation.operation operation) interpretation (ContextualTranslation.appendInputs context arguments), property atom) (atom : Atom τ U) (present : atom ∈ circuitAtoms (translation.compile circuit) interpretation (ContextualTranslation.appendInputs context input)) : property atom

Circuit-level form of forall_atoms_compileProgram.