Uniform Barrington's Theorem

Complexitylib/Circuits.lean

@@ -7,15 +7,34 @@ import Complexitylib.Circuits.Basic
 import Complexitylib.Circuits.BitString
 import Complexitylib.Circuits.DecisionTree
 import Complexitylib.Circuits.Formula
+import Complexitylib.Circuits.FormulaEncoding
+import Complexitylib.Circuits.FormulaEncoding.Navigation
+import Complexitylib.Circuits.FormulaEncoding.ForwardNavigation
+import Complexitylib.Circuits.FormulaEncoding.BitNavigation
+import Complexitylib.Circuits.FormulaEncoding.ProbeNavigation
+import Complexitylib.Circuits.CircuitFormula
 import Complexitylib.Circuits.Restriction
 import Complexitylib.Circuits.BranchingProgram
 import Complexitylib.Circuits.Barrington
 import Complexitylib.Circuits.BarringtonS5
 import Complexitylib.Circuits.BarringtonBridge
 import Complexitylib.Circuits.BarringtonRepr
 import Complexitylib.Circuits.BarringtonLength
+import Complexitylib.Circuits.BarringtonCompiler
+import Complexitylib.Circuits.BarringtonStreaming
+import Complexitylib.Circuits.BarringtonSlots
+import Complexitylib.Circuits.BarringtonSlotQuery
+import Complexitylib.Circuits.BarringtonTokenQuery
+import Complexitylib.Circuits.BarringtonBitQuery
+import Complexitylib.Circuits.BarringtonBitSerializer
+import Complexitylib.Circuits.BarringtonProbeQuery
+import Complexitylib.Circuits.BarringtonProbeSerializer
+import Complexitylib.Circuits.BranchingProgramEncoding
+import Complexitylib.Circuits.BranchingProgramEncoding.Machine
+import Complexitylib.Circuits.BarringtonCodeGenerator
 import Complexitylib.Circuits.BarringtonFamily
 import Complexitylib.Circuits.BarringtonConverse
+import Complexitylib.Circuits.CircuitFormula.Family
 import Complexitylib.Circuits.MultilinearExtension
 import Complexitylib.Circuits.NormalForm
 import Complexitylib.Circuits.AndOrNot
@@ -28,6 +47,7 @@ import Complexitylib.Circuits.EssentialInput
 import Complexitylib.Circuits.Shannon
 import Complexitylib.Circuits.LowerBound
 import Complexitylib.Circuits.Schnorr
+import Complexitylib.Circuits.DepthClasses
 import Complexitylib.Circuits.AC0
 import Complexitylib.Circuits.Nondeterminism
 import Complexitylib.Circuits.Hardwiring
@@ -84,7 +104,29 @@ convention.
 
 * **Barrington's theorem** (`barrington_equivalence`):
   Logarithmic-depth Boolean formula families are exactly polynomial-length
-  width-`5` permutation branching-program families.
+  width-`5` permutation branching-program families. The finite forward theorem
+  `barrington_representation_depth_four` gives the textbook length bound
+  `4 ^ depth`, and `barrington_quadratic_of_log_depth` specializes it to `n²`
+  at depth at most `log₂ n`.
+  `barringtonCompile_representation` supplies the same finite theorem through
+  an explicit executable compiler rather than an existential choice.
+  `BPCode.Program.decode?_encode` verifies the canonical serialized output
+  format needed by the remaining log-space uniformity proof.
+  `barringtonCompileCode_spec` then connects canonical formula bits to canonical
+  program bits, exact semantics, and a serialized output-size bound.
+  `barringtonCompileStream_instruction?` gives the corresponding exact
+  random-access instruction view without constructing the complete program,
+  while `barringtonCompileSlot?_eq_instruction?` follows one branch of the
+  fixed `4^D` address schedule and returns exactly its selected instruction,
+  while `barringtonCompileTokensSlot?_eq_instruction?` carries that query over
+  canonical postfix tokens using stack-free child-span recovery, and
+  `barringtonCompileBitsSlot?_eq_instruction?` performs the same query directly
+  over canonical encoded formula bits. `barringtonCompileProbeSlot?_eq_instruction?`
+  further replaces the complete bit list by a position-indexed source oracle,
+  with explicit finite decoding fuel. `barringtonCompileBitsCode_eq` then proves
+  the fixed-address two-pass serializer emits the exact canonical code.
+  `BoolFunFamily.onTotalAssignments_mem_Width5BP` applies the theorem to the
+  total-assignment view of an actual typed `NC1` circuit family.
 
 ## Module structure
 
