Semantics-preserving maps between circuit bases

A Basis.Hom relabels operations while preserving their arity and exact Boolean semantics. Circuit transport along a homomorphism preserves semantics, gate count, wiring, and depth exactly.

theorem Complexity.Gate.eval_mapBasis {source target : Basis} {W : ℕ} (hom : source.Hom target) (gate : Gate source W) (wireValues : BitString W) : (mapBasis hom gate).eval wireValues = gate.eval wireValues

Gate relabeling preserves evaluation exactly.

theorem Complexity.Circuit.wireValue_mapBasis {N M G : ℕ} [NeZero N] [NeZero M] {source target : Basis} (hom : source.Hom target) (circuit : Circuit source N M G) (input : BitString N) (wire : Fin (N + G)) : (mapBasis hom circuit).wireValue input wire = circuit.wireValue input wire

Basis transport preserves every wire value.

theorem Complexity.Circuit.eval_mapBasis {N M G : ℕ} [NeZero N] [NeZero M] {source target : Basis} (hom : source.Hom target) (circuit : Circuit source N M G) (input : BitString N) : (mapBasis hom circuit).eval input = circuit.eval input

Basis transport preserves circuit semantics exactly.

theorem Complexity.Circuit.wireDepth_mapBasis {N M G : ℕ} [NeZero N] [NeZero M] {source target : Basis} (hom : source.Hom target) (circuit : Circuit source N M G) (wire : Fin (N + G)) : (mapBasis hom circuit).wireDepth wire = circuit.wireDepth wire

Basis transport preserves every wire depth.

theorem Complexity.Circuit.outputDepth_mapBasis {N M G : ℕ} [NeZero N] [NeZero M] {source target : Basis} (hom : source.Hom target) (circuit : Circuit source N M G) (output : Fin M) : (mapBasis hom circuit).outputDepth output = circuit.outputDepth output

Basis transport preserves selected-output depth.

theorem Complexity.Circuit.depth_mapBasis {N M G : ℕ} [NeZero N] [NeZero M] {source target : Basis} (hom : source.Hom target) (circuit : Circuit source N M G) : (mapBasis hom circuit).depth = circuit.depth

Basis transport preserves total circuit depth.

theorem Complexity.Circuit.size_mapBasis {N M G : ℕ} [NeZero N] [NeZero M] {source target : Basis} (hom : source.Hom target) (circuit : Circuit source N M G) : (mapBasis hom circuit).size = circuit.size

Basis transport preserves the G + M size exactly.

theorem Complexity.CircuitFamily.function_mapBasis {source target : Basis} (hom : source.Hom target) (family : CircuitFamily source) : (mapBasis hom family).function = family.function

Basis transport preserves the computed Boolean function family.

theorem Complexity.CircuitFamily.size_mapBasis {source target : Basis} (hom : source.Hom target) (family : CircuitFamily source) : (mapBasis hom family).size = family.size

Basis transport preserves the pointwise family-size function.

theorem Complexity.CircuitFamily.depth_mapBasis {source target : Basis} (hom : source.Hom target) (family : CircuitFamily source) : (mapBasis hom family).depth = family.depth

Basis transport preserves the pointwise family-depth function.