Barrington's theorem (representation form)

Assembling the three preceding modules — the abstract move-set (Circuits/Barrington.lean), the S₅ cycle algebra (Circuits/BarringtonS5.lean), and the width-5 bridge (Circuits/BarringtonBridge.lean) — this module proves the semantic core of Barrington's theorem by structural recursion on Boolean formulas: every Boolean formula is computed by a width-5 permutation branching program, in the sense that the program evaluates to a fixed nonidentity permutation of S₅ exactly when the formula is true and to the identity otherwise.

The recursion follows the connectives directly: var/tru/fls are the base cases; neg flips the target cycle to its inverse; conj is the target-free AND gate BP.Computes_and5; and disj is De Morgan composed of AND and negation. Each step preserves representation through a genuine 5-cycle, which is what the commutator-trick AND requires.

The length bookkeeping lives in Circuits/BarringtonLength.lean, where length-preserving pointwise conjugation and compact negation sharpen this semantic recursion to the textbook 4^d bound. The nonuniform family lift and converse live in BarringtonFamily.lean and BarringtonConverse.lean.

Main results

• Complexity.Computes_formula — every formula is representable through any chosen 5-cycle target.
• Complexity.barrington_representation — Barrington's theorem, representation form: a width-5 program and a nonidentity σ ∈ S₅ with eval = σ ↔ φ true.
• Complexity.barrington_boolean — the Boolean-decision form: a width-5 program and a query point x whose orbit under the program's value decides φ.

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

Formula representability. For every Boolean formula φ and every target 5-cycle c of S₅, there is a width-5 permutation branching program that represents φ through c — evaluating to c when φ is true and to the identity otherwise. Proved by structural recursion on φ using the bridged Barrington moves.

theorem Complexity.barrington_representation (φ : BoolFormula) : ∃ (r : BP 5) (σ : Equiv.Perm (Fin 5)), σ ≠ 1 ∧ ∀ (α : ℕ → Bool), BP.eval α r = if BoolFormula.eval α φ = true then σ else 1

Barrington's theorem (representation form). Every Boolean formula φ is computed by a width-5 permutation branching program: there is a program r and a nonidentity permutation σ ∈ S₅ such that r evaluates to σ exactly when φ is true and to the identity otherwise. (The concrete witness cycle is finRotate 5.)

theorem Complexity.barrington_boolean (φ : BoolFormula) : ∃ (r : BP 5) (x : Fin 5), ∀ (α : ℕ → Bool), (BP.eval α r) x ≠ x ↔ BoolFormula.eval α φ = true

Barrington's theorem (Boolean-decision form). Every Boolean formula φ is decided by a width-5 permutation branching program: there is a program r and a query point x ∈ Fin 5 such that the program's value moves x exactly when φ is true. Reading (BP.eval α r) x ≠ x therefore computes φ, turning the permutation-valued representation into a genuine Boolean output. (The point x is any point the representing cycle σ moves; σ ≠ 1 guarantees one exists.)