Semantics-preserving maps between circuit bases -- proof internals

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

theorem Complexity.Circuit.wireValue_mapBasis_internal {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

theorem Complexity.Circuit.eval_mapBasis_internal {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

theorem Complexity.Circuit.wireDepth_mapBasis_internal {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

theorem Complexity.Circuit.outputDepth_mapBasis_internal {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

theorem Complexity.Circuit.depth_mapBasis_internal {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

theorem Complexity.Circuit.size_mapBasis_internal {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

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

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

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