Compiling alternating layers to CSLib

The output is a CSLib circuit over Basis.unboundedAndOr.signature. Size counts AND/OR gates and depth counts gate layers; signed inputs cost neither.

theorem Complexity.Shallow.Layer.exists_circuit {n d : ℕ} (f : Layer n (d + 1)) (op : AndOrOp) : ∃ (c : Cslib.Circuits.Circuit Basis.unboundedAndOr.signature n 1), c.size = f.size ∧ c.depth ≤ d + 1 ∧ (c.Computes Basis.unboundedAndOr.interpretation fun (x : Fin n → Bool) (x_1 : Fin 1) => eval op f x) ∧ InputNegationsOnly c

Alternating layers compile to a CSLib circuit with exactly their gate count, without increasing depth.