Barrington: bridging the abstract move-set to the S₅ cycle algebra

Circuits/Barrington.lean develops the width-w representation predicate BP.Computes and its closure moves (conjugation, negation, the commutator-trick AND, OR). Circuits/BarringtonS5.lean proves the group-theoretic S₅ input: every 5-cycle is the commutator of two 5-cycles. This module joins the two, specializing to width 5, to obtain the moves in the form Barrington's induction actually consumes — where the target representing cycle is an arbitrary 5-cycle rather than whatever the subprograms happened to produce.

Main results

• Complexity.BP.Computes_retarget — a program representing f through one 5-cycle can be rebuilt to represent f through any chosen 5-cycle (5-cycles are conjugate, and pointwise conjugation preserves length).
• Complexity.BP.Computes_retarget_length — the retargeted program has exactly the original length.
• Complexity.BP.Computes_and5 — given subprograms representing f and g through 5-cycles, f ∧ g is representable through any target 5-cycle. This is Barrington's AND gate with full target-cycle freedom, the exact shape the formula induction needs.

theorem Complexity.BP.Computes_retarget {p : BP 5} {f : (ℕ → Bool) → Bool} {σ : Equiv.Perm (Fin 5)} (hp : Computes σ p f) (hσc : σ.IsCycle) (hσo : orderOf σ = 5) {a : Equiv.Perm (Fin 5)} (hac : a.IsCycle) (hao : orderOf a = 5) : ∃ (r : BP 5), Computes a r f

Retargeting. If p represents f through a 5-cycle σ, then for any 5-cycle a there is a program representing f through a. (The two 5-cycles are conjugate — isConj_iff_cycleType_eq — and pointwise conjugation changes the representing permutation without adding instructions.)

theorem Complexity.BP.Computes_retarget_length {p : BP 5} {f : (ℕ → Bool) → Bool} {σ : Equiv.Perm (Fin 5)} (hp : Computes σ p f) (hσc : σ.IsCycle) (hσo : orderOf σ = 5) {a : Equiv.Perm (Fin 5)} (hac : a.IsCycle) (hao : orderOf a = 5) : ∃ (r : BP 5), Computes a r f ∧ List.length r = List.length p

Exact-length retargeting. Retargeting between 5-cycles by pointwise conjugation preserves program length exactly.

theorem Complexity.BP.Computes_and5 {p q : BP 5} {f g : (ℕ → Bool) → Bool} {σ τ : Equiv.Perm (Fin 5)} (hp : Computes σ p f) (hσc : σ.IsCycle) (hσo : orderOf σ = 5) (hq : Computes τ q g) (hτc : τ.IsCycle) (hτo : orderOf τ = 5) {c : Equiv.Perm (Fin 5)} (hcc : c.IsCycle) (hco : orderOf c = 5) : ∃ (r : BP 5), Computes c r fun (α : ℕ → Bool) => f α && g α

Barrington's AND gate, with target-cycle freedom. Given subprograms representing f and g each through some 5-cycle, and any chosen target 5-cycle c, there is a program representing f ∧ g through c.

Proof: c = ⁅a, b⁆ for 5-cycles a, b (every_fiveCycle_is_commutator); retarget the two subprograms to a and b; the commutator trick (BP.Computes_and) then represents f ∧ g through ⁅a, b⁆ = c.