Circuit depth bounds

This file proves bounds for Program.depth, defined in Cslib.Computability.Circuit.Program, and Circuit.depth, defined in Cslib.Computability.Circuit.Basic. Program depth is the maximum depth of its gates; circuit depth is the maximum depth of its designated outputs. Program.depth_le_iff and Circuit.depth_le_iff express bounds in terms of the individual gates and outputs. These characterizations give Circuit.depth_le_program_depth and Circuit.depth_le_size without assumptions on the signature's fan-in or its interpretation.

Constructor simplification lemmas preserve the depth of earlier wires when a gate is added. Every gate, including a constant gate, contributes one level; selecting outputs contributes none. A circuit with no outputs has depth zero, even when its program contains gates.

theorem Cslib.Circuits.Line.depth_le_add_one_iff {σ : Signature} {n g : ℕ} (line : Line σ n g) (depths : Wire n g → ℕ) {d : ℕ} : line.depth depths ≤ d + 1 ↔ ∀ (j : Fin (σ.Arity line.op)), depths (line.wires j) ≤ d

Bounding every argument by d bounds the gate's depth by d + 1.

theorem Cslib.Circuits.Line.depth_pos {σ : Signature} {n g : ℕ} (line : Line σ n g) (depths : Wire n g → ℕ) : 0 < line.depth depths

Every gate, including a constant gate, has positive depth.

@[simp]

theorem Cslib.Circuits.Program.depths_gate_last {σ : Signature} {n g : ℕ} (p : Program σ n g) (line : Line σ n g) : (p.gate line).depths (Fin.last g) = line.depth p.wireDepths

@[simp]

theorem Cslib.Circuits.Program.depths_gate_castSucc {σ : Signature} {n g : ℕ} (p : Program σ n g) (line : Line σ n g) (j : Fin g) : (p.gate line).depths j.castSucc = p.depths j

@[simp]

theorem Cslib.Circuits.Program.wireDepths_input {σ : Signature} {n g : ℕ} (p : Program σ n g) (i : Fin n) : p.wireDepths (Wire.input i) = 0

@[simp]

theorem Cslib.Circuits.Program.wireDepths_gateWire {σ : Signature} {n g : ℕ} (p : Program σ n g) (j : Fin g) : p.wireDepths (Wire.gate j) = p.depths j

@[simp]

theorem Cslib.Circuits.Program.wireDepths_gate_castSucc {σ : Signature} {n g : ℕ} (p : Program σ n g) (line : Line σ n g) (w : Wire n g) : (p.gate line).wireDepths w.castSucc = p.wireDepths w

@[simp]

theorem Cslib.Circuits.Program.depth_empty {σ : Signature} {n : ℕ} : empty.depth = 0

@[simp]

theorem Cslib.Circuits.Program.depth_gate {σ : Signature} {n g : ℕ} (p : Program σ n g) (line : Line σ n g) : (p.gate line).depth = max p.depth (line.depth p.wireDepths)

theorem Cslib.Circuits.Program.depth_le_iff {σ : Signature} {n g : ℕ} (p : Program σ n g) {d : ℕ} : p.depth ≤ d ↔ ∀ (j : Fin g), p.depths j ≤ d

Program depth is bounded by d exactly when every gate depth is bounded by d.

theorem Cslib.Circuits.Program.depths_le_depth {σ : Signature} {n g : ℕ} (p : Program σ n g) (j : Fin g) : p.depths j ≤ p.depth

Every gate depth is at most the depth of the program.

theorem Cslib.Circuits.Program.wireDepths_le_depth {σ : Signature} {n g : ℕ} (p : Program σ n g) (w : Wire n g) : p.wireDepths w ≤ p.depth

Every input or gate wire has depth at most the depth of the program.

theorem Cslib.Circuits.Program.depth_le_gateCount {σ : Signature} {n g : ℕ} (p : Program σ n g) : p.depth ≤ g

A program's depth is at most its number of gates.

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

Circuit depth is bounded by d exactly when every designated output depth is bounded by d.

theorem Cslib.Circuits.Circuit.outputDepths_le_depth {σ : Signature} {n m : ℕ} (c : Circuit σ n m) (j : Fin m) : c.outputDepths j ≤ c.depth

Every designated output has depth at most the circuit depth.

theorem Cslib.Circuits.Circuit.depth_le_program_depth {σ : Signature} {n m : ℕ} (c : Circuit σ n m) : c.depth ≤ c.program.depth

Selecting outputs cannot increase the maximum depth over all program gates.

theorem Cslib.Circuits.Circuit.depth_le_size {σ : Signature} {n m : ℕ} (c : Circuit σ n m) : c.depth ≤ c.size

Circuit depth is at most the number of gates.

@[simp]

theorem Cslib.Circuits.Circuit.depth_zero_outputs {σ : Signature} {n : ℕ} (c : Circuit σ n 0) : c.depth = 0