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 the fixed target barringtonTargetBase exactly when the formula is true (and to the identity otherwise), the target is not the identity, and the program's length is at most 4 ^ depth. That the target is a 5-cycle is the separate theorem barringtonTargetBase_spec; this statement records only that it is nonidentity.