The S₅ five-cycle commutator (Barrington's non-solvability input)

Barrington's theorem needs a specific algebraic fact about the symmetric group S₅ = Equiv.Perm (Fin 5): there are two 5-cycles whose commutator is again a 5-cycle. This is precisely the failure of solvability of S₅ that lets the commutator-trick AND gate (Circuits/Barrington.lean, BP.Computes_and) hit a genuine 5-cycle target, so the inductive construction can be conjugated to any desired output cycle.

We exhibit an explicit witness — a = finRotate 5 and the 5-cycle b = (0 2 4 3 1) — and verify by kernel computation (decide, hence no native_decide and no extra axioms) that a, b, and ⁅a, b⁆ each have order 5. Order 5 (a prime) together with a nonidentity element forces a single cycle via Equiv.Perm.isCycle_of_prime_order.

Conjugation upgrades the single witness to every 5-cycle: since the 5-cycles form one conjugacy class of S₅ and conjugation distributes over commutators, any 5-cycle is the commutator of two 5-cycles (every_fiveCycle_is_commutator). That is the form Barrington's induction consumes — it may target an arbitrary output cycle.

Main results

• Complexity.isCycle_orderOf_five_of_pow — a nonidentity g : S₅ with g⁵ = 1 is a 5-cycle of order 5.
• Complexity.conj_isCycle_orderOf_five — a conjugate of a 5-cycle is a 5-cycle.
• Complexity.exists_fiveCycle_commutator — two 5-cycles of S₅ whose commutator is again a 5-cycle.
• Complexity.every_fiveCycle_is_commutator — every 5-cycle of S₅ is the commutator of two 5-cycles.

theorem Complexity.isCycle_orderOf_five_of_pow {g : Equiv.Perm (Fin 5)} (h5 : g ^ 5 = 1) (hne : g ≠ 1) : g.IsCycle ∧ orderOf g = 5

A nonidentity permutation of Fin 5 whose fifth power is the identity is a 5-cycle of order 5. (Order divides the prime 5 and is not 1, so it is 5; a prime-order permutation is a single cycle.)

theorem Complexity.conj_isCycle_orderOf_five {a : Equiv.Perm (Fin 5)} (h : a.IsCycle ∧ orderOf a = 5) (g : Equiv.Perm (Fin 5)) : (g * a * g⁻¹).IsCycle ∧ orderOf (g * a * g⁻¹) = 5

A conjugate of a 5-cycle is again a 5-cycle. (Conjugation preserves both g⁵ = 1 — via the homomorphism MulAut.conj — and nonidentity, so isCycle_orderOf_five_of_pow applies to the conjugate.)

theorem Complexity.exists_fiveCycle_commutator : ∃ (a : Equiv.Perm (Fin 5)) (b : Equiv.Perm (Fin 5)), a.IsCycle ∧ orderOf a = 5 ∧ b.IsCycle ∧ orderOf b = 5 ∧ ⁅a, b⁆.IsCycle ∧ orderOf ⁅a, b⁆ = 5

Barrington's S₅ input. There exist two 5-cycles of S₅ whose commutator is again a 5-cycle. The explicit witnesses are finRotate 5 and the 5-cycle (0 2 4 3 1); the order-5 facts are checked by kernel computation.

theorem Complexity.every_fiveCycle_is_commutator (c : Equiv.Perm (Fin 5)) (hc : c.IsCycle) (hco : orderOf c = 5) : ∃ (a : Equiv.Perm (Fin 5)) (b : Equiv.Perm (Fin 5)), a.IsCycle ∧ orderOf a = 5 ∧ b.IsCycle ∧ orderOf b = 5 ∧ ⁅a, b⁆ = c

Every 5-cycle is a commutator of 5-cycles. Combining the single witness exists_fiveCycle_commutator with the fact that the 5-cycles form a single conjugacy class of S₅ (equal cycle type ⟹ conjugate) and that conjugation distributes over the commutator, any 5-cycle c of S₅ can be written as ⁅a, b⁆ for 5-cycles a, b. This is the target-cycle freedom Barrington's AND gate needs.