Independent copies of a circuit

Inputs and outputs are arranged in consecutive blocks. A family of circuits runs its members on disjoint blocks and adds their gate counts and arbitrary weighted costs exactly. Replication is the constant family: it preserves sharing between the outputs of each copy, and multiplies both gate count and arbitrary weighted cost exactly. Keeping a positive initial batch requires only input and output wiring. The resulting minimum cost is monotone even at zero copies, where a separate empty circuit suffices.

Main definitions

• Cslib.Circuits.directProduct: independent copies of a scalar function.
• Cslib.Circuits.Circuit.parallelFamily: different circuits on consecutive disjoint blocks.
• Cslib.Circuits.Circuit.replicate: independent copies of a multi-output circuit, the constant family.
• Cslib.Circuits.Circuit.replicateScalar: the single-output specialization.
• Cslib.Circuits.Circuit.takeDirectProductPrefix: retain a positive initial batch.

Main results

• Cslib.Circuits.Circuit.eval_parallelFamily_apply, Cslib.Circuits.Circuit.cost_program_parallelFamily: blockwise semantics and additive cost.
• Cslib.Circuits.Circuit.eval_replicate, Cslib.Circuits.Circuit.cost_program_replicate: exact replication semantics and cost.
• Cslib.Circuits.ecomplexityFrom_directProduct_le: the naive replication upper bound.
• Cslib.Circuits.ecomplexityFrom_directProduct_mono, Cslib.Circuits.complexity_directProduct_mono: monotonicity in the number of copies.
• Cslib.Circuits.ecomplexityFrom_directProduct_comp_wiring_le: blockwise input rewiring.

References

• Adapted from MassProduction/DirectProduct.lean and MassProduction/InputSplit.lean in S. Schlesinger, Boolean circuit mass production formalization.

def Cslib.Circuits.directProductInput {U : Type u} {n k : ℕ} (x : Fin (k * n) → U) (j : Fin k) : Fin n → U

Select one consecutive block of inputs.

def Cslib.Circuits.blockMap {U : Type u} {n m : ℕ} (f : (Fin n → U) → Fin m → U) (k : ℕ) : (Fin (k * n) → U) → Fin (k * m) → U

Apply a multi-output function independently to each input block.

def Cslib.Circuits.directProduct {U : Type u} {n : ℕ} (f : (Fin n → U) → U) (k : ℕ) : (Fin (k * n) → U) → Fin k → U

Apply a scalar function independently to each input block.

@[simp]

theorem Cslib.Circuits.blockMap_apply {U : Type u} {n m k : ℕ} (f : (Fin n → U) → Fin m → U) (x : Fin (k * n) → U) (j : Fin k) (i : Fin m) : blockMap f k x (finProdFinEquiv (j, i)) = f (directProductInput x j) i

def Cslib.Circuits.Circuit.parallelFamily {σ : Signature} {n m k : ℕ} : (Fin k → Circuit σ n m) → Circuit σ (k * n) (k * m)

Circuits of a family run on consecutive disjoint input blocks, preserving sharing within each member. Their outputs are arranged in the same block order.

theorem Cslib.Circuits.Circuit.eval_parallelFamily_apply {σ : Signature} {U : Type u} {n m k : ℕ} (cs : Fin k → Circuit σ n m) (I : Interpretation σ U) (x : Fin (k * n) → U) (j : Fin k) (i : Fin m) : (parallelFamily cs).eval I x (finProdFinEquiv (j, i)) = (cs j).eval I (directProductInput x j) i

Each output of each member reads exactly that member's input block.

theorem Cslib.Circuits.Circuit.cost_program_parallelFamily {σ : Signature} {n m k : ℕ} (cs : Fin k → Circuit σ n m) (cost : σ.Op → ℕ) : (parallelFamily cs).program.cost cost = ∑ j : Fin k, (cs j).program.cost cost

Running a family on disjoint blocks adds arbitrary weighted cost exactly.

@[simp]

theorem Cslib.Circuits.Circuit.size_parallelFamily {σ : Signature} {n m k : ℕ} (cs : Fin k → Circuit σ n m) : (parallelFamily cs).size = ∑ j : Fin k, (cs j).size

Running a family on disjoint blocks adds gate counts exactly.

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

Disjoint-input copies of a circuit, preserving sharing within each copy.

theorem Cslib.Circuits.Circuit.eval_replicate_apply {σ : Signature} {U : Type u} {n m : ℕ} (c : Circuit σ n m) (k : ℕ) (I : Interpretation σ U) (x : Fin (k * n) → U) (j : Fin k) (i : Fin m) : (c.replicate k).eval I x (finProdFinEquiv (j, i)) = c.eval I (directProductInput x j) i

Each output of each copy reads exactly its own input block.

@[simp]

theorem Cslib.Circuits.Circuit.eval_replicate {σ : Signature} {U : Type u} {n m : ℕ} (c : Circuit σ n m) (k : ℕ) (I : Interpretation σ U) (x : Fin (k * n) → U) : (c.replicate k).eval I x = blockMap (c.eval I) k x

Replication computes the blockwise application of the original circuit.

theorem Cslib.Circuits.Circuit.cost_program_replicate {σ : Signature} {n m : ℕ} (c : Circuit σ n m) (k : ℕ) (cost : σ.Op → ℕ) : (c.replicate k).program.cost cost = k * c.program.cost cost

