Documentation

Complexitylib.Algebraic.MassProduction.Nonuniform.ResourceBank

One evaluation circuit per resource #

The bank is indexed by the exact resource count, so padding used by routing does not increase the leading evaluation cost. Each member reads its own suffix block and produces one Boolean value.

source
def Algebraic.MassProduction.Nonuniform.ResourceBank.circuit {resources suffixWidth : ℕ} (members : Fin resources → Circuit DeMorgan.signature suffixWidth 1) :
Circuit DeMorgan.signature (resources * suffixWidth) resources

Evaluate every resource once on its own input block. Its gates are exactly the members' gates (circuit_size).

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    @[simp]
    theorem Algebraic.MassProduction.Nonuniform.ResourceBank.circuit_size {resources suffixWidth : ℕ} (members : Fin resources → Circuit DeMorgan.signature suffixWidth 1) :
    (circuit members).size = ∑ resource : Fin resources, (members resource).size

    The bank has exactly the members' gates, one member per resource: routing padding adds no gates.

    source
    theorem Algebraic.MassProduction.Nonuniform.ResourceBank.circuit_eval {resources suffixWidth : ℕ} (members : Fin resources → Circuit DeMorgan.signature suffixWidth 1) (input : Fin (resources * suffixWidth) → Bool) (resource : Fin resources) :
    (circuit members).eval DeMorgan.interpretation input resource = (members resource).eval DeMorgan.interpretation (fun (bit : Fin suffixWidth) => input (finProdFinEquiv (resource, bit))) 0

    Every bank output is exactly its resource's evaluation on its suffix block.

    source
    theorem Algebraic.MassProduction.Nonuniform.ResourceBank.circuit_cost {resources suffixWidth : ℕ} (members : Fin resources → Circuit DeMorgan.signature suffixWidth 1) :
    (circuit members).cost DeMorgan.standardCost = ∑ resource : Fin resources, (members resource).cost DeMorgan.standardCost

    No routing padding is charged as an extra resource evaluation.

    source
    theorem Algebraic.MassProduction.Nonuniform.ResourceBank.circuit_cost_le {resources suffixWidth bound : ℕ} (members : Fin resources → Circuit DeMorgan.signature suffixWidth 1) (bounded : ∀ (resource : Fin resources), (members resource).cost DeMorgan.standardCost ≤ bound) :
    (circuit members).cost DeMorgan.standardCost ≤ resources * bound

    A common resource bound contributes exactly resources * bound.