Barrington's theorem with a length bound

Circuits/BarringtonRepr.lean proves the existence of a width-5 permutation branching program for every Boolean formula, but discards the program's length. This module tracks both the original wrapper-based construction and the optimized textbook construction. Pointwise conjugation retargets a program without changing its length, while compact negation folds the final constant into the last instruction. The resulting binary-gate recurrence is exactly fourfold and proves the classical 4 ^ depth bound.

Main results

• Complexity.BP.length_inverse — program inversion preserves length.
• Complexity.BP.Computes_retarget_len, Complexity.BP.Computes_and5_len — compatibility bounds for the original wrapper construction.
• Complexity.BP.Computes_and5_tight — the exact additive-free commutator length recurrence.
• Complexity.barringtonBound, Complexity.barringtonBound_le — the explicit original length recurrence and its 13 ^ size closed form.
• Complexity.Computes_formula_len — the length-tracked formula recursion.
• Complexity.Computes_formula_depth_four — optimized formula recursion with the textbook 4 ^ depth bound.
• Complexity.barrington_representation_len — Barrington's theorem with the 13 ^ size length bound.
• Complexity.barrington_representation_depth_four — Barrington's theorem with the textbook 4 ^ depth length bound.

theorem Complexity.BP.length_inverse {w : ℕ} (p : BP w) : List.length p.inverse = List.length p

Inverting a branching program preserves its length.

theorem Complexity.BP.Computes_retarget_len {p : BP 5} {f : (ℕ → Bool) → Bool} {σ : Equiv.Perm (Fin 5)} (hp : Computes σ p f) (hσc : σ.IsCycle) (hσo : orderOf σ = 5) {a : Equiv.Perm (Fin 5)} (hac : a.IsCycle) (hao : orderOf a = 5) : ∃ (r : BP 5), Computes a r f ∧ List.length r ≤ List.length p + 2

Compatibility retargeting bound. Pointwise conjugation actually preserves length exactly, which is stronger than the historical two-instruction bound.

theorem Complexity.BP.Computes_and5_len {p q : BP 5} {f g : (ℕ → Bool) → Bool} {σ τ : Equiv.Perm (Fin 5)} (hp : Computes σ p f) (hσc : σ.IsCycle) (hσo : orderOf σ = 5) (hq : Computes τ q g) (hτc : τ.IsCycle) (hτo : orderOf τ = 5) {c : Equiv.Perm (Fin 5)} (hcc : c.IsCycle) (hco : orderOf c = 5) : ∃ (r : BP 5), (Computes c r fun (α : ℕ → Bool) => f α && g α) ∧ List.length r ≤ 2 * List.length p + 2 * List.length q + 8

Length-tracked AND gate: the commutator construction at most doubles the two subprograms and adds a constant from the two retargetings.

theorem Complexity.BP.Computes_and5_tight {p q : BP 5} {f g : (ℕ → Bool) → Bool} {σ τ : Equiv.Perm (Fin 5)} (hp : Computes σ p f) (hσc : σ.IsCycle) (hσo : orderOf σ = 5) (hq : Computes τ q g) (hτc : τ.IsCycle) (hτo : orderOf τ = 5) {c : Equiv.Perm (Fin 5)} (hcc : c.IsCycle) (hco : orderOf c = 5) : ∃ (r : BP 5), (Computes c r fun (α : ℕ → Bool) => f α && g α) ∧ List.length r = 2 * List.length p + 2 * List.length q

Tight Barrington AND gate. Pointwise retargeting has zero overhead, so the commutator program has exactly twice the sum of the two input lengths.

def Complexity.barringtonBound : BoolFormula → ℕ

Explicit length bound for the Barrington branching-program construction, following its recurrence: leaves cost ≤ 1, negation adds 1, and the AND / OR steps double the children and add a constant.

Equations

• Complexity.barringtonBound (Complexity.BoolFormula.var i) = 1
• Complexity.barringtonBound Complexity.BoolFormula.tru = 1
• Complexity.barringtonBound Complexity.BoolFormula.fls = 0
• Complexity.barringtonBound φ.neg = Complexity.barringtonBound φ + 1
• Complexity.barringtonBound (φ.conj ψ) = 2 * Complexity.barringtonBound φ + 2 * Complexity.barringtonBound ψ + 8
• Complexity.barringtonBound (φ.disj ψ) = 2 * Complexity.barringtonBound φ + 2 * Complexity.barringtonBound ψ + 13

theorem Complexity.barringtonBound_le (φ : BoolFormula) : barringtonBound φ ≤ 13 ^ φ.size

The construction bound is dominated by 13 ^ (size φ).

theorem Complexity.barringtonBound_le_pow_depth (φ : BoolFormula) : barringtonBound φ ≤ 17 ^ φ.depth

The construction bound is also dominated by 17 ^ (depth φ). Because depth is the NC¹ measure, this is the load-bearing bound: a formula of depth d = O(log n) compiles to a width-5 program of length 17^d = poly(n) — the NC¹ ⊆ polynomial-size width-5 branching programs direction of Barrington.

