Spira's formula-balancing theorem

Every Boolean formula has an equivalent formula of logarithmic depth and polynomial tree size. The quantitative statement below uses the existing total-node measure: a source formula of size s has an equivalent formula of depth at most 15 + 12 * clog₂(s) and size at most 80 * s ^ 8 - 4.

The construction balances arbitrary formulas, including nested negations. It does not assume a uniform circuit generator: this is a finite, nonuniform transformation.

Main result

• BoolFormula.exists_spira_balanced -- an equivalent logarithmic-depth, polynomial-size Boolean formula.

theorem Complexity.BoolFormula.exists_spira_balanced (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

Spira's balancing theorem. Every Boolean formula has an equivalent formula with logarithmic depth and polynomial tree size. The constants and degree are explicit so downstream family-level theorems need no hidden asymptotic reasoning.