@@ -94,10 +136,40 @@ Public modules (definitions a reviewer should read):
   `CompleteBasis`, `sizeComplexity`, `wireDepth`, `depth`
 * `Complexitylib.Circuits.BitString` — canonical bridges between `BitString n`
   and `List Bool`
+* `Complexitylib.Circuits.CircuitFormula` — exact selected-output unfolding from
+  fan-in-two circuit DAGs to Boolean formulas, with a factor-two depth bound
+* `Complexitylib.Circuits.FormulaEncoding` — canonical iterative postfix formula
+  codec with exact round trips and code length
+* `Complexitylib.Circuits.FormulaEncoding.ProbeNavigation` — exact token,
+  subtree, and child-span navigation through a position-indexed bit oracle
+* `Complexitylib.Circuits.CircuitFormula.Family` — family-level unfolding and
+  the typed-`NC1` bridge to width-`5` branching programs
 * `Complexitylib.Circuits.Family` — circuit families, list semantics, pointwise
   size/depth bounds, and the polynomial-size characterization
 * `Complexitylib.Circuits.BarringtonConverse` — balanced branching-program
   evaluation and the nonuniform Barrington equivalence
+* `Complexitylib.Circuits.BarringtonCompiler` — executable finite `S₅` search
+  and formula-to-program compilation with the `4 ^ depth` bound
+* `Complexitylib.Circuits.BarringtonStreaming` — random-access compilation by
+  instruction index without materializing the complete recursive program
+* `Complexitylib.Circuits.BarringtonSlots` — exact placement of compiled
+  instructions in a depth-bounded fixed-address schedule
+* `Complexitylib.Circuits.BarringtonSlotQuery` — structural first/last occupied
+  addresses and exact direct lookup in that fixed schedule
+* `Complexitylib.Circuits.BarringtonTokenQuery` — the same exact fixed-slot
+  query over canonical postfix token streams, without reconstructing a formula
+* `Complexitylib.Circuits.BarringtonBitQuery` — the fixed-slot query directly
+  over canonical encoded formula bits, with bit-level child-span recovery
+* `Complexitylib.Circuits.BarringtonBitSerializer` — exact two-pass canonical
+  serialization by scanning the fixed encoded-bit address schedule
+* `Complexitylib.Circuits.BarringtonProbeQuery` — exact fixed-address queries
+  through restartable position-indexed formula-code probes
+* `Complexitylib.Circuits.BranchingProgramEncoding` — canonical seven-bit
+  permutation ranks, instruction/program codecs, and exact size bounds
+* `Complexitylib.Circuits.BranchingProgramEncoding.Machine` — framed,
+  one-way machine emission of canonical instruction codes from binary registers
+* `Complexitylib.Circuits.BarringtonCodeGenerator` — the total bitstring-level
+  formula-code-to-program-code reference for promised log-depth `FL` generation
 * `Complexitylib.Circuits.Encoding` — canonical proof-free encoding, validation,
   and iterative evaluation of fan-in-two AND/OR circuits
 * `Complexitylib.Circuits.Encoding.Family` — tagged encoding and evaluation at
@@ -116,7 +188,9 @@ Public modules (definitions a reviewer should read):
   (`two_pow_le_complexity_of_xorBool`)
 * `Complexitylib.Circuits.XOR` — `Schnorr.xorBool` (N-input parity)
 * `Complexitylib.Circuits.EssentialInput` — `IsEssentialInput`, `essentialInputs`
-* `Complexitylib.Circuits.AC0` — `AC0`
+* `Complexitylib.Circuits.DepthClasses` — `DEPTH`, the nonuniform `NC` and `AC`
+  hierarchies, and the aliases `NC0`, `NC1`, and `AC0`
+* `Complexitylib.Circuits.AC0` — compatibility import for `AC0`
 * `Complexitylib.Circuits.Nondeterminism.Defs` — `existsQuantify`, `forallQuantify`
 * `Complexitylib.Circuits.Hardwiring` — exact-size prefix hardwiring
 * `Complexitylib.Circuits.Unrolling` — bounded machine-configuration layouts,

