Barrington for log-depth formula families: polynomial-length width-5 programs

Circuits/BarringtonLength.lean proves the textbook per-formula bound barrington_representation_depth_four (a formula of depth d compiles to a width-5 program of length ≤ 4^d). This module lifts that to families: a family of formulas of logarithmic depth is computed, formula by formula, by a family of width-5 permutation branching programs of polynomial length. That is the polynomial-size direction of Barrington's characterization, in the nonuniform (per-length) setting, for untyped FormulaFamily syntax (ℕ → BoolFormula). It is not stated for the library's NC1 class; the class-level results are NC1_subset_Width5BP (in Circuits/CircuitFormula/Family.lean) and barrington_equivalence.

The families here range over the same ℕ → Bool assignments the Barrington development already uses, so FormulaFamily.logDepth_polyLength_bp follows by applying the per-formula bound pointwise, together with the arithmetic fact that 4^{c·log₂ n + c} is bounded by a polynomial in n.

Main definitions and results

• FormulaFamily, FormulaFamily.LogDepth — a family of Boolean formulas and the logarithmic-depth (NC¹) regime.
• four_pow_logDepth_le_poly — the reusable arithmetic conversion from logarithmic depth to a polynomial 4 ^ depth bound.
• FormulaFamily.logDepth_polyLength_bp — the family-level containment.

theorem Complexity.four_pow_logDepth_le_poly (c n : ℕ) : 4 ^ (c * Nat.log 2 n + c) ≤ 4 ^ c * (n + 1) ^ (2 * c)

4^{c·log₂ n + c} ≤ 4^c · (n+1)^{2c}: the construction length for a depth-(c·log₂ n + c) formula is polynomial in n.

def Complexity.FormulaFamily : Type

A family of Boolean formulas, one per input length.

Equations

• Complexity.FormulaFamily = (ℕ → Complexity.BoolFormula)

def Complexity.FormulaFamily.LogDepth (F : FormulaFamily) : Prop

A formula family has logarithmic depth if depth (F n) ≤ c·log₂ n + c for some constant c — the NC¹ depth regime.

Equations

• F.LogDepth = ∃ (c : ℕ), ∀ (n : ℕ), (F n).depth ≤ c * Nat.log 2 n + c

theorem Complexity.FormulaFamily.logDepth_polyLength_bp (F : FormulaFamily) (hF : F.LogDepth) : ∃ (R : ℕ → BP 5) (S : ℕ → Equiv.Perm (Fin 5)) (C : ℕ) (p : ℕ), (∀ (n : ℕ), S n ≠ 1) ∧ (∀ (n : ℕ) (α : ℕ → Bool), BP.eval α (R n) = if BoolFormula.eval α (F n) = true then S n else 1) ∧ ∀ (n : ℕ), List.length (R n) ≤ C * (n + 1) ^ p

Barrington, family level: log-depth formula families ⊆ polynomial-size width-5 branching programs. A logarithmic-depth formula family is computed, formula by formula, by a family of width-5 permutation branching programs whose length is bounded by a fixed polynomial C·(n+1)^p in the input length — with each program evaluating to a nonidentity 5-cycle exactly when its formula is true, on every total assignment ℕ → Bool. The hypothesis is FormulaFamily.LogDepth, not membership in the NC1 class; for that, see NC1_subset_Width5BP and barrington_equivalence.

theorem Complexity.FormulaFamily.logDepth_polyLength_decides (F : FormulaFamily) (hF : F.LogDepth) : ∃ (R : ℕ → BP 5) (x : ℕ → Fin 5) (C : ℕ) (p : ℕ), (∀ (n : ℕ), List.length (R n) ≤ C * (n + 1) ^ p) ∧ ∀ (n : ℕ) (α : ℕ → Bool), (BP.eval α (R n)) (x n) ≠ x n ↔ BoolFormula.eval α (F n) = true

Family-level Barrington, Boolean-decision form. A logarithmic-depth formula family is decided by a family of polynomial-length width-5 branching programs together with a family of query points: reading whether program R n moves point x n computes formula F n.