Replicated Shannon synthesis

Independently replicate the finite Shannon construction to bound the mass complexity of any finite batch. The bound grows linearly with the number of copies; later mass-production constructions improve this dependence by sharing work between copies.

Main results

• Cslib.Circuits.Boolean.MassProduction.massComplexity_le_shannon: the finite replication bound.

References

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

theorem Cslib.Circuits.Boolean.MassProduction.massComplexity_le_shannon {n : ℕ} (hn : 16 ≤ n) (f : BooleanFunction n) (k : ℕ) : massComplexity f k ≤ ↑(k * (27 * 2 ^ n / n))

Independent Shannon synthesis bounds every finite batch, including zero copies. The natural division occurs inside the per-copy budget, after multiplication by 27.