Padding circuit mass-production bounds

Adding unused inputs preserves the mass complexity of a function with a nonempty input block. A fixed amount of padding changes the integer Shannon scale by only a constant factor. Consequently an eventual rational-rate bound extends to every positive input length.

Main results

• Cslib.Circuits.Boolean.MassProduction.massComplexity_comp_castLE: padding preserves cost.
• Cslib.Circuits.Boolean.MassProduction.shannonScale_le_of_le_add: the floor-stable scale bound.
• Cslib.Circuits.Boolean.MassProduction.MassProducesAt.allLengths: an eventual bound holds at every positive input length, with one larger constant.

References

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

theorem Cslib.Circuits.Boolean.MassProduction.massComplexity_comp_castLE {n p : ℕ} (hn : 0 < n) (hle : n ≤ p) (f : (Fin n → Bool) → Bool) (k : ℕ) : massComplexity (fun (x : Fin p → Bool) => f (x ∘ Fin.castLE hle)) k = massComplexity f k

Padding a nonempty block by ignored tail coordinates preserves minimum weighted cost.

theorem Cslib.Circuits.Boolean.MassProduction.shannonScale_le_of_le_add {n p padding : ℕ} (hn : 0 < n) (hle : n ≤ p) (hp : p ≤ n + padding) : 2 ^ p / p ≤ 2 * 2 ^ padding * (2 ^ n / n)

Adding at most padding inputs changes the integer Shannon scale by a fixed factor.

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

Padding by the fixed cutoff turns an eventual bound into an all-positive-length bound.