Replication multiplies arbitrary weighted cost exactly.

@[simp]

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

Replication multiplies the gate count exactly.

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

Single-output copies, with one output per input block.

@[simp]

theorem Cslib.Circuits.Circuit.eval_replicateScalar {σ : Signature} {U : Type u} {n : ℕ} (c : Circuit σ n 1) (k : ℕ) (I : Interpretation σ U) (x : Fin (k * n) → U) : (c.replicateScalar k).eval I x = directProduct (fun (y : Fin n → U) => c.eval I y 0) k x

theorem Cslib.Circuits.Circuit.cost_program_replicateScalar {σ : Signature} {n : ℕ} (c : Circuit σ n 1) (k : ℕ) (cost : σ.Op → ℕ) : (c.replicateScalar k).program.cost cost = k * c.program.cost cost

Scalar replication also preserves the exact weighted cost.

@[simp]

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

theorem Cslib.Circuits.Circuit.Computes.replicateScalar {σ : Signature} {U : Type u} {n : ℕ} {c : Circuit σ n 1} {I : Interpretation σ U} {f : (Fin n → U) → U} (hc : c.Computes I (single f)) (k : ℕ) : (c.replicateScalar k).Computes I (directProduct f k)

A scalar computation gives a concrete circuit for every finite direct product.

def Cslib.Circuits.Circuit.takeDirectProductPrefix {σ : Signature} {n large : ℕ} (c : Circuit σ (large * n) large) (small : ℕ) (hsmall : 0 < small) (hle : small ≤ large) : Circuit σ (small * n) small

Retain a positive initial batch by rewiring inputs and selecting outputs, without adding or removing gates. Discarded input blocks read the first retained block.

theorem Cslib.Circuits.Circuit.cost_program_takeDirectProductPrefix {σ : Signature} {n small large : ℕ} (c : Circuit σ (large * n) large) (hsmall : 0 < small) (hle : small ≤ large) (cost : σ.Op → ℕ) : (c.takeDirectProductPrefix small hsmall hle).program.cost cost = c.program.cost cost

Retaining a positive initial batch keeps the exact weighted cost.

theorem Cslib.Circuits.Circuit.Computes.takeDirectProductPrefix {σ : Signature} {U : Type u} {n small large : ℕ} {c : Circuit σ (large * n) large} {I : Interpretation σ U} {f : (Fin n → U) → U} (hc : c.Computes I (directProduct f large)) (hsmall : 0 < small) (hle : small ≤ large) : (c.takeDirectProductPrefix small hsmall hle).Computes I (directProduct f small)

Retaining an initial batch preserves direct-product semantics.

@[simp]

theorem Cslib.Circuits.ecomplexityFrom_directProduct_zero {σ : Signature} {U : Type u} {n : ℕ} {I : Interpretation σ U} {cost : σ.Op → ℕ} {f : (Fin n → U) → U} : ecomplexityFrom I cost (directProduct f 0) id = 0

Zero copies have zero weighted complexity, even for a function with no circuit.

theorem Cslib.Circuits.ecomplexityFrom_directProduct_le {σ : Signature} {U : Type u} {n : ℕ} {I : Interpretation σ U} {cost : σ.Op → ℕ} {f : (Fin n → U) → U} (k : ℕ) : ecomplexityFrom I cost (directProduct f k) id ≤ ↑k * ecomplexityFrom I cost (single f) id

Independently replicating a scalar implementation gives the naive weighted upper bound. The statement includes zero copies and functions of infinite complexity.

theorem Cslib.Circuits.ecomplexityFrom_directProduct_mono {σ : Signature} {U : Type u} {n : ℕ} {I : Interpretation σ U} {cost : σ.Op → ℕ} {f : (Fin n → U) → U} {small large : ℕ} (hle : small ≤ large) : ecomplexityFrom I cost (directProduct f small) id ≤ ecomplexityFrom I cost (directProduct f large) id

Minimum weighted direct-product complexity is monotone in the number of copies.

theorem Cslib.Circuits.ecomplexityFrom_directProduct_comp_wiring_le {σ : Signature} {U : Type u} {n : ℕ} {I : Interpretation σ U} {cost : σ.Op → ℕ} {f : (Fin n → U) → U} {p : ℕ} (select : Fin n → Fin p) (k : ℕ) : ecomplexityFrom I cost (directProduct (fun (x : Fin p → U) => f (x ∘ select)) k) id ≤ ecomplexityFrom I cost (directProduct f k) id

Applying the same input wiring independently in every block adds no weighted cost.

theorem Cslib.Circuits.complexity_directProduct_mono {σ : Signature} {U : Type u} {n : ℕ} {I : Interpretation σ U} {f : (Fin n → U) → U} [I.IsComplete] {small large : ℕ} (hle : small ≤ large) : complexity I (directProduct f small) ≤ complexity I (directProduct f large)

Minimum direct-product size is monotone in the number of copies, including zero copies.

theorem Cslib.Circuits.complexity_directProduct_one_le {σ : Signature} {U : Type u} {n : ℕ} {I : Interpretation σ U} {f : (Fin n → U) → U} [I.IsComplete] : complexity I (directProduct f 1) ≤ complexity I (single f)

One copy costs no more than a single-output implementation.