Documentation

Complexitylib.Circuits.CircuitFormula.Family

Circuit-family outputs as formula families #

This module lifts selected-output circuit unfolding to total families. A typed fan-in-two circuit family yields a formula family with identical semantics and at most twice its depth. Its formulas also read only their declared inputs. Consequently every NC1 Boolean-function family lies in the typed FormulaNC1 class and hence in the typed width-5 class Width5BP.

The explicitly named total-assignment bridge remains available for clients whose functions genuinely have domain ℕ → Bool.

No formula-size bound is used: shared circuit DAGs may expand exponentially when unfolded. Barrington's construction depends on formula depth, which the translation controls directly.

source
theorem Complexity.Circuit.depth_eq_outputDepth_zero {N G : ℕ} [NeZero N] (circuit : Circuit Basis.andOr2 N 1 G) :
circuit.depth = circuit.outputDepth 0

A single-output circuit's global depth is the depth of its unique output.

source
theorem Complexity.CircuitFamily.eval_outputFormulaFamily (F : CircuitFamily Basis.andOr2) (n : ℕ) (assignment : ℕ → Bool) :
BoolFormula.eval assignment (F.outputFormulaFamily n) = F.function n fun (input : Fin n) => assignment ↑input

The unfolded formula at length n has exactly the circuit family's length-n semantics on the corresponding total assignment.

source
theorem Complexity.CircuitFamily.depth_outputFormulaFamily_le (F : CircuitFamily Basis.andOr2) (n : ℕ) :
(F.outputFormulaFamily n).depth ≤ 2 * F.depth n

Family-level selected-output unfolding increases depth by at most a factor of two.

source
theorem Complexity.CircuitFamily.outputFormulaFamily_variables_lt (F : CircuitFamily Basis.andOr2) (n index : ℕ) (hindex : index ∈ (F.outputFormulaFamily n).vars) :
index < n

Every variable mentioned by the unfolded length-n formula lies below the declared input arity n.

source
def Complexity.CircuitFamily.fixedArityOutputFormulaFamily (F : CircuitFamily Basis.andOr2) :
FixedArityFormulaFamily

Package circuit-output unfolding as a genuinely fixed-arity formula family.

Equations
Instances For
    source
    theorem Complexity.CircuitFamily.function_fixedArityOutputFormulaFamily (F : CircuitFamily Basis.andOr2) :
    F.fixedArityOutputFormulaFamily.function = F.function

    The fixed-arity unfolded formula family has exactly the source circuit family's typed semantics.

    source
    theorem Complexity.CircuitFamily.depth_fixedArityOutputFormulaFamily_le (F : CircuitFamily Basis.andOr2) (n : ℕ) :
    F.fixedArityOutputFormulaFamily.depth n ≤ 2 * F.depth n

    The fixed-arity formula packaging preserves the factor-two depth bound.

    source
    theorem Complexity.CircuitFamily.outputFormulaFamily_computes {F : CircuitFamily Basis.andOr2} {f : BoolFunFamily} (hcomputes : F.Computes f) :
    F.outputFormulaFamily.ComputesOnTotalAssignments f.onTotalAssignments

    Unfolding a circuit family computes its total-assignment semantics.

    source
    theorem Complexity.CircuitFamily.outputFormulaFamily_logDepth {F : CircuitFamily Basis.andOr2} {c : ℕ} (hdepth : F.DepthBoundedBy fun (n : ℕ) => c * Nat.log 2 n + c) :
    F.outputFormulaFamily.LogDepth

    A c * log₂ n + c circuit-depth bound produces a logarithmic-depth formula family.

    source
    theorem Complexity.CircuitFamily.fixedArityOutputFormulaFamily_logDepth {F : CircuitFamily Basis.andOr2} {c : ℕ} (hdepth : F.DepthBoundedBy fun (n : ℕ) => c * Nat.log 2 n + c) :
    F.fixedArityOutputFormulaFamily.LogDepth

    A logarithmic circuit-depth bound gives a logarithmic-depth fixed-arity formula family.

    source
    theorem Complexity.NC1_subset_FormulaNC1 :
    NC1 ⊆ FormulaNC1

    Every typed NC1 circuit family has a variable-bounded, logarithmic-depth formula family.

    source
    theorem Complexity.NC1_subset_Width5BP :
    NC1 ⊆ Width5BP

    Every typed NC1 circuit family has a variable-bounded, polynomial-length width-5 permutation branching-program family.

    source
    theorem Complexity.BoolFunFamily.mem_Width5BP {f : BoolFunFamily} (hf : f ∈ NC1) :
    f ∈ Width5BP

    Pointwise typed Barrington theorem for an NC1 Boolean-function family.

    source
    theorem Complexity.NC1_onTotalAssignments_subset_FormulaNC1OnTotalAssignments :
    BoolFunFamily.onTotalAssignments '' NC1 ⊆ FormulaNC1OnTotalAssignments

    The total-assignment views of NC1 Boolean-function families are logarithmic-depth formula families.

    source
    theorem Complexity.BoolFunFamily.onTotalAssignments_mem_FormulaNC1OnTotalAssignments {f : BoolFunFamily} (hf : f ∈ NC1) :
    f.onTotalAssignments ∈ FormulaNC1OnTotalAssignments

    Pointwise form of the bridge from typed NC1 circuit families to logarithmic-depth formula families.

    source
    theorem Complexity.NC1_onTotalAssignments_subset_Width5BPOnTotalAssignments :
    BoolFunFamily.onTotalAssignments '' NC1 ⊆ Width5BPOnTotalAssignments

    Barrington for typed NC1 circuit families. Their total-assignment views have polynomial-length width-5 permutation branching programs.

    source
    theorem Complexity.BoolFunFamily.onTotalAssignments_mem_Width5BPOnTotalAssignments {f : BoolFunFamily} (hf : f ∈ NC1) :
    f.onTotalAssignments ∈ Width5BPOnTotalAssignments

    Pointwise Barrington theorem for a typed NC1 Boolean-function family.