Exponential live-volume bound for block induction

This module proves that all live-record terms in one equal-block induction step fit below a single exponential with a fixed strict margin from the full input width. Its public endpoint is step_overheadVolume_exponential_le.

Strict exponent margin for the complete overhead

def Algebraic.MassProduction.BlockInduction.stepMarginDenominator (level denominator : ℕ) : ℕ

Denominator of the strict common overhead exponent.

Equations

• Algebraic.MassProduction.BlockInduction.stepMarginDenominator level denominator = 24 * denominator * (level + 1)

def Algebraic.MassProduction.BlockInduction.stepFieldExponent (denominator blockWidth : ℕ) : ℕ

Floored exponent appearing in the extension-field cardinality bound.

Equations

• Algebraic.MassProduction.BlockInduction.stepFieldExponent denominator blockWidth = blockWidth / Algebraic.MassProduction.BlockInduction.stepDimension denominator

def Algebraic.MassProduction.BlockInduction.stepCommonExponent (level denominator blockWidth : ℕ) : ℕ

One strict subunit exponent dominating all non-resource volumes.

Equations

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

theorem Algebraic.MassProduction.BlockInduction.stepMarginDenominator_positive (level denominator : ℕ) (denominatorPositive : 0 < denominator) : 0 < stepMarginDenominator level denominator

theorem Algebraic.MassProduction.BlockInduction.exponent_le_stepCommonExponent (level denominator blockWidth exponent : ℕ) (denominatorPositive : 0 < denominator) (scaledMargin : exponent * (24 * denominator) + blockWidth ≤ 24 * denominator * (level + 1) * blockWidth) : exponent ≤ stepCommonExponent level denominator blockWidth

A scaled block-unit margin implies the common strict subunit exponent on the complete (level + 1)-block input.

theorem Algebraic.MassProduction.BlockInduction.step_volume_exponents_le (level numerator denominator blockWidth : ℕ) (levelAtLeastTwo : 2 ≤ level) (denominatorPositive : 0 < denominator) (rateBelowLevel : (level + 1) * numerator < level * denominator) : have groupExponent := groupExponent level denominator blockWidth; have loadExponent := groupLoadExponent denominator blockWidth; have fieldExponent := stepFieldExponent denominator blockWidth; have requestExponent := numerator * stepInputWidth level blockWidth / denominator; have commonExponent := stepCommonExponent level denominator blockWidth; groupExponent + loadExponent + loadExponent + fieldExponent ≤ commonExponent ∧ groupExponent + loadExponent + fieldExponent ≤ commonExponent ∧ requestExponent + fieldExponent ≤ commonExponent ∧ groupExponent + blockWidth ≤ commonExponent

All four live-volume exponents fit under one fixed exponent strictly below the total input width.

def Algebraic.MassProduction.BlockInduction.stepFieldConstant (denominator : ℕ) : ℕ

Fixed multiplicative loss in the field-cardinality estimate.

Equations

• Algebraic.MassProduction.BlockInduction.stepFieldConstant denominator = 2 ^ (4 * Algebraic.MassProduction.BlockInduction.stepDimension denominator + 3)

def Algebraic.MassProduction.BlockInduction.stepSlotConstant (denominator : ℕ) : ℕ

Fixed multiplicative loss in the affine resource-slot estimate.

Equations

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

def Algebraic.MassProduction.BlockInduction.stepVolumeConstant (denominator : ℕ) : ℕ

Common constant multiplying the strict live-volume exponential.

Equations

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

theorem Algebraic.MassProduction.BlockInduction.step_overheadVolume_exponential_le (level numerator denominator blockWidth copies : ℕ) (levelAtLeastTwo : 2 ≤ level) (denominatorPositive : 0 < denominator) (rateBelowLevel : (level + 1) * numerator < level * denominator) (blockLarge : 4 * denominator ≤ blockWidth) (copiesPositive : 0 < copies) (copiesBound : copies ≤ 2 ^ (numerator * stepInputWidth level blockWidth / denominator)) : let dimension := stepDimension denominator; have dimensionPositive := ⋯; have width := CodeParameters.fieldWidth blockWidth dimension dimensionPositive; have groups := groupCount level denominator blockWidth; have schedulerDepth := FiniteParameters.schedulerDepth copies groups width; have routingDepth := FiniteParameters.routingDepth copies groups dimension width; OverheadBound.overheadVolume copies groups width schedulerDepth routingDepth ≤ stepVolumeConstant denominator * 2 ^ stepCommonExponent level denominator blockWidth

The complete canonical live-record volume is a fixed constant times a strict subunit exponential.