Denominator-free leading-coefficient accounting #
Multiply the code-storage and shorter-function precision inequalities, transfer the suffix normalization to the original input length, and add the reserved runtime-overhead allowance. All arithmetic takes place in the natural numbers; no floor approximation or division loss is introduced.
theorem
Algebraic.MassProduction.Nonuniform.CoefficientParameters.cost_le_coefficient
{numerator denominator precision : ℕ}
(parameters : CoefficientParameters numerator denominator precision)
{prefixWidth suffixWidth inputs resources resourceCost overhead : ℕ}
(inputSplit : prefixWidth + suffixWidth = inputs)
(suffixFraction : parameters.geometry.suffixSlope * inputs ≤ parameters.geometry.inputSlope * suffixWidth)
(storage : parameters.resourcePrecision * resources ≤ (parameters.resourcePrecision + 2) * 2 ^ prefixWidth)
(synthesis :
parameters.resourcePrecision * resourceCost * suffixWidth ≤ (parameters.resourcePrecision + 1) * 2 ^ suffixWidth)
(runtime : 2 * precision * (denominator - numerator) * inputs * overhead ≤ denominator * 2 ^ inputs)
:
Exact integer rate, synthesis, split, and overhead bounds imply the target normalized coefficient for the complete finite circuit cost.