Documentation

Complexitylib.Algebraic.LowerBound.Hierarchy.Family

Nonuniform circuit size classes and hierarchy #

sizeClass bound consists of Boolean function families computed by circuits of size O(bound n). The definition uses minimum gate count; an equivalence exhibits actual circuit families with the same eventual multiplicative bound. No uniformity or computability of the chosen circuits is asserted.

Below the Shannon scale, an upper budget separated from every constant multiple of a lower budget by the 2 * n interpolation overhead gives a strict inclusion of size classes.

source
@[reducible, inline]
abbrev Algebraic.DeMorgan.FunctionFamily :
Type

One scalar Boolean function at each input width.

Equations
Instances For
    source
    def Algebraic.DeMorgan.sizeClass (bound : ℕ → ℕ) :
    Set FunctionFamily

    Nonuniform size O(bound n), allowing a constant factor and finitely many exceptional widths. All internal De Morgan gates are counted.

    Equations
    Instances For
      source
      theorem Algebraic.DeMorgan.mem_sizeClass_iff (family : FunctionFamily) (bound : ℕ → ℕ) :
      family ∈ sizeClass bound ↔ ∃ (circuits : Circuit.Family signature 1), circuits.Computes interpretation (Target.scalarFamily family) ∧ ∃ (constant : ℕ), ∀ᶠ (n : ℕ) in Filter.atTop, circuits.size n ≤ constant * bound n

      Size-class membership is equivalent to the existence of an actual shared circuit family with an eventual constant-factor size bound.

      source
      theorem Algebraic.DeMorgan.sizeClass_mono {lower upper : ℕ → ℕ} (dominated : ∀ᶠ (n : ℕ) in Filter.atTop, lower n ≤ upper n) :
      sizeClass lower ⊆ sizeClass upper

      Eventual domination of budgets gives inclusion of nonuniform size classes.

      source
      theorem Algebraic.DeMorgan.exists_family_between (budget : ℕ → ℕ) (positive : ∀ᶠ (n : ℕ) in Filter.atTop, 1 ≤ budget n) (small : ∀ᶠ (n : ℕ) in Filter.atTop, budget n ≤ 2 ^ n / n) :
      ∃ (family : FunctionFamily), ∀ᶠ (n : ℕ) in Filter.atTop, budget n < complexity (family n) ∧ complexity (family n) ≤ budget n + 2 * n

      A nonuniform family simultaneously realizes an arbitrary eventual budget below the Shannon scale, with additive error at most twice the width.

      source
      theorem Algebraic.DeMorgan.sizeClass_ssubset_of_gap (lower upper : ℕ → ℕ) (small : ∀ᶠ (n : ℕ) in Filter.atTop, upper n ≤ 2 ^ n / n) (gap : ∀ (constant : ℕ), ∀ᶠ (n : ℕ) in Filter.atTop, constant * lower n + 2 * n + 1 ≤ upper n) :
      sizeClass lower ⊂ sizeClass upper

      General size hierarchy below the Shannon scale. The gap must absorb every constant multiple of the smaller budget and the exact interpolation overhead.