Proofs and CSLib compilation for alternating layers

Parallel subcircuits retain their depths. The combining gate consumes signed outputs directly, so primary-input negations require no separate gate layer.

theorem Complexity.Shallow.Layer.size_mapInputs {n m d : ℕ} (ρ : Fin n → Fin m × Bool) (f : Layer n d) : (mapInputs ρ f).size = f.size

theorem Complexity.Shallow.Layer.eval_mapInputs {n m d : ℕ} (ρ : Fin n → Fin m × Bool) (f : Layer n d) (op : AndOrOp) (x : BitString m) : eval op (mapInputs ρ f) x = eval op f fun (i : Fin n) => (ρ i).2 ^^ x (ρ i).1

theorem Complexity.Shallow.Layer.eval_neg {n d : ℕ} (f : Layer n d) (op : AndOrOp) (x : BitString n) : eval op.dual f.neg x = !eval op f x

theorem Complexity.Shallow.Layer.exists_signed_circuit {n d : ℕ} (f : Layer n d) (op : AndOrOp) : ∃ (c : Cslib.Circuits.Circuit Basis.unboundedAndOr.signature n 1) (b : Bool), c.size = f.size ∧ c.depth ≤ d ∧ (∀ (x : Fin n → Bool), (b ^^ c.eval Basis.unboundedAndOr.interpretation x 0) = eval op f x) ∧ (0 < d → b = false) ∧ InputNegationsOnly c