Fixed-arity nonuniform Barrington theorem

This is the typed version of Barrington's theorem. At every input length, a formula or branching program carries a proof that it reads only variables in that fixed arity. Both sides denote BoolFunFamily; the branching-program model stores the unique zero-input answer separately.

Main results

• fixedArityFormulaFamily_exists_bp -- logarithmic-depth formulas compile to polynomial-length, variable-bounded width-5 programs.
• fixedArityBPFamily_exists_formula -- balanced formulas give the converse.
• barrington_equivalence -- the typed nonuniform class equivalence.

theorem Complexity.fixedArityFormulaFamily_exists_bp (F : FixedArityFormulaFamily) (hF : F.LogDepth) : ∃ (R : FixedArityBPFamily 5), R.PolynomialLength ∧ R.function = F.function

Every fixed-arity logarithmic-depth formula family has an equivalent fixed-arity polynomial-length width-5 branching-program family.

theorem Complexity.fixedArityBPFamily_exists_formula (R : FixedArityBPFamily 5) (hR : R.PolynomialLength) : ∃ (F : FixedArityFormulaFamily), F.LogDepth ∧ F.function = R.function

Every fixed-arity polynomial-length width-5 branching-program family has an equivalent fixed-arity logarithmic-depth formula family.

theorem Complexity.formulaNC1_subset_width5BP : FormulaNC1 ⊆ Width5BP

Typed logarithmic-depth formula families are contained in typed polynomial-length width-5 branching-program families.

theorem Complexity.width5BP_subset_formulaNC1 : Width5BP ⊆ FormulaNC1

Typed polynomial-length width-5 branching-program families are contained in typed logarithmic-depth formula families.

theorem Complexity.barrington_equivalence : FormulaNC1 = Width5BP

Typed nonuniform Barrington theorem. Variable-bounded, logarithmic-depth formula families compute exactly the same typed Boolean function families as variable-bounded, polynomial-length width-5 permutation branching programs.