theorem Complexity.Computes_formula_len (φ : BoolFormula) (c : Equiv.Perm (Fin 5)) : c.IsCycle → orderOf c = 5 → ∃ (r : BP 5), (BP.Computes c r fun (α : ℕ → Bool) => BoolFormula.eval α φ) ∧ List.length r ≤ barringtonBound φ

Length-tracked formula representability. Every Boolean formula φ is computed through any target 5-cycle by a program of length at most barringtonBound φ. Same recursion as Computes_formula, carrying the length bound through the length-tracked moves.

theorem Complexity.Computes_formula_depth_four (φ : BoolFormula) (c : Equiv.Perm (Fin 5)) : c.IsCycle → orderOf c = 5 → ∃ (r : BP 5), (BP.Computes c r fun (α : ℕ → Bool) => BoolFormula.eval α φ) ∧ List.length r ≤ 4 ^ φ.depth

Textbook depth-tracked formula representability. Every Boolean formula φ is represented through any target 5-cycle by a program of length at most 4 ^ depth φ. Pointwise retargeting contributes no instructions, compact negation contributes no length beyond max 1, and each binary gate uses the four copies in the commutator construction.

theorem Complexity.barrington_representation_len (φ : BoolFormula) : ∃ (r : BP 5) (σ : Equiv.Perm (Fin 5)), σ ≠ 1 ∧ (∀ (α : ℕ → Bool), BP.eval α r = if BoolFormula.eval α φ = true then σ else 1) ∧ List.length r ≤ 13 ^ φ.size

Barrington's theorem with a length bound. Every Boolean formula φ is computed by a width-5 permutation branching program (a nonidentity σ ∈ S₅ with program-value = σ ↔ φ true) whose length is at most 13 ^ (size φ).

theorem Complexity.barrington_representation_depth_four (φ : BoolFormula) : ∃ (r : BP 5) (σ : Equiv.Perm (Fin 5)), σ ≠ 1 ∧ (∀ (α : ℕ → Bool), BP.eval α r = if BoolFormula.eval α φ = true then σ else 1) ∧ List.length r ≤ 4 ^ φ.depth

Barrington's theorem, textbook finite form. Every Boolean formula φ of depth d is computed by a width-5 permutation branching program of length at most 4 ^ d.

theorem Complexity.barrington_representation_depth (φ : BoolFormula) : ∃ (r : BP 5) (σ : Equiv.Perm (Fin 5)), σ ≠ 1 ∧ (∀ (α : ℕ → Bool), BP.eval α r = if BoolFormula.eval α φ = true then σ else 1) ∧ List.length r ≤ 17 ^ φ.depth

Compatibility form of the earlier depth bound. The textbook theorem barrington_representation_depth_four now gives the stronger base 4; this corollary retains the former base-17 API.

theorem Complexity.pow_four_log_le (n : ℕ) (hn : n ≠ 0) : 4 ^ Nat.log 2 n ≤ n ^ 2

4 ^ (log₂ n) ≤ n ^ 2: the arithmetic specialization of the textbook Barrington bound to logarithmic depth.

theorem Complexity.barrington_quadratic_of_log_depth (φ : BoolFormula) (n : ℕ) (hn : n ≠ 0) (hd : φ.depth ≤ Nat.log 2 n) : ∃ (r : BP 5) (σ : Equiv.Perm (Fin 5)), σ ≠ 1 ∧ (∀ (α : ℕ → Bool), BP.eval α r = if BoolFormula.eval α φ = true then σ else 1) ∧ List.length r ≤ n ^ 2

Log-depth formulas have quadratic-length width-5 programs. A formula of depth at most log₂ n compiles to a program of length at most n².

theorem Complexity.pow_seventeen_log_le (n : ℕ) (hn : n ≠ 0) : 17 ^ Nat.log 2 n ≤ n ^ 5

17 ^ (log₂ n) ≤ n ^ 5: since 17 ≤ 2⁵, 17^{log₂ n} ≤ (2^{log₂ n})⁵ ≤ n⁵. This is the arithmetic behind "logarithmic depth gives polynomial size".

theorem Complexity.barrington_poly_of_log_depth (φ : BoolFormula) (n : ℕ) (hn : n ≠ 0) (hd : φ.depth ≤ Nat.log 2 n) : ∃ (r : BP 5) (σ : Equiv.Perm (Fin 5)), σ ≠ 1 ∧ (∀ (α : ℕ → Bool), BP.eval α r = if BoolFormula.eval α φ = true then σ else 1) ∧ List.length r ≤ n ^ 5

NC¹ ⟹ polynomial size (concrete form). A formula of depth at most log₂ n is computed by a width-5 permutation branching program of length at most n ^ 5 — the polynomial-size direction of Barrington made explicit: the program is polynomial-size in n whenever the formula's depth is logarithmic.