Toward Barrington's theorem: the group-theoretic core

Barrington's theorem builds a width-5 permutation branching program for any NC¹ formula by representing a Boolean function through a fixed non-identity permutation. This module formalizes the reusable, group-theoretic heart of that construction (roadmap track M3), independent of the eventual S₅ choice of permutations.

The central notion is BP.Computes σ p f: the program p represents the Boolean function f through the permutation σ, meaning it evaluates to σ exactly when f holds and to 1 (the identity) otherwise. The closure lemmas proved here are the moves in Barrington's inductive construction:

• conjugation changes the representing permutation, either by wrapping the program (Computes_conj) or pointwise with no length overhead (Computes_conjugate);
• negation flips the function while inverting the permutation, either by appending a constant (Computes_not) or by folding that constant into the final instruction (Computes_not_compact);
• the commutator trick (Computes_and) represents f ∧ g through the commutator ⁅σ, τ⁆ — choosing σ, τ to be 5-cycles in S₅ whose commutator is again a 5-cycle is exactly what makes the AND gate work.

Main definitions and results

• BPInstr.inverse, BP.inverse, BP.eval_inverse — inverting a program inverts the permutation it evaluates to.
• BPInstr.const, BPInstr.eval_const — constant instructions.
• BPInstr.conjugate, BP.conjugate, BP.eval_conjugate — length-preserving pointwise conjugation.
• BPInstr.postMul, BP.postMul, BP.eval_postMul — fold a final constant into the last instruction, adding an instruction only to the empty program.
• BP.Computes, BP.Computes_conj, BP.Computes_not, BP.Computes_not_compact, BP.Computes_and.

def Complexity.BPInstr.inverse {w : ℕ} (ins : BPInstr w) : BPInstr w

Invert a branching-program instruction: keep the variable read, invert both branch permutations.

Equations

• ins.inverse = { var := ins.var, perm0 := ins.perm0⁻¹, perm1 := ins.perm1⁻¹ }

@[simp]

theorem Complexity.BPInstr.eval_inverse {w : ℕ} (α : ℕ → Bool) (ins : BPInstr w) : eval α ins.inverse = (eval α ins)⁻¹

Inverting an instruction inverts the permutation it selects.

def Complexity.BPInstr.const {w : ℕ} (c : Equiv.Perm (Fin w)) : BPInstr w

A constant instruction applies the permutation c regardless of the input.

Equations

• Complexity.BPInstr.const c = { var := 0, perm0 := c, perm1 := c }

@[simp]

theorem Complexity.BPInstr.eval_const {w : ℕ} (α : ℕ → Bool) (c : Equiv.Perm (Fin w)) : eval α (const c) = c

A constant instruction always evaluates to its permutation.

def Complexity.BPInstr.conjugate {w : ℕ} (τ : Equiv.Perm (Fin w)) (ins : BPInstr w) : BPInstr w

Conjugate both branches of an instruction by the same permutation.

Equations

• Complexity.BPInstr.conjugate τ ins = { var := ins.var, perm0 := τ * ins.perm0 * τ⁻¹, perm1 := τ * ins.perm1 * τ⁻¹ }

@[simp]

theorem Complexity.BPInstr.eval_conjugate {w : ℕ} (α : ℕ → Bool) (τ : Equiv.Perm (Fin w)) (ins : BPInstr w) : eval α (conjugate τ ins) = τ * eval α ins * τ⁻¹

Pointwise instruction conjugation realizes group conjugation.

def Complexity.BPInstr.postMul {w : ℕ} (ins : BPInstr w) (c : Equiv.Perm (Fin w)) : BPInstr w

Right-multiply both branches of an instruction by a fixed permutation.

Equations

• ins.postMul c = { var := ins.var, perm0 := ins.perm0 * c, perm1 := ins.perm1 * c }

@[simp]

theorem Complexity.BPInstr.eval_postMul {w : ℕ} (α : ℕ → Bool) (ins : BPInstr w) (c : Equiv.Perm (Fin w)) : eval α (ins.postMul c) = eval α ins * c

Right-multiplication commutes with selecting an instruction branch.

def Complexity.BP.conjugate {w : ℕ} (τ : Equiv.Perm (Fin w)) (p : BP w) : BP w

Conjugate every instruction of a branching program. Unlike wrapping with constant instructions, this operation preserves length exactly.

Equations

• Complexity.BP.conjugate τ p = List.map (Complexity.BPInstr.conjugate τ) p

theorem Complexity.BP.eval_conjugate {w : ℕ} (α : ℕ → Bool) (τ : Equiv.Perm (Fin w)) (p : BP w) : eval α (conjugate τ p) = τ * eval α p * τ⁻¹

Pointwise conjugation conjugates the value of the whole program.

@[simp]

theorem Complexity.BP.length_conjugate {w : ℕ} (τ : Equiv.Perm (Fin w)) (p : BP w) : List.length (conjugate τ p) = List.length p

Pointwise conjugation preserves program length exactly.

def Complexity.BP.postMul {w : ℕ} (p : BP w) (c : Equiv.Perm (Fin w)) : BP w

Fold a final constant multiplication into the last instruction. The empty program has no last instruction, so it becomes a singleton constant program.

Equations

• p.postMul c = if p = [] then [Complexity.BPInstr.const c] else List.modifyLast (fun (ins : Complexity.BPInstr w) => ins.postMul c) p

theorem Complexity.BP.eval_postMul {w : ℕ} (α : ℕ → Bool) (p : BP w) (c : Equiv.Perm (Fin w)) : eval α (p.postMul c) = eval α p * c

