The manuscript's sharp theorem for real copy rates

For every real 0 <= gamma < 1 and every positive additive error, one cutoff works for all input functions and all positive integer copy counts at most 2^(gamma*n). The conclusion supplies a finite natural cost bound, so no conversion of infinite circuit complexity to a real number is used.

def Algebraic.MassProduction.Nonuniform.RealSharpMassProduction : Prop

The sharp leading coefficient with the manuscript's real-rate and additive-error quantifiers, witnessed by an actual finite cost bound.

Equations

• One or more equations did not get rendered due to their size.

theorem Algebraic.MassProduction.Nonuniform.realSharpMassProduction : RealSharpMassProduction

Both the improved coefficient and the full real exponential copy range hold for complete De Morgan circuits on the original disjoint input blocks.