The sharp nonuniform exponential-range coefficient

For every rational copy exponent gamma = numerator / denominator < 1, the worst-case normalized cost is eventually at most (1 + 1/precision) / (1 - gamma) for every positive integer precision. The theorem constructs the complete runtime circuit, including its code, placement, lookup, scheduler, resource bank, recovery, and output order.

The statement is denominator-free in ENat and quantifies uniformly over all Boolean functions and all positive copy counts in the allowed range.

def Algebraic.MassProduction.Nonuniform.SharpMassProducesAt (numerator denominator : ℕ) : Prop

Precise integer formulation of the coefficient 1/(1-gamma) + o(1) at one rational copy exponent.

Equations

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

def Algebraic.MassProduction.Nonuniform.SharpExponentialMassProduction : Prop

Sharp nonuniform mass production at every fixed rational exponent below one.

Equations

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

theorem Algebraic.MassProduction.Nonuniform.CoefficientParameters.Ready.booleanMassComplexity_le {numerator denominator precision inputs : ℕ} {parameters : CoefficientParameters numerator denominator precision} (ready : parameters.Ready inputs) (function : ScalarFunction Bool inputs) (copies : ℕ) (copiesPositive : 0 < copies) (copiesBound : copies ≤ 2 ^ (numerator * inputs / denominator + 1)) : booleanMassComplexity function copies ≤ ↑(parameters.totalCost inputs)

Ready parameters yield the complete finite bound for an arbitrary Boolean function on the original input length and every allowed copy count.

theorem Algebraic.MassProduction.Nonuniform.sharpMassProducesAt {numerator denominator : ℕ} (proper : numerator < denominator) : SharpMassProducesAt numerator denominator

The complete nonuniform construction achieves the coefficient 1/(1-gamma) + o(1) for every rational exponent gamma < 1.

theorem Algebraic.MassProduction.Nonuniform.sharpExponentialMassProduction : SharpExponentialMassProduction

Both the exponential copy range and the improved leading coefficient are proved uniformly over all input functions.