Spira formula balancing -- proof internals

This file implements the separator-subformula argument behind Spira's balancing theorem. The construction is kept internal; the public surface states only the existence of an equivalent shallow, polynomial-size formula.

theorem Complexity.BoolFormula.exists_spira_balanced_internal (formula : BoolFormula) : ∃ (balanced : BoolFormula), (∀ (assignment : ℕ → Bool), eval assignment balanced = eval assignment formula) ∧ balanced.depth ≤ 15 + 12 * Nat.clog 2 formula.size ∧ balanced.size + 4 ≤ 80 * formula.size ^ 8