Complexitylib/Circuits/AC0.lean

@@ -4,13 +4,14 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Samuel Schlesinger
 -/
 import Complexitylib.Circuits.AC0.Defs
+import Complexitylib.Circuits.DepthClasses
 
 /-!
 # The class AC⁰
 
-Surface module for `Complexity.AC0`: Boolean-function families computable by
-constant-depth, polynomial-size circuit families of unbounded fan-in AND/OR
-gates with free negation on wires. The definition lives in
-`Complexitylib.Circuits.AC0.Defs`; separation results against AC⁰ are a
-roadmap item and will surface here.
+Compatibility surface for `Complexity.AC0`: Boolean-function families computed
+by constant-depth, polynomial-size circuit families of unbounded fan-in AND/OR
+gates with free negation on wires. The definition and basic API now live in
+`Complexitylib.Circuits.DepthClasses`; separation results against AC⁰ remain
+a roadmap item.
 -/

Complexitylib/Circuits/AC0/Defs.lean

@@ -3,35 +3,12 @@ Copyright (c) 2025 Samuel Schlesinger. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Samuel Schlesinger
 -/
-import Complexitylib.Circuits.AndOrNot.Defs
+import Complexitylib.Circuits.DepthClasses.Defs
 
-/-! # AC0 — Core Definitions
+/-!
+# AC0 -- compatibility import
 
-This module defines the AC0 circuit complexity class.
-
-## Main definitions
-
-* `AC0` — the class of families in AC0 (constant depth, polynomial size,
-  unbounded fan-in AND/OR)
+`Complexity.AC0` now lives with the complete `DEPTH`/`NC`/`AC` hierarchy in
+`Complexitylib.Circuits.DepthClasses.Defs`. This module preserves the original
+import path.
 -/
-
-namespace Complexity
-
-/-- A Boolean function family is in **AC0** if there exist constants `d`
-(depth bound) and `c` (size exponent) such that for every input length
-`N ≥ 1`, some unbounded-fan-in AND/OR circuit of depth at most `d` and
-size at most `N ^ c` computes `f N`.
-
-This captures the standard definition of AC0:
-- **Constant depth**: the circuit depth does not grow with `N`.
-- **Polynomial size**: the number of gates is bounded by a polynomial in `N`.
-- **Unbounded fan-in**: AND and OR gates may have arbitrarily many inputs.
-- **Free negation**: each gate input carries a negation flag (standard in
-  circuit complexity). -/
-def AC0 : Set BoolFunFamily := fun f =>
-  ∃ (d c : Nat), ∀ (N : Nat) [NeZero N],
-    ∃ (G : Nat) (circuit : Circuit Basis.unboundedAndOr N 1 G),
-      circuit.depth ≤ d ∧ circuit.size ≤ N ^ c ∧
-      (fun x => (circuit.eval x) 0) = f N
-
-end Complexity

Complexitylib/Circuits/Barrington.lean

@@ -5,6 +5,7 @@ Authors: Samuel Schlesinger
 -/
 import Complexitylib.Circuits.BranchingProgram
 import Mathlib.Algebra.Group.Commutator
+import Mathlib.Data.List.ModifyLast
 
 /-!
 # Toward Barrington's theorem: the group-theoretic core
@@ -20,9 +21,12 @@ Boolean function `f` through the permutation `σ`, meaning it evaluates to `σ`
 exactly when `f` holds and to `1` (the identity) otherwise. The closure lemmas
 proved here are the moves in Barrington's inductive construction:
 
-- **conjugation** changes the representing permutation (`Computes_conj`);
-- **negation** flips the function while inverting the permutation
-  (`Computes_not`);
+- **conjugation** changes the representing permutation, either by wrapping the
+  program (`Computes_conj`) or pointwise with no length overhead
+  (`Computes_conjugate`);
+- **negation** flips the function while inverting the permutation, either by
+  appending a constant (`Computes_not`) or by folding that constant into the
+  final instruction (`Computes_not_compact`);
 - the **commutator trick** (`Computes_and`) represents `f ∧ g` through the
   commutator `⁅σ, τ⁆` — choosing `σ, τ` to be `5`-cycles in `S₅` whose
   commutator is again a `5`-cycle is exactly what makes the `AND` gate work.
