Statements of fine mass production

For a rational copy exponent γ = num / den < 1, fine mass production bounds the cost of every allowed batch by (1 + 1 / P) / (1 - γ) · 2 ^ n / n for every positive precision P, eventually in n. The core form FineMassProducesThrough allows 2 ^ (⌊γ n⌋ + 1) copies, including zero copies; FineMassProducesAt is the source's statement over the floor budget rationalCopyBudget and positive copy counts. The real-rate statement RealFineMassProduction quantifies over real 0 ≤ γ < 1 and additive errors ε > 0, with copy counts at most 2 ^ (γ n).

Fine refers to the explicit leading coefficient 1 / (1 - γ), as opposed to the unspecified constant of MassProducesAt (4 den via FineMassProducesThrough.massProducesAt); it does not claim optimality. One copy of most functions already needs (1 - o(1)) 2 ^ n / n nonconstant gates, by the counting argument of [Sha49] for gate circuits Jukna, Theorem 1.14 (cslib's Cslib.Circuits.Boolean.Shannon.lt_complexity gives one such function, counting constant gates, of which at most two are needed), so the coefficient is optimal at γ = 0; no matching lower bound is claimed for γ > 0.

The core form implies the other two (FineMassProducesThrough.fineMassProducesAt, realFineMassProduction_of_fine) and, at precision one, the exponential-range theorem with a constant coefficient at every positive input length (exponentialMassProduction_of_fine).

All statements bound massComplexity, which charges NOT, AND and OR once and constants never. They are bounds on circuit cost, not on the running time of any circuit constructor.

Main definitions

• Cslib.Circuits.Boolean.MassProduction.FineMassProducesThrough: the core fine bound.
• Cslib.Circuits.Boolean.MassProduction.FineMassProducesAt: the source's rational statement.
• Cslib.Circuits.Boolean.MassProduction.RealFineMassProduction: the real-rate statement.

Main results

• Cslib.Circuits.Boolean.MassProduction.FineMassProducesThrough.massProducesAt: the coefficient 4 den at one rational exponent.
• Cslib.Circuits.Boolean.MassProduction.exponentialMassProduction_of_fine, Cslib.Circuits.Boolean.MassProduction.realFineMassProduction_of_fine: the corollaries.

References

• Adapted from MassProduction/Nonuniform/{SharpTheorem,RealParameters,RealTheorem}.lean in S. Schlesinger, Boolean circuit mass production formalization.
• C. E. Shannon, The Synthesis of Two-Terminal Switching Circuits
• Stasys Jukna, Boolean Function Complexity: Advances and Frontiers, Theorem 1.14

def Cslib.Circuits.Boolean.MassProduction.FineMassProducesThrough (num den : ℕ) : Prop

The core fine bound at rational exponent num / den: for every precision P, eventually every function on n inputs has k ≤ 2 ^ (⌊num n / den⌋ + 1) copies with P (den - num) n · cost ≤ (P + 1) den 2 ^ n. For P > 0 this is the coefficient (1 + 1 / P) den / (den - num); P = 0 holds trivially.

def Cslib.Circuits.Boolean.MassProduction.FineMassProducesAt (num den : ℕ) : Prop

The source's statement at rational exponent num / den, over the floor budget and positive copy counts.

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

The source's real-rate statement: for every real 0 ≤ γ < 1 and every ε > 0, eventually every positive copy count at most 2 ^ (γ n) has a finite cost bound below (1 / (1 - γ) + ε) 2 ^ n / n.

theorem Cslib.Circuits.Boolean.MassProduction.rationalCopyBudget_le_two_pow {num den : ℕ} (n : ℕ) : rationalCopyBudget num den n ≤ 2 ^ (num * n / den + 1)

The floor budget is within the core budget.

theorem Cslib.Circuits.Boolean.MassProduction.FineMassProducesThrough.fineMassProducesAt {num den : ℕ} (h : FineMassProducesThrough num den) : FineMassProducesAt num den

theorem Cslib.Circuits.Boolean.MassProduction.FineMassProducesThrough.massProducesAt {num den : ℕ} (hnd : num < den) (h : FineMassProducesThrough num den) : MassProducesAt num den

At precision one the core bound gives the constant 4 den: eventually every allowed batch costs at most 4 den (2 ^ n / n).

theorem Cslib.Circuits.Boolean.MassProduction.exponentialMassProduction_of_fine (h : ∀ (num den : ℕ), num < den → FineMassProducesThrough num den) : ExponentialMassProduction

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

theorem Cslib.Circuits.Boolean.MassProduction.exists_rat_coefficient {γ ε : ℝ} (hγ : 0 ≤ γ) (hγ1 : γ < 1) (hε : 0 < ε) : ∃ (num : ℕ) (den : ℕ) (P : ℕ), num < den ∧ 0 < P ∧ γ < ↑num / ↑den ∧ (↑P + 1) * ↑den ≤ (1 / (1 - γ) + ε) * ↑P * ↑(den - num)

Real rates and additive errors admit a rational rate above γ and an integer precision whose coefficient (1 + 1 / P) den / (den - num) is at most 1 / (1 - γ) + ε.

theorem Cslib.Circuits.Boolean.MassProduction.le_two_pow_of_real {num den : ℕ} {γ : ℝ} {n k : ℕ} (hden : 0 < den) (hγ : γ ≤ ↑num / ↑den) (hk : ↑k ≤ 2 ^ (γ * ↑n)) : k ≤ 2 ^ (num * n / den + 1)

A real copy budget 2 ^ (γ n) below a rational exponent num / den is within the core budget 2 ^ (⌊num n / den⌋ + 1).

theorem Cslib.Circuits.Boolean.MassProduction.realFineMassProduction_of_fine (h : ∀ (num den : ℕ), num < den → FineMassProducesThrough num den) : RealFineMassProduction

Real-rate fine mass production from the core fine bound at every rational exponent.