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)

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