Minimal Scope for merging Barrington's Theorem in CSLib?

Stream: CSLib

[Anvit Aggarwal]

Hi. I have been working on formalising Barrington's theorem in Lean. Here is the repository:
https://github.com/AnvitAggarwal/barrington-theorem-lean

I posted on the CSLib group a few months ago:
https://leanprover.zulipchat.com/#narrow/channel/513188-CSLib/topic/Formalisation.20of.20Barrington's.20Theorem/with/548137132
and I have tried to incorporate the feedback from that discussion. The main takeaways were:

1. Reduce the usage of simp and split longer proofs.
2. Change the definition of Formula to remove the fixed basis.
3. Generalise some proofs (e.g. using Sym → G instead of Perm (Fin n) and Bool).
4. Prove Barrington’s theorem for branching programs, not only for group programs.

I am currently working on removing the fixed basis and have updated my definition of Formula.
To prove Barrington’s theorem for a general basis, my current plan is:

1. Prove it for OR gates,
2. Use this to show that {AND, OR, NOT} are functionally complete,
3. Extend the proof to a general basis using this.

I would like to ask two things:

1. Does this approach seem reasonable?
2. More importantly, I would like to define a minimal version of this development that would be acceptable for merging into CSLib, before pursuing further generalisations. What would you consider must-have for such a mergeable version, and what would be nice-to-have or suitable for later work?

[Anvit Aggarwal]

Any suggestions would be appreciated. Thanks!

[Anvit Aggarwal]

To make this question easier to answer, let me make it more concrete.
Barrington's theorem states that:
"Every Boolean function computable by a polynomial-size, logarithmic-depth Boolean formula can be computed by a width-5 polynomial-size branching program."
Here's a handout I have been referring to.
Currently, I have defined Formula for a general basis but proved Barrington's theorem only for group programs and not branching programs, and only for the {AND, NOT} basis, and not a general basis. While I plan to define and prove Barrington's theorem for branching programs as well along with a general basis, I wanted to ask whether the current version might be an acceptable first version to get it merged to CSLib.

[Chris Henson]

I am not sure exactly how the group program aspect interacts, but I know that @Alex Meiburg mentioned at #CSLib > Parity is not in AC0 @ 💬 that he's also been working in this area and reached some form of Barrington's theorem. His definitions seem like a fairly general base that may take a bit of time to get PR'd before we are ready for Barrington.