Parameters at every input length

Use floor(inputs/inputSlope) field blocks and put the remainder into the suffix. The input length is exact, while the suffix fraction never falls below its fixed rational slope. Fixed lower bounds on the block count discharge the copy-exponent and direction-capacity margins.

def Algebraic.MassProduction.Nonuniform.GeometricSlopes.prefixSlope {numerator denominator upperNumerator upperDenominator : ℕ} (parameters : GeometricSlopes numerator denominator upperNumerator upperDenominator) : ℕ

Prefix bits per field block, with one extra block bit for rounding slack.

Equations

• parameters.prefixSlope = parameters.dimension * parameters.blockWidth + 1

def Algebraic.MassProduction.Nonuniform.GeometricSlopes.blocks {numerator denominator upperNumerator upperDenominator : ℕ} (parameters : GeometricSlopes numerator denominator upperNumerator upperDenominator) (inputs : ℕ) : ℕ

Complete field blocks at the current input length.

Equations

• parameters.blocks inputs = inputs / parameters.inputSlope

def Algebraic.MassProduction.Nonuniform.GeometricSlopes.prefixWidth {numerator denominator upperNumerator upperDenominator : ℕ} (parameters : GeometricSlopes numerator denominator upperNumerator upperDenominator) (inputs : ℕ) : ℕ

Source-table prefix width.

Equations

• parameters.prefixWidth inputs = parameters.prefixSlope * parameters.blocks inputs

def Algebraic.MassProduction.Nonuniform.GeometricSlopes.suffixWidth {numerator denominator upperNumerator upperDenominator : ℕ} (parameters : GeometricSlopes numerator denominator upperNumerator upperDenominator) (inputs : ℕ) : ℕ

Exact remaining input bits form the shorter function's suffix.

Equations

• parameters.suffixWidth inputs = inputs - parameters.prefixWidth inputs

def Algebraic.MassProduction.Nonuniform.GeometricSlopes.fieldWidth {numerator denominator upperNumerator upperDenominator : ℕ} (parameters : GeometricSlopes numerator denominator upperNumerator upperDenominator) (inputs : ℕ) : ℕ

Binary-extension symbol width on the required block subsequence.

Equations

• parameters.fieldWidth inputs = parameters.blockWidth * parameters.blocks inputs

def Algebraic.MassProduction.Nonuniform.GeometricSlopes.copyDepth {numerator denominator upperNumerator upperDenominator : ℕ} (parameters : GeometricSlopes numerator denominator upperNumerator upperDenominator) (inputs : ℕ) : ℕ

Power-of-two scheduler batch depth.

Equations

• parameters.copyDepth inputs = parameters.copySlope * parameters.blocks inputs

def Algebraic.MassProduction.Nonuniform.GeometricSlopes.suffixSlope {numerator denominator upperNumerator upperDenominator : ℕ} (parameters : GeometricSlopes numerator denominator upperNumerator upperDenominator) : ℕ

Positive slope of the shorter suffix.

Equations

• parameters.suffixSlope = parameters.inputSlope - parameters.prefixSlope

theorem Algebraic.MassProduction.Nonuniform.GeometricSlopes.inputSlope_positive {numerator denominator upperNumerator upperDenominator : ℕ} (parameters : GeometricSlopes numerator denominator upperNumerator upperDenominator) : 0 < parameters.inputSlope

The block divisor is positive.

theorem Algebraic.MassProduction.Nonuniform.GeometricSlopes.suffixSlope_positive {numerator denominator upperNumerator upperDenominator : ℕ} (parameters : GeometricSlopes numerator denominator upperNumerator upperDenominator) : 0 < parameters.suffixSlope

At least one suffix bit is retained per full block.

theorem Algebraic.MassProduction.Nonuniform.GeometricSlopes.prefixWidth_le {numerator denominator upperNumerator upperDenominator : ℕ} (parameters : GeometricSlopes numerator denominator upperNumerator upperDenominator) (inputs : ℕ) : parameters.prefixWidth inputs ≤ inputs

The source prefix fits at every input length.

theorem Algebraic.MassProduction.Nonuniform.GeometricSlopes.prefix_add_suffix {numerator denominator upperNumerator upperDenominator : ℕ} (parameters : GeometricSlopes numerator denominator upperNumerator upperDenominator) (inputs : ℕ) : parameters.prefixWidth inputs + parameters.suffixWidth inputs = inputs

Prefix and suffix exactly partition the original input length.

