The converse direction of Barrington's theorem -- proof internals

This file proves correctness and logarithmic depth for balanced branching-program evaluation, then lifts that construction to polynomial-length families.

theorem Complexity.BP.eval_reachesFormula_internal {w : ℕ} (α : ℕ → Bool) (d : ℕ) (p : BP w) (x y : Fin w) : List.length p ≤ 2 ^ d → (BoolFormula.eval α (reachesFormula d p x y) = true ↔ (eval α p) x = y)

theorem Complexity.BP.depth_reachesFormula_le_internal {w : ℕ} (d : ℕ) (p : BP w) (x y : Fin w) : (reachesFormula d p x y).depth ≤ (w + 1) * d + 1

theorem Complexity.BP.eval_decisionFormula_eq_true_internal {w : ℕ} (α : ℕ → Bool) (p : BP w) (x : Fin w) : BoolFormula.eval α (p.decisionFormula x) = true ↔ (eval α p) x ≠ x

theorem Complexity.BP.depth_decisionFormula_le_internal {w : ℕ} (p : BP w) (x : Fin w) : (p.decisionFormula x).depth ≤ (w + 1) * Nat.clog 2 (List.length p) + 2

theorem Complexity.BP.vars_decisionFormula_lt_internal {w n : ℕ} (p : BP w) (x : Fin w) (hvars : ∀ instruction ∈ p, instruction.var < n) (index : ℕ) : index ∈ (p.decisionFormula x).vars → index < n

theorem Complexity.clog_le_of_polynomial_bound_internal (C p n m : ℕ) (h : m ≤ C * (n + 1) ^ p) : Nat.clog 2 m ≤ Nat.clog 2 C + p * (Nat.log 2 n + 1)

theorem Complexity.BPFamily.toFormulaFamily_computes_internal {w : ℕ} {R : BPFamily w} {x : ℕ → Fin w} {f : ℕ → (ℕ → Bool) → Bool} (h : R.DecidesOnTotalAssignments x f) : (R.toFormulaFamily x).ComputesOnTotalAssignments f

theorem Complexity.BPFamily.toFormulaFamily_logDepth_internal {R : BPFamily 5} {x : ℕ → Fin 5} (h : R.PolynomialLength) : (R.toFormulaFamily x).LogDepth

theorem Complexity.formulaNC1OnTotalAssignments_subset_width5BPOnTotalAssignments_internal : FormulaNC1OnTotalAssignments ⊆ Width5BPOnTotalAssignments

theorem Complexity.width5BPOnTotalAssignments_subset_formulaNC1OnTotalAssignments_internal : Width5BPOnTotalAssignments ⊆ FormulaNC1OnTotalAssignments