@@ -32,7 +36,12 @@ proved here are the moves in Barrington's inductive construction:
 - `BPInstr.inverse`, `BP.inverse`, `BP.eval_inverse` — inverting a program
   inverts the permutation it evaluates to.
 - `BPInstr.const`, `BPInstr.eval_const` — constant instructions.
-- `BP.Computes`, `BP.Computes_conj`, `BP.Computes_not`, `BP.Computes_and`.
+- `BPInstr.conjugate`, `BP.conjugate`, `BP.eval_conjugate` — length-preserving
+  pointwise conjugation.
+- `BPInstr.postMul`, `BP.postMul`, `BP.eval_postMul` — fold a final constant
+  into the last instruction, adding an instruction only to the empty program.
+- `BP.Computes`, `BP.Computes_conj`, `BP.Computes_not`,
+  `BP.Computes_not_compact`, `BP.Computes_and`.
 -/
 
 open scoped commutatorElement
@@ -60,6 +69,83 @@ def BPInstr.const {w : ℕ} (c : Equiv.Perm (Fin w)) : BPInstr w :=
   simp only [BPInstr.eval, BPInstr.const]
   cases α 0 <;> rfl
 
+/-- Conjugate both branches of an instruction by the same permutation. -/
+def BPInstr.conjugate {w : ℕ} (τ : Equiv.Perm (Fin w))
+    (ins : BPInstr w) : BPInstr w :=
+  { ins with
+    perm0 := τ * ins.perm0 * τ⁻¹
+    perm1 := τ * ins.perm1 * τ⁻¹ }
+
+/-- Pointwise instruction conjugation realizes group conjugation. -/
+@[simp] theorem BPInstr.eval_conjugate {w : ℕ} (α : ℕ → Bool)
+    (τ : Equiv.Perm (Fin w)) (ins : BPInstr w) :
+    BPInstr.eval α (BPInstr.conjugate τ ins) =
+      τ * BPInstr.eval α ins * τ⁻¹ := by
+  simp only [BPInstr.eval, BPInstr.conjugate]
+  cases α ins.var <;> rfl
+
+/-- Right-multiply both branches of an instruction by a fixed permutation. -/
+def BPInstr.postMul {w : ℕ} (ins : BPInstr w)
+    (c : Equiv.Perm (Fin w)) : BPInstr w :=
+  { ins with perm0 := ins.perm0 * c, perm1 := ins.perm1 * c }
+
+/-- Right-multiplication commutes with selecting an instruction branch. -/
+@[simp] theorem BPInstr.eval_postMul {w : ℕ} (α : ℕ → Bool)
+    (ins : BPInstr w) (c : Equiv.Perm (Fin w)) :
+    BPInstr.eval α (BPInstr.postMul ins c) = BPInstr.eval α ins * c := by
+  simp only [BPInstr.eval, BPInstr.postMul]
+  cases α ins.var <;> rfl
+
+/-- Conjugate every instruction of a branching program. Unlike wrapping with
+constant instructions, this operation preserves length exactly. -/
+def BP.conjugate {w : ℕ} (τ : Equiv.Perm (Fin w)) (p : BP w) : BP w :=
+  p.map (BPInstr.conjugate τ)
+
+/-- Pointwise conjugation conjugates the value of the whole program. -/
+theorem BP.eval_conjugate {w : ℕ} (α : ℕ → Bool)
+    (τ : Equiv.Perm (Fin w)) (p : BP w) :
+    BP.eval α (BP.conjugate τ p) = τ * BP.eval α p * τ⁻¹ := by
+  induction p with
+  | nil => simp [BP.conjugate, BP.eval]
+  | cons ins p ih =>
+      rw [show BP.conjugate τ (ins :: p) =
+        BPInstr.conjugate τ ins :: BP.conjugate τ p from rfl]
+      rw [BP.eval_cons, BPInstr.eval_conjugate, ih, BP.eval_cons]
+      simp only [mul_assoc, inv_mul_cancel_left]
+
+/-- Pointwise conjugation preserves program length exactly. -/
+@[simp] theorem BP.length_conjugate {w : ℕ}
+    (τ : Equiv.Perm (Fin w)) (p : BP w) :
+    (BP.conjugate τ p).length = p.length := by
+  simp [BP.conjugate]
+
+/-- Fold a final constant multiplication into the last instruction. The empty
+program has no last instruction, so it becomes a singleton constant program. -/
+def BP.postMul {w : ℕ} (p : BP w) (c : Equiv.Perm (Fin w)) : BP w :=
+  if p = [] then [BPInstr.const c]
+  else p.modifyLast fun ins => BPInstr.postMul ins c
+
+/-- Folding a final constant into the last instruction right-multiplies the
+program value. -/
+theorem BP.eval_postMul {w : ℕ} (α : ℕ → Bool) (p : BP w)
+    (c : Equiv.Perm (Fin w)) :
+    BP.eval α (BP.postMul p c) = BP.eval α p * c := by
+  induction p using List.reverseRecOn with
+  | nil => simp [BP.postMul, BP.eval_singleton]
+  | append_singleton p ins ih =>
+      simp [BP.postMul, List.modifyLast_concat, BP.eval_append,
+        BP.eval_singleton, mul_assoc]
+
+/-- Folding a final constant uses the original length, except that an empty
+program needs one instruction. -/
+theorem BP.length_postMul {w : ℕ} (p : BP w)
+    (c : Equiv.Perm (Fin w)) :
+    (BP.postMul p c).length = max 1 p.length := by
+  induction p using List.reverseRecOn with
+  | nil => simp [BP.postMul]
+  | append_singleton p ins ih =>
+      simp [BP.postMul, List.modifyLast_concat]
+
 /-- Invert a branching program: reverse the instruction list and invert each
     instruction. -/
 def BP.inverse {w : ℕ} (p : BP w) : BP w := (p.map BPInstr.inverse).reverse
