Circuit composition -- proof internals

theorem Complexity.Gate.eval_rewire_internal {B : Basis} {W W' : ℕ} (gate : Gate B W) (mapWire : Fin W → Fin W') (wireValue : BitString W') : (gate.rewire mapWire).eval wireValue = gate.eval fun (wire : Fin W) => wireValue (mapWire wire)

theorem Complexity.Circuit.wireValue_compose_inner_internal {B : Basis} {N K M G₁ G₂ : ℕ} [NeZero N] [NeZero K] [NeZero M] (outer : Circuit B K M G₂) (inner : Circuit B N K G₁) (input : BitString N) (wire : Fin (N + G₁)) : (outer.compose inner).wireValue input (embedInnerWire wire) = inner.wireValue input wire

theorem Complexity.Circuit.wireValue_compose_innerOutput_internal {B : Basis} {N K M G₁ G₂ : ℕ} [NeZero N] [NeZero K] [NeZero M] (outer : Circuit B K M G₂) (inner : Circuit B N K G₁) (input : BitString N) (output : Fin K) : (outer.compose inner).wireValue input (embedInnerOutput output) = inner.eval input output

theorem Complexity.Circuit.wireValue_compose_outer_internal {B : Basis} {N K M G₁ G₂ : ℕ} [NeZero N] [NeZero K] [NeZero M] (outer : Circuit B K M G₂) (inner : Circuit B N K G₁) (input : BitString N) (wire : Fin (K + G₂)) : (outer.compose inner).wireValue input (embedOuterWire wire) = outer.wireValue (inner.eval input) wire

theorem Complexity.Circuit.eval_compose_internal {B : Basis} {N K M G₁ G₂ : ℕ} [NeZero N] [NeZero K] [NeZero M] (outer : Circuit B K M G₂) (inner : Circuit B N K G₁) (input : BitString N) : (outer.compose inner).eval input = outer.eval (inner.eval input)

Parallel composition

theorem Complexity.Circuit.wireValue_parallel_left_internal {B : Basis} {N K M G₁ G₂ : ℕ} [NeZero N] [NeZero K] [NeZero M] (left : Circuit B N K G₁) (right : Circuit B N M G₂) (input : BitString N) (wire : Fin (N + G₁)) : (left.parallel right).wireValue input (embedParallelLeftWire wire) = left.wireValue input wire

theorem Complexity.Circuit.wireValue_parallel_right_internal {B : Basis} {N K M G₁ G₂ : ℕ} [NeZero N] [NeZero K] [NeZero M] (left : Circuit B N K G₁) (right : Circuit B N M G₂) (input : BitString N) (wire : Fin (N + G₂)) : (left.parallel right).wireValue input (embedParallelRightWire wire) = right.wireValue input wire

theorem Complexity.Circuit.eval_parallel_internal {B : Basis} {N K M G₁ G₂ : ℕ} [NeZero N] [NeZero K] [NeZero M] (left : Circuit B N K G₁) (right : Circuit B N M G₂) (input : BitString N) : (left.parallel right).eval input = Fin.append (left.eval input) (right.eval input)

theorem Complexity.Circuit.size_parallel_internal {B : Basis} {N K M G₁ G₂ : ℕ} [NeZero N] [NeZero K] [NeZero M] (left : Circuit B N K G₁) (right : Circuit B N M G₂) : (left.parallel right).size = left.size + right.size

theorem Complexity.Circuit.exists_parallelFamily_internal {B : Basis} {N : ℕ} [NeZero N] {count : ℕ} [NeZero count] (circuits : Fin count → (internalGates : ℕ) × Circuit B N 1 internalGates) : ∃ (internalGates : ℕ) (packed : Circuit B N count internalGates), packed.size = ∑ i : Fin count, (circuits i).snd.size ∧ ∀ (input : BitString N) (i : Fin count), packed.eval input i = (circuits i).snd.eval input 0

theorem Complexity.Circuit.wireDepth_compose_inner_internal {B : Basis} {N K M G₁ G₂ : ℕ} [NeZero N] [NeZero K] [NeZero M] (outer : Circuit B K M G₂) (inner : Circuit B N K G₁) (wire : Fin (N + G₁)) : (outer.compose inner).wireDepth (embedInnerWire wire) = inner.wireDepth wire

theorem Complexity.Circuit.wireDepth_compose_innerOutput_internal {B : Basis} {N K M G₁ G₂ : ℕ} [NeZero N] [NeZero K] [NeZero M] (outer : Circuit B K M G₂) (inner : Circuit B N K G₁) (output : Fin K) : (outer.compose inner).wireDepth (embedInnerOutput output) = inner.outputDepth output

theorem Complexity.Circuit.wireDepth_compose_outer_le_internal {B : Basis} {N K M G₁ G₂ : ℕ} [NeZero N] [NeZero K] [NeZero M] (outer : Circuit B K M G₂) (inner : Circuit B N K G₁) (wire : Fin (K + G₂)) : (outer.compose inner).wireDepth (embedOuterWire wire) ≤ inner.depth + outer.wireDepth wire

theorem Complexity.Circuit.depth_compose_le_internal {B : Basis} {N K M G₁ G₂ : ℕ} [NeZero N] [NeZero K] [NeZero M] (outer : Circuit B K M G₂) (inner : Circuit B N K G₁) : (outer.compose inner).depth ≤ inner.depth + outer.depth