Independent block evaluation

This file formalizes the direct-product operation used by circuit mass production. Inputs are stored as consecutive row-major blocks. It also builds the naive circuit obtained by placing independent copies of one circuit side by side, with exact semantic and cost accounting.

The construction is generic in the signature, interpretation, carrier, and number of outputs. Boolean mass-production theorems specialize the scalar case later.

def Algebraic.MassProduction.scalarTarget {U : Type u_1} {n : ℕ} (function : ScalarFunction U n) : Target U n 1

Regard a scalar function as a one-output target.

Equations

• Algebraic.MassProduction.scalarTarget function input x✝ = function input

def Algebraic.MassProduction.blockPrefixIndex {copies width : ℕ} (index : Fin (copies * width)) : Fin (copies.succ * width)

Embed an index from the initial copies blocks into a layout with one additional final block.

Equations

• Algebraic.MassProduction.blockPrefixIndex index = Fin.cast ⋯ (Fin.castAdd width index)

def Algebraic.MassProduction.blockSuffixIndex {copies width : ℕ} (index : Fin width) : Fin (copies.succ * width)

Embed an index from the final block into a layout with copies preceding blocks.

Equations

• Algebraic.MassProduction.blockSuffixIndex index = Fin.cast ⋯ (Fin.natAdd (copies * width) index)

def Algebraic.MassProduction.blockPrefix {copies width : ℕ} {U : Type u} (input : Fin (copies.succ * width) → U) : Fin (copies * width) → U

Read the initial copies blocks of a layout with one additional final block.

Equations

• Algebraic.MassProduction.blockPrefix input = input ∘ Algebraic.MassProduction.blockPrefixIndex

def Algebraic.MassProduction.blockSuffix {copies width : ℕ} {U : Type u} (input : Fin (copies.succ * width) → U) : Fin width → U

Read the final block of a layout with copies preceding blocks.

Equations

• Algebraic.MassProduction.blockSuffix input = input ∘ Algebraic.MassProduction.blockSuffixIndex

def Algebraic.MassProduction.directProductInput {copies n : ℕ} {U : Sort u_1} (input : Fin (copies * n) → U) (copy : Fin copies) : Fin n → U

Select one row-major input block.

Equations

• Algebraic.MassProduction.directProductInput input copy index = input (finProdFinEquiv (copy, index))

def Algebraic.MassProduction.blockMap {U : Type u_1} {n m : ℕ} (target : Target U n m) (copies : ℕ) : Target U (copies * n) (copies * m)

Apply a vector-valued target independently to consecutive input blocks.

Equations

• One or more equations did not get rendered due to their size.

def Algebraic.MassProduction.directProduct {U : Type u_1} {n : ℕ} (function : ScalarFunction U n) (copies : ℕ) : Target U (copies * n) copies

Evaluate one scalar function independently on copies row-major input blocks and return all answers. This is the target denoted f^{× copies} in the mass-production manuscript.

Equations

• Algebraic.MassProduction.directProduct function copies input copy = function (Algebraic.MassProduction.directProductInput input copy)

@[simp]

theorem Algebraic.MassProduction.directProductInput_apply {copies n : ℕ} {U : Sort u_1} (input : Fin (copies * n) → U) (copy : Fin copies) (index : Fin n) : directProductInput input copy index = input (finProdFinEquiv (copy, index))

@[simp]

theorem Algebraic.MassProduction.blockMap_apply {U : Type u_1} {n m copies : ℕ} (target : Target U n m) (input : Fin (copies * n) → U) (copy : Fin copies) (output : Fin m) : blockMap target copies input (finProdFinEquiv (copy, output)) = target (directProductInput input copy) output

@[simp]

theorem Algebraic.MassProduction.directProduct_apply {U : Type u_1} {n copies : ℕ} (function : ScalarFunction U n) (input : Fin (copies * n) → U) (copy : Fin copies) : directProduct function copies input copy = function (directProductInput input copy)

def Cslib.Circuits.Circuit.replicate {σ : Signature} {n m : ℕ} (circuit : Circuit σ n m) (copies : ℕ) : Circuit σ (copies * n) (copies * m)

Place copies independent, disjoint-input copies of one circuit side by side. Sharing internal to the original circuit is preserved within each copy.

Equations

• One or more equations did not get rendered due to their size.
• circuit.replicate 0 = Cslib.Circuits.Circuit.castCounts ⋯ ⋯ (Cslib.Circuits.Circuit.id σ 0)

