Fusion covers under homomorphisms

A homomorphism of interpretations maps every semantic gate to the corresponding gate in the image. A predicate on image values is preserved there exactly when its pullback is preserved in the source. Thus every cover of the pulled-back predicates maps to a cover of the original predicates, with the same indexed operations and exactly the same operation costs.

No injectivity or surjectivity is required. Minimum cover complexity can decrease: image covers may use arguments outside the range of the homomorphism. Lower bounds on image covers therefore transfer to source covers, and coverComplexity_le_ecomplexityFrom transfers them to circuits. Witnesses and predicates use the existing Fusion API; no separate model wrapper is needed.

Main definitions

• Cslib.Circuits.Fusion.Atom.map: apply a carrier map to an atom's arguments.
• Cslib.Circuits.Fusion.Cover.map: transport a cover through a homomorphism.

Main results

• Cslib.Circuits.Fusion.programAtoms_map: extraction commutes with homomorphisms.
• Cslib.Circuits.Fusion.Cover.cost_map: transport preserves exact operation costs.
• Cslib.Circuits.Fusion.coverComplexity_le_comap: image lower bounds transfer to source covers.

References

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

def Cslib.Circuits.Fusion.Atom.map {σ : Signature} {U : Type v} {V : Type w} (a : Atom σ U) (f : U → V) : Atom σ V

Apply a carrier map to every argument of an atom, retaining its operation.

@[simp]

theorem Cslib.Circuits.Fusion.Atom.op_map {σ : Signature} {U : Type v} {V : Type w} (a : Atom σ U) (f : U → V) : (a.map f).op = a.op

@[simp]

theorem Cslib.Circuits.Fusion.Atom.arguments_map {σ : Signature} {U : Type v} {V : Type w} (a : Atom σ U) (f : U → V) : (a.map f).arguments = f ∘ a.arguments

@[simp]

theorem Cslib.Circuits.Fusion.Atom.map_id {σ : Signature} {U : Type v} (a : Atom σ U) : a.map id = a

@[simp]

theorem Cslib.Circuits.Fusion.Atom.map_map {σ : Signature} {U : Type v} {V : Type w} {T : Type t} (a : Atom σ U) (f : U → V) (g : V → T) : (a.map f).map g = a.map (g ∘ f)

theorem Cslib.Circuits.Fusion.Atom.preserves_map_iff {σ : Signature} {U : Type v} {V : Type w} {I : Interpretation σ U} {J : Interpretation σ V} (a : Atom σ U) (h : Homomorphism I J) (Q : V → Prop) : (a.map h.map).Preserves J Q ↔ a.Preserves I (Q ∘ h.map)

Preservation of an image predicate is equivalent to preservation of its pullback.

theorem Cslib.Circuits.Fusion.programAtoms_map {σ : Signature} {U : Type v} {V : Type w} {I : Interpretation σ U} {J : Interpretation σ V} {n g : ℕ} (p : Program σ n g) (h : Homomorphism I J) (input : Fin n → U) (k : Fin g) : (programAtoms p I input k).map h.map = programAtoms p J (h.map ∘ input) k

Semantic gate extraction commutes with a homomorphism, at every gate index.

def Cslib.Circuits.Fusion.Cover.map {σ : Signature} {U : Type v} {V : Type w} {W : Type z} {I : Interpretation σ U} {J : Interpretation σ V} {P : W → V → Prop} (h : Homomorphism I J) (c : Cover I fun (t : W) => P t ∘ h.map) : Cover J P

Map a cover of pulled-back predicates to a cover of the original predicates.

@[simp]

theorem Cslib.Circuits.Fusion.Cover.size_map {σ : Signature} {U : Type v} {V : Type w} {W : Type z} {I : Interpretation σ U} {J : Interpretation σ V} {P : W → V → Prop} (h : Homomorphism I J) (c : Cover I fun (t : W) => P t ∘ h.map) : (map h c).size = c.size

@[simp]

theorem Cslib.Circuits.Fusion.Cover.atoms_map {σ : Signature} {U : Type v} {V : Type w} {W : Type z} {I : Interpretation σ U} {J : Interpretation σ V} {P : W → V → Prop} (h : Homomorphism I J) (c : Cover I fun (t : W) => P t ∘ h.map) (i : Fin c.size) : (map h c).atoms i = (c.atoms i).map h.map

@[simp]

theorem Cslib.Circuits.Fusion.Cover.cost_map {σ : Signature} {U : Type v} {V : Type w} {W : Type z} {I : Interpretation σ U} {J : Interpretation σ V} {P : W → V → Prop} (h : Homomorphism I J) (c : Cover I fun (t : W) => P t ∘ h.map) (weight : σ.Op → ℕ) : (map h c).cost weight = c.cost weight

Transport preserves arbitrary operation weights, including zero weights and repeated atoms.

theorem Cslib.Circuits.Fusion.coverComplexity_le_comap {σ : Signature} {U : Type v} {V : Type w} {W : Type z} {I : Interpretation σ U} {J : Interpretation σ V} (h : Homomorphism I J) (P : W → V → Prop) (weight : σ.Op → ℕ) : coverComplexity J P weight ≤ coverComplexity I (fun (t : W) => P t ∘ h.map) weight

Image cover complexity lower-bounds the complexity of covering pulled-back predicates.