theorem Algebraic.MassProduction.Nonuniform.GeometricSlopes.incidenceSlope_le {numerator denominator upperNumerator upperDenominator : ℕ} (parameters : GeometricSlopes numerator denominator upperNumerator upperDenominator) : parameters.copySlope + parameters.blockWidth ≤ parameters.prefixSlope

The slope gap bounds the incidence exponent by the prefix exponent.

theorem Algebraic.MassProduction.Nonuniform.GeometricSlopes.pointBudget {numerator denominator upperNumerator upperDenominator : ℕ} (parameters : GeometricSlopes numerator denominator upperNumerator upperDenominator) (inputs : ℕ) : Sorting.networkRecords (parameters.copyDepth inputs) * 2 ^ parameters.fieldWidth inputs ≤ 2 ^ parameters.prefixWidth inputs

All generated request/scalar pairs fit in the source-table scale.

theorem Algebraic.MassProduction.Nonuniform.GeometricSlopes.fieldWidth_le {numerator denominator upperNumerator upperDenominator : ℕ} (parameters : GeometricSlopes numerator denominator upperNumerator upperDenominator) (inputs : ℕ) : parameters.fieldWidth inputs ≤ inputs

The field bit width is no larger than the input length.

theorem Algebraic.MassProduction.Nonuniform.GeometricSlopes.copyDepth_le {numerator denominator upperNumerator upperDenominator : ℕ} (parameters : GeometricSlopes numerator denominator upperNumerator upperDenominator) (inputs : ℕ) : parameters.copyDepth inputs ≤ inputs

The scheduler depth is no larger than the input length.

theorem Algebraic.MassProduction.Nonuniform.GeometricSlopes.suffixWidth_lower {numerator denominator upperNumerator upperDenominator : ℕ} (parameters : GeometricSlopes numerator denominator upperNumerator upperDenominator) (inputs : ℕ) : parameters.suffixSlope * parameters.blocks inputs ≤ parameters.suffixWidth inputs

Each full block contributes the prescribed number of suffix bits.

theorem Algebraic.MassProduction.Nonuniform.GeometricSlopes.blocks_le_suffixWidth {numerator denominator upperNumerator upperDenominator : ℕ} (parameters : GeometricSlopes numerator denominator upperNumerator upperDenominator) (inputs : ℕ) : parameters.blocks inputs ≤ parameters.suffixWidth inputs

The block count itself is a lower bound on the suffix length.

theorem Algebraic.MassProduction.Nonuniform.GeometricSlopes.suffixFraction {numerator denominator upperNumerator upperDenominator : ℕ} (parameters : GeometricSlopes numerator denominator upperNumerator upperDenominator) (inputs : ℕ) : parameters.suffixSlope * inputs ≤ parameters.inputSlope * parameters.suffixWidth inputs

Putting the incomplete block into the suffix preserves the desired suffix/input fraction without any rounding loss in the leading coefficient.

theorem Algebraic.MassProduction.Nonuniform.GeometricSlopes.copyExponent_le {numerator denominator upperNumerator upperDenominator : ℕ} (parameters : GeometricSlopes numerator denominator upperNumerator upperDenominator) (inputs : ℕ) (blocksLarge : numerator * parameters.inputSlope ≤ parameters.blocks inputs) : numerator * inputs / denominator ≤ parameters.copyDepth inputs

A fixed block-count cutoff makes the scheduler's batch cover every copy count allowed by the target rational exponent.

theorem Algebraic.MassProduction.Nonuniform.GeometricSlopes.copyExponent_succ_le {numerator denominator upperNumerator upperDenominator : ℕ} (parameters : GeometricSlopes numerator denominator upperNumerator upperDenominator) (inputs : ℕ) (blocksLarge : numerator * parameters.inputSlope + 1 ≤ parameters.blocks inputs) : numerator * inputs / denominator + 1 ≤ parameters.copyDepth inputs

One further block of slack also covers rounding the rational exponent upward.

theorem Algebraic.MassProduction.Nonuniform.GeometricSlopes.directionBudget {numerator denominator upperNumerator upperDenominator : ℕ} (parameters : GeometricSlopes numerator denominator upperNumerator upperDenominator) (inputs : ℕ) (blocksLarge : 9 ≤ parameters.blocks inputs) : 512 * Sorting.networkRecords (parameters.copyDepth inputs) * Nat.card (BinaryExtension (parameters.fieldWidth inputs)) ≤ Nat.card (Projectivization (BinaryExtension (parameters.fieldWidth inputs)) (Fin parameters.dimension → BinaryExtension (parameters.fieldWidth inputs)))

Nine complete field blocks absorb the fixed scheduler constant 512.