Integer slopes inside a prescribed rational interval

Choose a fixed field block width and dimension, then reserve a strict gap between the allowed copy exponent and projective-direction capacity. The prefix fraction can still lie in any prescribed interval above that copy exponent. This is an exact integer construction, without limiting notation.

structure Algebraic.MassProduction.Nonuniform.GeometricSlopes (numerator denominator upperNumerator upperDenominator : ℕ) : Type

Numerical slopes supporting a geometric scheduler and a prescribed upper bound on the fraction of input bits used as source prefixes.

• dimension : ℕ

  Affine-space dimension, fixed independently of the input length.

• blockWidth : ℕ

  Bits per field block on the selected field-size subsequence.

• copySlope : ℕ

  Scheduled batch exponent per complete field block.

• inputSlope : ℕ

  Input bits per complete field block.

• blockPositive : 0 < self.blockWidth

  Every field block has positive width.

• dimensionPositive : 0 < self.dimension

  The affine space has positive dimension.

• dimensionFits : self.dimension ≤ 2 ^ self.blockWidth

  The common-zero-block code admits the selected dimension.

• directionSlack : self.copySlope + self.blockWidth + 1 ≤ self.blockWidth * (self.dimension - 1)

  Strict exponential room absorbs the scheduler's fixed packing constant.

• splitPositive : self.dimension * self.blockWidth + 1 < self.inputSlope

  The prefix leaves a positive suffix slope.

• copyRate : numerator * self.inputSlope < denominator * self.copySlope

  The scheduled exponent strictly exceeds the requested exponent.

• prefixRate : upperDenominator * (self.dimension * self.blockWidth + 1) < upperNumerator * self.inputSlope

  The prefix fraction is below the chosen coefficient threshold.

theorem Algebraic.MassProduction.Nonuniform.existsGeometricSlopes {numerator denominator upperNumerator upperDenominator : ℕ} (proper : numerator < denominator) (upperPositive : 0 < upperNumerator) (upperProper : upperNumerator < upperDenominator) (between : numerator * upperDenominator < denominator * upperNumerator) : Nonempty (GeometricSlopes numerator denominator upperNumerator upperDenominator)

Every nonempty rational interval above the copy exponent contains the prefix fraction of a suitable geometric parameter choice.