Depth of parallel CSLib circuits

Continuing a program preserves the depths of its existing wires. If the continuation reads only primary inputs, its wires also retain their original depths. Consequently, parallel composition takes the maximum output depth.

@[simp]

theorem Cslib.Circuits.Program.wireDepths_gate_last {σ : Signature} {n g : ℕ} (p : Program σ n g) (l : Line σ n g) : (p.gate l).wireDepths (Wire.gate (Fin.last g)) = l.depth p.wireDepths

theorem Cslib.Circuits.Program.wireDepths_append_castAdd {σ : Signature} {n k g h : ℕ} (p : Program σ n g) (feed : Fin k → Wire n g) (q : Program σ k h) (w : Wire n g) : (p.append feed q).wireDepths (Wire.castAdd h w) = p.wireDepths w

Existing wires keep their depths under continuation.

theorem Cslib.Circuits.Program.wireDepths_append_input {σ : Signature} {n k g h : ℕ} (p : Program σ n g) (select : Fin k → Fin n) (q : Program σ k h) (w : Wire k h) : (p.append (Wire.input ∘ select) q).wireDepths (appendedWire (Wire.input ∘ select) w) = q.wireDepths w

A continuation fed by primary inputs retains its own wire depths.

theorem Cslib.Circuits.Circuit.depth_le_iff {σ : Signature} {n m : ℕ} (c : Circuit σ n m) (d : ℕ) : c.depth ≤ d ↔ ∀ (i : Fin m), c.outputDepths i ≤ d

The circuit depth is bounded exactly when every output depth is bounded.

@[simp]

theorem Cslib.Circuits.Circuit.outputDepths_append_left {σ : Signature} {n m r : ℕ} (c : Circuit σ n m) (d : Circuit σ n r) (i : Fin m) : (c.append d).outputDepths (Fin.castAdd r i) = c.outputDepths i

Parallel composition preserves the depths of the left outputs.

@[simp]

theorem Cslib.Circuits.Circuit.outputDepths_append_right {σ : Signature} {n m r : ℕ} (c : Circuit σ n m) (d : Circuit σ n r) (i : Fin r) : (c.append d).outputDepths (Fin.natAdd m i) = d.outputDepths i

Parallel composition preserves the depths of the right outputs.

theorem Cslib.Circuits.Circuit.depth_append_le {σ : Signature} {n m r : ℕ} (c : Circuit σ n m) (d : Circuit σ n r) (b : ℕ) (hc : c.depth ≤ b) (hd : d.depth ≤ b) : (c.append d).depth ≤ b

A common depth bound survives parallel composition.