feat(circuit): certify exact balanced-code generation

Complexity.lean

@@ -117,6 +117,7 @@ public import Complexity.Computability.Circuit.Boolean.AffineDisperser.Step
 public import Complexity.Computability.Circuit.Boolean.AltFormula
 public import Complexity.Computability.Circuit.Boolean.AltFormula.TopDown
 public import Complexity.Computability.Circuit.Boolean.AtLeast
+public import Complexity.Computability.Circuit.Boolean.BalancedCode
 public import Complexity.Computability.Circuit.Boolean.Barrington
 public import Complexity.Computability.Circuit.Boolean.BarringtonClass
 public import Complexity.Computability.Circuit.Boolean.BatchLookup

Complexity/Computability/Circuit/Balanced.lean

@@ -34,6 +34,7 @@ not charge the fallback. Appending circuits duplicates their programs, even on s
 
 * `Cslib.Circuits.Circuit.eval_balanced`: it computes the balanced fold of their values.
 * `Cslib.Circuits.Circuit.size_balanced`: its size, for a nonempty list.
+* `Cslib.Circuits.Circuit.size_balanced_le`: a uniform bound including the empty fallback.
 * `Cslib.Circuits.Circuit.depth_balanced_le`: its depth.
 
 ## References
@@ -80,6 +81,16 @@ theorem size_balanced (op : Circuit σ (r + r) r) (unit : Circuit σ n r)
     ha, hb, Nat.add_sub_cancel, Nat.add_sub_cancel, show a + 1 + (b + 1) - 1 = a + b + 1 by omega]
   ring
 
+/-- A uniform gate bound also covering the empty fallback and an unused expensive operator. -/
+theorem size_balanced_le (op : Circuit σ (r + r) r) (unit : Circuit σ n r)
+    (l : List (Circuit σ n r)) :
+    (balanced op unit l).size ≤ unit.size + (l.map size).sum + l.length * op.size := by
+  by_cases hl : l = []
+  · simp [hl, balanced]
+  · rw [size_balanced op unit hl]
+    have := Nat.mul_le_mul_right op.size (Nat.sub_le l.length 1)
+    omega
+
 /-- **Depth of a balanced tree of circuits.** If every circuit of a list of `k` circuits has depth
 at most `D`, then combining them by `op` along a balanced tree gives depth at most
 `D + depth op * ⌈log₂ k⌉`. -/