An executable Barrington compiler

This module turns the finite Barrington theorem into an explicit recursive compiler. Earlier existence proofs selected S₅ conjugators in Prop; here, allPermutationsFin gives a computable enumeration and firstConjugator5 performs a deterministic finite search. The resulting barringtonCompile contains no choice operation.

For every Boolean formula and target 5-cycle, the compiler returns a width-5 permutation branching program with exact representation semantics and the textbook length bound 4 ^ depth. The remaining work for a fully uniform Barrington theorem is therefore serialization and a resource-bounded generator proof, not extraction of program data from an existential theorem.

Main results

• Complexity.firstConjugator5_spec -- correctness of finite conjugator search.
• Complexity.barrington_commutator -- the searched factors decompose every target 5-cycle.
• Complexity.barringtonCompile_computes -- exact compiler semantics.
• Complexity.barringtonCompile_length_le -- length at most 4 ^ depth.
• Complexity.barringtonCompile_var_bound -- no new queried variables.
• Complexity.barringtonCompile_representation -- constructive finite Barrington theorem for the fixed canonical target cycle.

theorem Complexity.mem_allPermutationsFin {n : ℕ} (permutation : Equiv.Perm (Fin n)) : permutation ∈ allPermutationsFin n

allPermutationsFin n contains every permutation of Fin n.

theorem Complexity.firstConjugator5_spec (source target : Equiv.Perm (Fin 5)) (hexists : ∃ (g : Equiv.Perm (Fin 5)), g * source * g⁻¹ = target) : firstConjugator5 source target * source * (firstConjugator5 source target)⁻¹ = target

If two permutations are conjugate, the executable finite search returns a valid conjugator.

theorem Complexity.barringtonLeftBase_spec : barringtonLeftBase.IsCycle ∧ orderOf barringtonLeftBase = 5

The fixed left base permutation is a 5-cycle.

theorem Complexity.barringtonRightBase_spec : barringtonRightBase.IsCycle ∧ orderOf barringtonRightBase = 5

The fixed right base permutation is a 5-cycle.

theorem Complexity.barringtonTargetBase_spec : barringtonTargetBase.IsCycle ∧ orderOf barringtonTargetBase = 5

The fixed commutator target is a 5-cycle.

theorem Complexity.barringtonLeft_spec (target : Equiv.Perm (Fin 5)) : (barringtonLeft target).IsCycle ∧ orderOf (barringtonLeft target) = 5

The canonical left factor is a 5-cycle for every target value.

theorem Complexity.barringtonRight_spec (target : Equiv.Perm (Fin 5)) : (barringtonRight target).IsCycle ∧ orderOf (barringtonRight target) = 5

The canonical right factor is a 5-cycle for every target value.

theorem Complexity.barrington_commutator (target : Equiv.Perm (Fin 5)) (hcycle : target.IsCycle) (horder : orderOf target = 5) : ⁅barringtonLeft target, barringtonRight target⁆ = target

The executable factors have commutator equal to any target 5-cycle.

theorem Complexity.BP.length_commutatorProgram {w : ℕ} (p q : BP w) : List.length (p.commutatorProgram q) = 2 * List.length p + 2 * List.length q

The four-block commutator program has exactly twice the sum of the source lengths.

theorem Complexity.barringtonCompile_computes (formula : BoolFormula) (target : Equiv.Perm (Fin 5)) (hcycle : target.IsCycle) (horder : orderOf target = 5) : BP.Computes target (barringtonCompile formula target) fun (assignment : ℕ → Bool) => BoolFormula.eval assignment formula

The executable compiler represents a formula through any target 5-cycle.

theorem Complexity.barringtonCompile_length_le (formula : BoolFormula) (target : Equiv.Perm (Fin 5)) : List.length (barringtonCompile formula target) ≤ 4 ^ formula.depth

The executable compiler satisfies the textbook 4 ^ depth length bound.

theorem Complexity.barringtonCompile_var_bound (formula : BoolFormula) (target : Equiv.Perm (Fin 5)) (bound : ℕ) (hvars : ∀ index ∈ formula.vars, index ≤ bound) (instruction : BPInstr 5) : instruction ∈ barringtonCompile formula target → instruction.var ≤ bound

The executable compiler reads no formula-external variable: any bound on the source formula's variable indices bounds every emitted instruction. Constant instructions use variable zero, so the bound is stated for a natural upper bound rather than as a literal subset of formula.vars.

theorem Complexity.barringtonTargetBase_ne_one : barringtonTargetBase ≠ 1

The canonical target cycle is nonidentity.

theorem Complexity.barringtonCompile_representation (formula : BoolFormula) : barringtonTargetBase ≠ 1 ∧ (∀ (assignment : ℕ → Bool), BP.eval assignment (barringtonCompile formula barringtonTargetBase) = if BoolFormula.eval assignment formula = true then barringtonTargetBase else 1) ∧ List.length (barringtonCompile formula barringtonTargetBase) ≤ 4 ^ formula.depth

Constructive finite Barrington theorem. The explicit compiled program evaluates to one fixed nonidentity 5-cycle exactly when the formula is true, and its length is at most 4 ^ depth.