theorem Cslib.Circuits.Circuit.eval_replicate_apply {σ : Signature} {n m : ℕ} {U : Type u_2} (circuit : Circuit σ n m) (copies : ℕ) (interpretation : Interpretation σ U) (input : Fin (copies * n) → U) (copy : Fin copies) (output : Fin m) : (circuit.replicate copies).eval interpretation input (finProdFinEquiv (copy, output)) = circuit.eval interpretation (Algebraic.MassProduction.directProductInput input copy) output

Replication evaluates one selected copy exactly as the original circuit on the corresponding row-major input block.

theorem Cslib.Circuits.Circuit.eval_replicate {σ : Signature} {n m : ℕ} {U : Type u_2} (circuit : Circuit σ n m) (copies : ℕ) (interpretation : Interpretation σ U) (input : Fin (copies * n) → U) : (circuit.replicate copies).eval interpretation input = Algebraic.MassProduction.blockMap (circuit.eval interpretation) copies input

Replication applies the original circuit independently to all consecutive input blocks.

@[simp]

theorem Cslib.Circuits.Circuit.cost_replicate {σ : Signature} {n m : ℕ} (circuit : Circuit σ n m) (copies : ℕ) (operationCost : Algebraic.OperationCost σ) : (circuit.replicate copies).cost operationCost = copies * circuit.cost operationCost

Replication has exactly multiplicative weighted cost.

@[simp]

theorem Cslib.Circuits.Circuit.size_replicate {σ : Signature} {n m : ℕ} (circuit : Circuit σ n m) (copies : ℕ) : (circuit.replicate copies).size = copies * circuit.size

Replication has exactly copies times the original gate count.

def Cslib.Circuits.Circuit.replicateScalar {σ : Signature} {n : ℕ} (circuit : Circuit σ n 1) (copies : ℕ) : Circuit σ (copies * n) copies

A scalar circuit replicated on disjoint inputs has the manuscript's direct-product semantics after removing the trivial Fin 1 output factor.

Equations

• circuit.replicateScalar copies = (circuit.replicate copies).mapOutputs fun (copy : Fin copies) => finProdFinEquiv (copy, 0)

@[simp]

theorem Cslib.Circuits.Circuit.eval_replicateScalar {σ : Signature} {n : ℕ} {U : Type u_2} (circuit : Circuit σ n 1) (copies : ℕ) (interpretation : Interpretation σ U) (input : Fin (copies * n) → U) : (circuit.replicateScalar copies).eval interpretation input = Algebraic.MassProduction.directProduct (circuit.outputFunction interpretation 0) copies input

@[simp]

theorem Cslib.Circuits.Circuit.cost_replicateScalar {σ : Signature} {n : ℕ} (circuit : Circuit σ n 1) (copies : ℕ) (operationCost : Algebraic.OperationCost σ) : (circuit.replicateScalar copies).cost operationCost = copies * circuit.cost operationCost

@[simp]

theorem Cslib.Circuits.Circuit.size_replicateScalar {σ : Signature} {n : ℕ} (circuit : Circuit σ n 1) (copies : ℕ) : (circuit.replicateScalar copies).size = copies * circuit.size

theorem Cslib.Circuits.Circuit.replicateScalar_computes_directProduct {σ : Signature} {n : ℕ} {U : Type u_2} {circuit : Circuit σ n 1} {interpretation : Interpretation σ U} {function : Algebraic.ScalarFunction U n} (computes : circuit.outputFunction interpretation 0 = function) (copies : ℕ) : (circuit.replicateScalar copies).ComputesWith interpretation (Algebraic.MassProduction.directProduct function copies)

The concrete naive upper bound: copies disjoint copies of a scalar circuit compute the direct product at exactly multiplicative cost.

theorem Cslib.Circuits.Circuit.outputFunction_eq_of_computes_scalarTarget {σ : Signature} {n : ℕ} {U : Type u_2} {circuit : Circuit σ n 1} {interpretation : Interpretation σ U} {function : Algebraic.ScalarFunction U n} (computes : circuit.ComputesWith interpretation (Algebraic.MassProduction.scalarTarget function)) : circuit.outputFunction interpretation 0 = function

Computation of a one-output target identifies its scalar output function.

Retaining an initial sub-batch

def Cslib.Circuits.Circuit.prefixOrZeroCopy {large : ℕ} (small : ℕ) (smallPositive : 0 < small) (copy : Fin large) : Fin small

Send a copy of a larger batch to the same copy of a smaller batch when it exists, and to copy zero otherwise. The positivity premise is explicit rather than hidden in an instance.

Equations

• Cslib.Circuits.Circuit.prefixOrZeroCopy small smallPositive copy = if bounded : ↑copy < small then ⟨↑copy, bounded⟩ else ⟨0, smallPositive⟩

@[simp]

