Eventual validity and normalized cost of the chosen parameters

Fixed block-count cutoffs supply the code rate, packing precision, synthesis precision, and direction/copy margins. A single exponential-growth estimate absorbs the complete seventh-degree runtime overhead after normalization by the input length.

def Algebraic.MassProduction.Nonuniform.CoefficientParameters.resourceBound {numerator denominator precision : ℕ} (parameters : CoefficientParameters numerator denominator precision) (inputs : ℕ) : ℕ

Integral sharp bound used for every shorter resource function.

Equations

• parameters.resourceBound inputs = (parameters.resourcePrecision + 1) * 2 ^ parameters.geometry.suffixWidth inputs / (parameters.resourcePrecision * parameters.geometry.suffixWidth inputs)

def Algebraic.MassProduction.Nonuniform.CoefficientParameters.totalCost {numerator denominator precision : ℕ} (parameters : CoefficientParameters numerator denominator precision) (inputs : ℕ) : ℕ

Exact finite theorem bound at the selected input-length parameters.

Equations

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

structure Algebraic.MassProduction.Nonuniform.CoefficientParameters.Ready {numerator denominator precision : ℕ} (parameters : CoefficientParameters numerator denominator precision) (inputs : ℕ) : Prop

Numerical and resource-synthesis premises needed to apply the finite theorem and obtain the target coefficient at one input length.

• blocksLarge : 9 ≤ parameters.geometry.blocks inputs

  Absorbs the scheduler's fixed constant and ensures positive field width.

• copiesFit : numerator * inputs / denominator + 1 ≤ parameters.geometry.copyDepth inputs

  The scheduled batch covers the rational exponent rounded upward.

• resourcesBounded (function : ScalarFunction Bool (parameters.geometry.suffixWidth inputs)) : (LupanovSynthesis.lupanovCircuit (parameters.geometry.suffixWidth inputs) function).cost DeMorgan.standardCost ≤ parameters.resourceBound inputs

  Every actual shorter Lupanov circuit meets the selected integral bound.

• costBound : precision * (denominator - numerator) * inputs * parameters.totalCost inputs ≤ (precision + 1) * denominator * 2 ^ inputs

  The complete finite cost satisfies the target normalized coefficient.

theorem Algebraic.MassProduction.Nonuniform.CoefficientParameters.eventually_ready {numerator denominator precision : ℕ} (parameters : CoefficientParameters numerator denominator precision) : ∀ᶠ (inputs : ℕ) in Filter.atTop, parameters.Ready inputs

All chosen premises hold eventually, uniformly in the Boolean function and in the number of requested copies.