Documentation

Complexity.Computability.Circuit.Boolean.MassProduction.Fine

Fine mass production #

The construction for 2 ^ D copies of a function on p + w inputs:

  1. Store, for every suffix, the 2 ^ p values of the prefixes in copies codewords of a high-rate line-parity code on K ^ ℓ, with K a field of 2 ^ b elements (LineCode.HighRate.exists_lineCode). Every bit of every code coordinate is a resource function of the suffix; there are copies * card K ^ ℓ * b of them.
  2. A scheduler circuit gives every request a punctured line through its information point, with the lines of distinct requests disjoint (IsScheduler). It exists, with near-linear size, whenever universal menus exist (SchedulerSizeBound), and they do under the direction budget (LineCode.exists_isUniversalMenu).
  3. A pipeline looks up the information points, routes every suffix to the resources on its line, evaluates each resource once and sums the returned bits (PipelineSizeBound).

With the parameters of MassProduction.Fine, the resource bank costs (1 + o(1)) / (1 - γ) · 2 ^ n / n and every other circuit is exponentially smaller.

SchedulerSizeBound and PipelineSizeBound are the two circuit-size contracts; this module derives the core fine theorem from them (fineMassProducesThrough_of_bounds) and discharges both (schedulerSizeBound, pipelineSizeBound). Sizes count every gate. These are bounds on circuit size, not on the running time of any circuit constructor.

Main definitions #

Main results #

References #

source
def Cslib.Circuits.Boolean.MassProduction.SchedulerSizeBound (A E : ℕ) :
Prop

Schedulers of size at most A * 2 ^ D * (s + 1) * (D + ℓ * b + 2) ^ E exist for 2 ^ D requests whenever universal menus exist for every number of pending requests.

Instances For
    source
    def Cslib.Circuits.Boolean.MassProduction.PipelineSizeBound (A E : ℕ) :
    Prop

    The finite composition bound: t copies of a function on p + w inputs cost a scheduler, the resource bank and an overhead of at most A * (2 ^ p + t * (s + 1) + copies * (s + 1) ^ ℓ) * (p + w + ℓ * b + log₂ (t + copies) + 2) ^ E gates.

    Instances For
      source
      theorem Cslib.Circuits.Boolean.MassProduction.pow_le_pow_add {B E E' x : ℕ} (hx : x ≤ B) (hB : 1 ≤ B) :
      x ^ E ≤ B ^ (E + E')
      source
      theorem Cslib.Circuits.Boolean.MassProduction.exists_complexity_le_of_bounds {A₁ E₁ A₂ E₂ : ℕ} (hS : SchedulerSizeBound A₁ E₁) (hP : PipelineSizeBound A₂ E₂) {X p w ℓ h m D L : ℕ} (hX : 0 < X) (hh : 0 < h) (hm : 0 < m) (hℓh : ℓ ≤ 2 ^ h) (hrate : X * (2 ^ (h * ℓ) - 1) ≤ m) (hbudget : 9 + D ≤ (ℓ - 2) * (h * m)) (hloss : X * (h * m) * 2 ^ (ℓ * (h * m)) ≤ 2 ^ p) (hL : ∀ (g : BooleanFunction w), complexity interpretation (single g) ≤ L) (f : BooleanFunction (p + w)) :
      ∃ (R : ℕ) (O : ℕ), complexity interpretation (directProduct f (2 ^ D)) ≤ R * L + O ∧ X * R ≤ (X + 2) * 2 ^ p ∧ O ≤ (A₁ + 4 * A₂) * (2 ^ p + 2 ^ (D + h * m)) * (2 * (p + w) + ℓ * (h * m) + D + 4) ^ (E₁ + E₂)

      The finite fine bound at one input length. With a field of 2 ^ (h * m) elements, ℓ ≤ 2 ^ h, enough blocks for the rate precision X, the direction budget, a negligible last code copy and single copies of size at most L on w inputs, the 2 ^ D copies of every function on p + w inputs cost a resource bank R * L with X R ≤ (X + 2) 2 ^ p, plus an overhead O exponentially smaller than 2 ^ (p + w).

      source
      theorem Cslib.Circuits.Boolean.MassProduction.pipelineSizeBound :
      PipelineSizeBound 1444 4

      The pipeline of MassProduction.Pipeline satisfies the composition contract.

      source
      theorem Cslib.Circuits.Boolean.MassProduction.fineMassProducesThrough_of_bounds {A₁ E₁ A₂ E₂ : ℕ} (hS : SchedulerSizeBound A₁ E₁) (hP : PipelineSizeBound A₂ E₂) {num den : ℕ} (hnd : num < den) :
      FineMassProducesThrough num den

      Fine mass production from the circuit contracts. If schedulers and the pipeline obey polynomial size bounds, then at every rational exponent num / den < 1 and positive precision P, eventually every function on n inputs has k ≤ 2 ^ (⌊num n / den⌋ + 1) copies of cost at most (1 + 1 / P) den / (den - num) · 2 ^ n / n.

      source
      theorem Cslib.Circuits.Boolean.MassProduction.schedulerSizeBound :
      SchedulerSizeBound 524288 5

      The halving scheduler of MassProduction.Scheduler satisfies the scheduler contract.

      source
      theorem Cslib.Circuits.Boolean.MassProduction.fineMassProducesThrough {num den : ℕ} (hnd : num < den) :
      FineMassProducesThrough num den

      Fine mass production at every rational exponent num / den < 1: for every precision P, eventually every function on n inputs has k ≤ 2 ^ (⌊num n / den⌋ + 1) copies of cost c with P (den - num) n c ≤ (P + 1) den 2 ^ n, that is, at most (1 + 1 / P) / (1 - num / den) · 2 ^ n / n when P > 0.

      source
      theorem Cslib.Circuits.Boolean.MassProduction.fineMassProducesAt {num den : ℕ} (hnd : num < den) :
      FineMassProducesAt num den

      The source's statement at every rational exponent below one.

      source
      theorem Cslib.Circuits.Boolean.MassProduction.exponentialMassProduction :
      ExponentialMassProduction

      Exponential-range mass production: every fixed rational exponent below one has a constant coefficient at every positive input length.

      source
      theorem Cslib.Circuits.Boolean.MassProduction.realFineMassProduction :
      RealFineMassProduction

      Fine mass production for real rates: for every real 0 ≤ γ < 1 and every ε > 0, eventually every positive number of copies at most 2 ^ (γ n) costs at most (1 / (1 - γ) + ε) 2 ^ n / n.