theorem Cslib.Circuits.Circuit.prefixOrZeroCopy_castLE {small large : ℕ} (smallPositive : 0 < small) (smallLeLarge : small ≤ large) (copy : Fin small) : prefixOrZeroCopy small smallPositive (Fin.castLE smallLeLarge copy) = copy

def Cslib.Circuits.Circuit.prefixBatchInputMap (width small large : ℕ) (smallPositive : 0 < small) : Fin (large * width) → Fin (small * width)

Rewire the inputs expected by a larger batch circuit onto a smaller batch. Inputs belonging to discarded copies are harmlessly redirected to the first retained block.

Equations

• One or more equations did not get rendered due to their size.

theorem Cslib.Circuits.Circuit.directProductInput_prefixBatchInputMap {small large width : ℕ} {U : Sort u_1} (smallPositive : 0 < small) (smallLeLarge : small ≤ large) (input : Fin (small * width) → U) (copy : Fin small) : Algebraic.MassProduction.directProductInput (input ∘ prefixBatchInputMap width small large smallPositive) (Fin.castLE smallLeLarge copy) = Algebraic.MassProduction.directProductInput input copy

def Cslib.Circuits.Circuit.takeDirectProductPrefix {sigma : Signature} {large width : ℕ} (circuit : Circuit sigma (large * width) large) (small : ℕ) (smallPositive : 0 < small) (smallLeLarge : small ≤ large) : Circuit sigma (small * width) small

A circuit for large independent copies yields, without adding gates, a circuit for every positive initial batch of at most large copies.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Cslib.Circuits.Circuit.takeDirectProductPrefix_cost {sigma : Signature} {large width small : ℕ} (circuit : Circuit sigma (large * width) large) (smallPositive : 0 < small) (smallLeLarge : small ≤ large) (operationCost : Algebraic.OperationCost sigma) : (circuit.takeDirectProductPrefix small smallPositive smallLeLarge).cost operationCost = circuit.cost operationCost

@[simp]

theorem Cslib.Circuits.Circuit.takeDirectProductPrefix_size {sigma : Signature} {large width small : ℕ} (circuit : Circuit sigma (large * width) large) (smallPositive : 0 < small) (smallLeLarge : small ≤ large) : (circuit.takeDirectProductPrefix small smallPositive smallLeLarge).size = circuit.size

Retaining an initial sub-batch adds no gates.

theorem Cslib.Circuits.Circuit.takeDirectProductPrefix_computes {sigma : Signature} {large width : ℕ} {U : Type u_2} {interpretation : Interpretation sigma U} {small : ℕ} (circuit : Circuit sigma (large * width) large) (function : Algebraic.ScalarFunction U width) (computes : circuit.ComputesWith interpretation (Algebraic.MassProduction.directProduct function large)) (smallPositive : 0 < small) (smallLeLarge : small ≤ large) : (circuit.takeDirectProductPrefix small smallPositive smallLeLarge).ComputesWith interpretation (Algebraic.MassProduction.directProduct function small)

theorem Cslib.Circuits.Circuit.costComplexity_directProduct_mono_copies {sigma : Signature} {U : Type u_2} {width small large : ℕ} (interpretation : Interpretation sigma U) (operationCost : Algebraic.OperationCost sigma) (function : Algebraic.ScalarFunction U width) (smallPositive : 0 < small) (smallLeLarge : small ≤ large) : costComplexity interpretation operationCost (Algebraic.MassProduction.directProduct function small) ≤ costComplexity interpretation operationCost (Algebraic.MassProduction.directProduct function large)

Minimum direct-product complexity is monotone in the number of positive copies. This is the formal version of fixing unused inputs and discarding unused outputs.

theorem Cslib.Circuits.Circuit.costComplexity_directProduct_le {σ : Signature} {U : Type u_2} {n : ℕ} (interpretation : Interpretation σ U) (operationCost : Algebraic.OperationCost σ) (function : Algebraic.ScalarFunction U n) (copies : ℕ) : costComplexity interpretation operationCost (Algebraic.MassProduction.directProduct function copies) ≤ ↑copies * costComplexity interpretation operationCost (Algebraic.MassProduction.scalarTarget function)

The naive direct-product upper bound for minimum weighted complexity. It is valid even when the one-copy function is not representable, in which case the right side may be ⊤.

theorem Cslib.Circuits.Circuit.gateComplexity_directProduct_le {σ : Signature} {U : Type u_2} {n : ℕ} (interpretation : Interpretation σ U) (function : Algebraic.ScalarFunction U n) (copies : ℕ) : gateComplexity interpretation (Algebraic.MassProduction.directProduct function copies) ≤ ↑copies * gateComplexity interpretation (Algebraic.MassProduction.scalarTarget function)

The naive direct-product upper bound for minimum gate count.