@@ -91,6 +177,16 @@ theorem BP.Computes_conj {w : ℕ} {σ : Equiv.Perm (Fin w)} {p : BP w}
   simp only [BP.eval_append, BP.eval_singleton, BPInstr.eval_const, h α]
   rcases Bool.eq_false_or_eq_true (f α) with hf | hf <;> simp [hf]
 
+/-- **Length-preserving conjugation.** Conjugating every instruction changes
+the representing permutation without adding constant instructions. -/
+theorem BP.Computes_conjugate {w : ℕ} {σ : Equiv.Perm (Fin w)} {p : BP w}
+    {f : (ℕ → Bool) → Bool} (h : BP.Computes σ p f)
+    (τ : Equiv.Perm (Fin w)) :
+    BP.Computes (τ * σ * τ⁻¹) (BP.conjugate τ p) f := by
+  intro α
+  rw [BP.eval_conjugate, h α]
+  rcases Bool.eq_false_or_eq_true (f α) with hf | hf <;> simp [hf]
+
 /-- **Negation.** Appending a constant `σ⁻¹` to a program that represents `f`
     through `σ` yields a program representing `¬f` through `σ⁻¹`. -/
 theorem BP.Computes_not {w : ℕ} {σ : Equiv.Perm (Fin w)} {p : BP w}
@@ -100,6 +196,16 @@ theorem BP.Computes_not {w : ℕ} {σ : Equiv.Perm (Fin w)} {p : BP w}
   simp only [BP.eval_append, BP.eval_singleton, BPInstr.eval_const, h α]
   rcases Bool.eq_false_or_eq_true (f α) with hf | hf <;> simp [hf]
 
+/-- **Compact negation.** Multiplying the final selected permutation by `σ⁻¹`
+represents `¬f` through `σ⁻¹`. The multiplication is folded into the last
+instruction, so the length becomes only `max 1 p.length`. -/
+theorem BP.Computes_not_compact {w : ℕ} {σ : Equiv.Perm (Fin w)} {p : BP w}
+    {f : (ℕ → Bool) → Bool} (h : BP.Computes σ p f) :
+    BP.Computes σ⁻¹ (BP.postMul p σ⁻¹) (fun α => !f α) := by
+  intro α
+  rw [BP.eval_postMul, h α]
+  rcases Bool.eq_false_or_eq_true (f α) with hf | hf <;> simp [hf]
+
 /-- **The commutator trick** (Barrington's `AND` gate). If `p` represents `f`
     through `σ` and `q` represents `g` through `τ`, then the commutator program
     `p q p⁻¹ q⁻¹` represents `f ∧ g` through the commutator `⁅σ, τ⁆`.