Polynomial overhead absorption for block induction

This module combines the finite ledger with the strict live-volume exponent and proves that every non-resource cost in one equal-block induction step is eventually bounded by one Shannon-scale unit.

Absorbing the polynomial ledger

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

Slope relating ledger widths to the complete input width.

Equations

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

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

Constant coefficient of the degree-ten polynomial ledger envelope.

Equations

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

theorem Algebraic.MassProduction.BlockInduction.step_parameterBound_le (level denominator blockWidth : ℕ) : stepParameterBound level denominator blockWidth ≤ stepParameterSlope denominator * (stepInputWidth level blockWidth + 1)

theorem Algebraic.MassProduction.BlockInduction.step_coefficient_le (level denominator blockWidth : ℕ) : have parameterBound := stepParameterBound level denominator blockWidth; have inputWidth := stepInputWidth level blockWidth; OverheadBound.coefficientEnvelope parameterBound + 5 * parameterBound ≤ stepCoefficientConstant denominator * (inputWidth + 1) ^ 10

theorem Algebraic.MassProduction.BlockInduction.step_coefficient_le_monomial (level denominator blockWidth : ℕ) (blockPositive : 0 < blockWidth) : have parameterBound := stepParameterBound level denominator blockWidth; have inputWidth := stepInputWidth level blockWidth; OverheadBound.coefficientEnvelope parameterBound + 5 * parameterBound ≤ stepCoefficientConstant denominator * 2 ^ 10 * inputWidth ^ 10

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

Fixed coefficient of the polynomial-times-exponential overhead bound.

Equations

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

theorem Algebraic.MassProduction.BlockInduction.step_overhead_le_of_growth (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)) (growthBound : stepOverheadConstant denominator * stepInputWidth level blockWidth ^ 10 * 2 ^ stepCommonExponent level denominator blockWidth ≤ 2 ^ stepInputWidth level blockWidth / stepInputWidth level blockWidth) : 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 groupBitWidth := FiniteParameters.groupBitWidth groups; have orderWidth := FiniteParameters.orderWidth copies width; have routingDepth := FiniteParameters.routingDepth copies groups dimension width; CompositionBound.overheadCostBound copies groups blockWidth dimension width (stepSuffixWidth level blockWidth) schedulerDepth groupBitWidth orderWidth routingDepth routingDepth ≤ 2 ^ stepInputWidth level blockWidth / stepInputWidth level blockWidth

Pointwise composition of the exact ledger, the live-volume estimate, and the common polynomial coefficient estimate.

theorem Algebraic.MassProduction.BlockInduction.eventually_step_overhead_le (level numerator denominator : ℕ) (levelAtLeastTwo : 2 ≤ level) (denominatorPositive : 0 < denominator) (rateBelowLevel : (level + 1) * numerator < level * denominator) : ∀ᶠ (blockWidth : ℕ) in Filter.atTop, ∀ (copies : ℕ), 0 < copies → 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 groupBitWidth := FiniteParameters.groupBitWidth groups; have orderWidth := FiniteParameters.orderWidth copies width; have routingDepth := FiniteParameters.routingDepth copies groups dimension width; CompositionBound.overheadCostBound copies groups blockWidth dimension width (stepSuffixWidth level blockWidth) schedulerDepth groupBitWidth orderWidth routingDepth routingDepth ≤ 2 ^ stepInputWidth level blockWidth / stepInputWidth level blockWidth

All non-resource work is eventually at most one Shannon-scale unit, uniformly over every permitted batch.