Parameters approaching the coefficient 1 / (1 - gamma)

Choose a resource precision and a rational prefix fraction that leave half of the requested coefficient error for runtime overhead. Integer geometric slopes realize that fraction while retaining a strict direction-capacity and copy-exponent gap.

structure Algebraic.MassProduction.Nonuniform.CoefficientParameters (numerator denominator precision : ℕ) : Type

Fixed numerical parameters with enough coefficient slack for the final polynomial-overhead absorption.

• resourcePrecision : ℕ

  Precision used for both the code rate and shorter-function synthesis.

• upperNumerator : ℕ

  Auxiliary rational upper bound on the prefix fraction.

• upperDenominator : ℕ

  Denominator of that auxiliary rational upper bound.

• geometry : GeometricSlopes numerator denominator self.upperNumerator self.upperDenominator

  Integer field, copy, and input slopes inside the allowed interval.

• resourcePositive : 0 < self.resourcePrecision

  The resource precision is positive.

• leadingCoefficient : 2 * precision * (denominator - numerator) * self.geometry.inputSlope * (self.resourcePrecision + 2) * (self.resourcePrecision + 1) ≤ (2 * precision + 1) * denominator * (self.geometry.inputSlope - (self.geometry.dimension * self.geometry.blockWidth + 1)) * self.resourcePrecision ^ 2

  The leading resource cost uses at most half of the target error allowance.

theorem Algebraic.MassProduction.Nonuniform.existsCoefficientParameters {numerator denominator precision : ℕ} (proper : numerator < denominator) (precisionPositive : 0 < precision) : Nonempty (CoefficientParameters numerator denominator precision)

Every rational copy exponent below one and every positive target precision admit fixed parameters with the required leading-coefficient slack.