Boolean circuit mass production

Mass complexity is the minimum cost of evaluating a Boolean function on several independent input blocks. Constants are free; NOT, AND and OR each cost one. The circuits and interpretation are CSLib's, and the minimum is the existing weighted source complexity with raw inputs supplied.

The discrete exponential copy budget is 2 ^ (numerator * inputs / denominator), with natural division implementing the floor. The bounding constant is chosen before the input length, function and number of copies. These definitions state the eventual and every-positive-length versions; the exponential-range theorem requires further constructions.

Main definitions

• Cslib.Circuits.Boolean.MassProduction.massComplexity: minimum cost of independent copies.
• Cslib.Circuits.Boolean.MassProduction.MassProductionBound: the bound at one input length.
• Cslib.Circuits.Boolean.MassProduction.MassProducesAt: the eventual rational-rate statement.
• Cslib.Circuits.Boolean.MassProduction.ExponentialMassProduction: the all-length statement for every fixed nonnegative rational exponent below one.

Main results

• Cslib.Circuits.Boolean.MassProduction.massComplexity_le_iff: a finite budget has a circuit.
• Cslib.Circuits.Boolean.MassProduction.massComplexity_mono: monotonicity in the copy count.
• Cslib.Circuits.Boolean.MassProduction.massComplexity_le_complexity: comparison with size.
• Cslib.Circuits.Boolean.MassProduction.massComplexity_le_replicate: the naive upper bound.

References

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

noncomputable def Cslib.Circuits.Boolean.MassProduction.massComplexity {n : ℕ} (f : (Fin n → Bool) → Bool) (k : ℕ) : ℕ∞

Minimum cost of evaluating f on independent blocks, with constants free.

theorem Cslib.Circuits.Boolean.MassProduction.massComplexity_le_iff {n k : ℕ} {f : (Fin n → Bool) → Bool} {b : ℕ} : massComplexity f k ≤ ↑b ↔ ∃ (c : Circuit signature (k * n) k), c.Computes interpretation (directProduct f k) ∧ c.program.cost nonconstantCost ≤ b

Every finite bound is witnessed by a circuit with that nonconstant-gate budget.

theorem Cslib.Circuits.Boolean.MassProduction.massComplexity_ne_top {n k : ℕ} {f : (Fin n → Bool) → Bool} : massComplexity f k ≠ ⊤

The Boolean basis implements every finite direct product, including at zero inputs.

theorem Cslib.Circuits.Boolean.MassProduction.exists_computes_cost_eq_massComplexity {n k : ℕ} {f : (Fin n → Bool) → Bool} : ∃ (c : Circuit signature (k * n) k), c.Computes interpretation (directProduct f k) ∧ ↑(c.program.cost nonconstantCost) = massComplexity f k

Some circuit attains the minimum cost. This is an existence theorem, not an efficient algorithm for finding a minimum circuit.

theorem Cslib.Circuits.Boolean.MassProduction.massComplexity_le_complexity {n k : ℕ} {f : (Fin n → Bool) → Bool} : massComplexity f k ≤ ↑(complexity interpretation (directProduct f k))

Charging only nonconstant gates costs at most the minimum size, which counts every gate.

@[simp]

theorem Cslib.Circuits.Boolean.MassProduction.massComplexity_zero {n : ℕ} {f : (Fin n → Bool) → Bool} : massComplexity f 0 = 0

theorem Cslib.Circuits.Boolean.MassProduction.massComplexity_mono {n : ℕ} {f : (Fin n → Bool) → Bool} {small large : ℕ} (h : small ≤ large) : massComplexity f small ≤ massComplexity f large

Discarding copies cannot increase minimum cost, including discarding all copies.

theorem Cslib.Circuits.Boolean.MassProduction.massComplexity_le_replicate {n : ℕ} {f : (Fin n → Bool) → Bool} (k : ℕ) : massComplexity f k ≤ ↑k * ecomplexityFrom interpretation nonconstantCost (single f) id

Naive independent replication costs at most the number of copies times one-copy cost.

theorem Cslib.Circuits.Boolean.MassProduction.massComplexity_comp_wiring_le {n : ℕ} {f : (Fin n → Bool) → Bool} {p : ℕ} (select : Fin n → Fin p) (k : ℕ) : massComplexity (fun (x : Fin p → Bool) => f (x ∘ select)) k ≤ massComplexity f k

Rewiring every input block adds no cost.

def Cslib.Circuits.Boolean.MassProduction.rationalCopyBudget (numerator denominator inputs : ℕ) : ℕ

The copy budget at rational exponent numerator / denominator, rounding down.

theorem Cslib.Circuits.Boolean.MassProduction.rationalCopyBudget_mono_numerator {small large denominator inputs : ℕ} (h : small ≤ large) : rationalCopyBudget small denominator inputs ≤ rationalCopyBudget large denominator inputs

theorem Cslib.Circuits.Boolean.MassProduction.rationalCopyBudget_mono_inputs {numerator denominator small large : ℕ} (h : small ≤ large) : rationalCopyBudget numerator denominator small ≤ rationalCopyBudget numerator denominator large

def Cslib.Circuits.Boolean.MassProduction.MassProductionBound (numerator denominator constant inputs : ℕ) : Prop

The uniform bound at one input length, for every function and positive allowed copy count.

theorem Cslib.Circuits.Boolean.MassProduction.MassProductionBound.mono_numerator {small large denominator constant inputs : ℕ} (h : MassProductionBound large denominator constant inputs) (hle : small ≤ large) : MassProductionBound small denominator constant inputs

Decreasing the allowed numerator preserves a bound at one input length.

def Cslib.Circuits.Boolean.MassProduction.MassProducesAt (numerator denominator : ℕ) : Prop

Eventual mass production at a fixed rational exponent. The constant and cutoff may depend on the exponent, but are uniform in input length, function and number of copies.

def Cslib.Circuits.Boolean.MassProduction.MassProducesAtAllLengths (numerator denominator : ℕ) : Prop

Mass production at every positive input length, with one constant for the fixed exponent.

def Cslib.Circuits.Boolean.MassProduction.ExponentialMassProduction : Prop

Every fixed nonnegative rational exponent below one has an all-length bound.

theorem Cslib.Circuits.Boolean.MassProduction.MassProducesAtAllLengths.eventually {numerator denominator : ℕ} (h : MassProducesAtAllLengths numerator denominator) : MassProducesAt numerator denominator

An all-length bound holds eventually.

theorem Cslib.Circuits.Boolean.MassProduction.MassProducesAt.mono_numerator {small large denominator : ℕ} (h : MassProducesAt large denominator) (hle : small ≤ large) : MassProducesAt small denominator

Decreasing the allowed numerator preserves eventual mass production.

theorem Cslib.Circuits.Boolean.MassProduction.MassProducesAtAllLengths.mono_numerator {small large denominator : ℕ} (h : MassProducesAtAllLengths large denominator) (hle : small ≤ large) : MassProducesAtAllLengths small denominator

Decreasing the allowed numerator preserves all-length mass production.