Conditional circuits give Boolean synthesis bounds

A circuit with formal supplied inputs can be appended to any program already computing those values. All existing wires are preserved, so its gate budget gives CSLib's Synthesis predicate. No converse is asserted: Synthesis quantifies over starting programs and can use all their intermediate wires.

theorem Cslib.Circuits.Boolean.synthesis_of_conditionalGateComplexity_le {n m k : ℕ} (target : Algebraic.Target Bool n m) (supplied : Algebraic.Target Bool n k) (budget : ℕ) (bounded : Circuit.conditionalGateComplexity interpretation target supplied ≤ ↑budget) : Synthesis interpretation (Set.range fun (i : Fin k) (input : Fin n → Bool) => supplied input i) (Set.range fun (i : Fin m) (input : Fin n → Bool) => target input i) budget

A conditional circuit can be instantiated after any program that already computes its supplied family, preserving all existing wire functions.