Folding a final constant into the last instruction right-multiplies the program value.

theorem Complexity.BP.length_postMul {w : ℕ} (p : BP w) (c : Equiv.Perm (Fin w)) : List.length (p.postMul c) = max 1 (List.length p)

Folding a final constant uses the original length, except that an empty program needs one instruction.

def Complexity.BP.inverse {w : ℕ} (p : BP w) : BP w

Invert a branching program: reverse the instruction list and invert each instruction.

Equations

• p.inverse = (List.map Complexity.BPInstr.inverse p).reverse

theorem Complexity.BP.eval_inverse {w : ℕ} (α : ℕ → Bool) (p : BP w) : eval α p.inverse = (eval α p)⁻¹

Inversion is correct: the inverted program evaluates to the inverse of the original program's permutation.

def Complexity.BP.Computes {w : ℕ} (σ : Equiv.Perm (Fin w)) (p : BP w) (f : (ℕ → Bool) → Bool) : Prop

Computes σ p f : the branching program p represents the Boolean function f through the permutation σ — it evaluates to σ when f holds and to the identity otherwise.

Equations

• Complexity.BP.Computes σ p f = ∀ (α : ℕ → Bool), Complexity.BP.eval α p = if f α = true then σ else 1

theorem Complexity.BP.Computes_conj {w : ℕ} {σ : Equiv.Perm (Fin w)} {p : BP w} {f : (ℕ → Bool) → Bool} (h : Computes σ p f) (τ : Equiv.Perm (Fin w)) : Computes (τ * σ * τ⁻¹) ([BPInstr.const τ] ++ p ++ [BPInstr.const τ⁻¹]) f

Conjugation of the representing permutation. Wrapping a program between a constant τ and a constant τ⁻¹ conjugates the permutation it represents.

theorem Complexity.BP.Computes_conjugate {w : ℕ} {σ : Equiv.Perm (Fin w)} {p : BP w} {f : (ℕ → Bool) → Bool} (h : Computes σ p f) (τ : Equiv.Perm (Fin w)) : Computes (τ * σ * τ⁻¹) (conjugate τ p) f

Length-preserving conjugation. Conjugating every instruction changes the representing permutation without adding constant instructions.

theorem Complexity.BP.Computes_not {w : ℕ} {σ : Equiv.Perm (Fin w)} {p : BP w} {f : (ℕ → Bool) → Bool} (h : Computes σ p f) : Computes σ⁻¹ (p ++ [BPInstr.const σ⁻¹]) fun (α : ℕ → Bool) => !f α

Negation. Appending a constant σ⁻¹ to a program that represents f through σ yields a program representing ¬f through σ⁻¹.

theorem Complexity.BP.Computes_not_compact {w : ℕ} {σ : Equiv.Perm (Fin w)} {p : BP w} {f : (ℕ → Bool) → Bool} (h : Computes σ p f) : Computes σ⁻¹ (p.postMul σ⁻¹) fun (α : ℕ → Bool) => !f α

Compact negation. Multiplying the final selected permutation by σ⁻¹ represents ¬f through σ⁻¹. The multiplication is folded into the last instruction, so the length becomes only max 1 p.length.

theorem Complexity.BP.Computes_and {w : ℕ} {σ τ : Equiv.Perm (Fin w)} {p q : BP w} {f g : (ℕ → Bool) → Bool} (hp : Computes σ p f) (hq : Computes τ q g) : Computes ⁅σ, τ⁆ (p ++ q ++ p.inverse ++ q.inverse) fun (α : ℕ → Bool) => f α && g α

The commutator trick (Barrington's AND gate). If p represents f through σ and q represents g through τ, then the commutator program p q p⁻¹ q⁻¹ represents f ∧ g through the commutator ⁅σ, τ⁆.

When both f and g hold the four factors multiply to σ τ σ⁻¹ τ⁻¹ = ⁅σ, τ⁆; if either fails, the corresponding factor collapses to 1 and the product telescopes to the identity.

theorem Complexity.BP.Computes_false {w : ℕ} (σ : Equiv.Perm (Fin w)) : Computes σ [] fun (x : ℕ → Bool) => false

Base case — constant false. The empty program represents the constant function false through any permutation (it always evaluates to the identity).

theorem Complexity.BP.Computes_true {w : ℕ} (σ : Equiv.Perm (Fin w)) : Computes σ [BPInstr.const σ] fun (x : ℕ → Bool) => true

Base case — constant true. A single constant-σ instruction represents the constant function true through σ.

theorem Complexity.BP.Computes_var {w : ℕ} (σ : Equiv.Perm (Fin w)) (i : ℕ) : Computes σ [{ var := i, perm0 := 1, perm1 := σ }] fun (α : ℕ → Bool) => α i

Base case — a literal. The single instruction reading variable i, which applies σ when the bit is true and the identity when it is false, represents the projection fun α => α i through σ.

theorem Complexity.BP.Computes_or {w : ℕ} {σ τ : Equiv.Perm (Fin w)} {p q : BP w} {f g : (ℕ → Bool) → Bool} (hp : Computes σ p f) (hq : Computes τ q g) : ∃ (μ : Equiv.Perm (Fin w)), ∃ (r : BP w), Computes μ r fun (α : ℕ → Bool) => f α || g α

Disjunction is representable. By De Morgan (f ∨ g = ¬(¬f ∧ ¬g)), the negation and commutator constructions combine to represent f ∨ g. With the base cases (Computes_false, Computes_true, Computes_var) and negation, this gives a functionally complete set of moves for width-w permutation branching programs — the abstract engine of Barrington's induction.