Finite ledger for one equal-block induction step

This module places every width and sorting depth used by one induction step under a shared parameter bound and reduces the exact live-record volume to four explicit contributions consumed by the exponent analysis.

A shared bound for all finite bookkeeping parameters

def Algebraic.MassProduction.BlockInduction.stepSuffixWidth (level blockWidth : ℕ) : ℕ

Width of the recursive suffix containing level equal blocks.

Equations

• Algebraic.MassProduction.BlockInduction.stepSuffixWidth level blockWidth = level * blockWidth

def Algebraic.MassProduction.BlockInduction.stepInputWidth (level blockWidth : ℕ) : ℕ

Total width of the prefix block followed by the recursive suffix.

Equations

• Algebraic.MassProduction.BlockInduction.stepInputWidth level blockWidth = blockWidth + level * blockWidth

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

Linear upper bound for the least admissible extension-field width.

Equations

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

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

Common bound for every width and sorting depth in the finite ledger.

Equations

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

theorem Algebraic.MassProduction.BlockInduction.targetNumerator_lt_denominator (level numerator denominator : ℕ) (denominatorPositive : 0 < denominator) (rateBelowLevel : (level + 1) * numerator < level * denominator) : numerator < denominator

theorem Algebraic.MassProduction.BlockInduction.groupExponent_le_inputWidth (level denominator blockWidth : ℕ) (levelAtLeastTwo : 2 ≤ level) (denominatorPositive : 0 < denominator) : groupExponent level denominator blockWidth ≤ stepInputWidth level blockWidth

theorem Algebraic.MassProduction.BlockInduction.requestGroupSize_le_copies (copies groups : ℕ) (groupsPositive : 0 < groups) : GroupedScheduler.requestGroupSize copies groups ≤ copies

theorem Algebraic.MassProduction.BlockInduction.step_parameters_bounded (level numerator denominator blockWidth copies : ℕ) (levelAtLeastTwo : 2 ≤ level) (denominatorPositive : 0 < denominator) (rateBelowLevel : (level + 1) * numerator < level * denominator) (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 groupBitWidth := FiniteParameters.groupBitWidth groups; have orderWidth := FiniteParameters.orderWidth copies width; have routingDepth := FiniteParameters.routingDepth copies groups dimension width; have bound := stepParameterBound level denominator blockWidth; dimension ≤ bound ∧ width ≤ bound ∧ schedulerDepth ≤ bound ∧ blockWidth ≤ bound ∧ IncidenceRouting.incidenceKeyWidth groupBitWidth dimension width ≤ bound ∧ stepSuffixWidth level blockWidth ≤ bound ∧ orderWidth + 1 ≤ bound ∧ routingDepth ≤ bound

Every bit width and network depth in one induction-step ledger is bounded by one explicit expression linear in the total input width.

Exact live-record volume

theorem Algebraic.MassProduction.BlockInduction.step_overheadVolume_le (level denominator blockWidth copies : ℕ) (denominatorPositive : 0 < denominator) (copiesPositive : 0 < copies) : let dimension := stepDimension denominator; have dimensionPositive := ⋯; have width := CodeParameters.fieldWidth blockWidth dimension dimensionPositive; have groups := groupCount level denominator blockWidth; have groupSize := GroupedScheduler.requestGroupSize copies groups; OverheadBound.overheadVolume copies groups width (FiniteParameters.schedulerDepth copies groups width) (FiniteParameters.routingDepth copies groups dimension width) ≤ 2 * groups * groupSize * groupSize * 2 ^ width + groups * groupSize * 2 ^ width + 6 * copies * 2 ^ width + 4 * groups * 2 ^ (dimension * width)

The canonical live-record volume has precisely the four contributions needed by the exponent calculation: grouped scheduling, group-line work, incidences, and group-indexed resource slots.