Finite ledger for the two-block base case

This module bounds every width and sorting depth in the canonical two-block construction by one shared parameter and reduces its exact live-record volume to three explicit contributions.

def Algebraic.MassProduction.EqualBlock.twoBlockWidthBound (denominator blockWidth : ℕ) : ℕ

Linear upper bound for the selected extension-field bit width in the two-block construction.

Equations

• Algebraic.MassProduction.EqualBlock.twoBlockWidthBound denominator blockWidth = blockWidth + 4 * Algebraic.MassProduction.EqualBlock.twoBlockDimension denominator + 3

def Algebraic.MassProduction.EqualBlock.twoBlockParameterBound (denominator blockWidth : ℕ) : ℕ

Shared linear bound for every bit width and sorting depth occurring in the canonical two-block ledger.

Equations

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

theorem Algebraic.MassProduction.EqualBlock.twoBlock_fieldWidth_le_widthBound (denominator blockWidth : ℕ) (denominatorPositive : 0 < denominator) : CodeParameters.fieldWidth blockWidth (twoBlockDimension denominator) ⋯ ≤ twoBlockWidthBound denominator blockWidth

theorem Algebraic.MassProduction.EqualBlock.twoBlock_parameters_bounded (numerator denominator blockWidth copies : ℕ) (denominatorPositive : 0 < denominator) (rateBelowHalf : 2 * numerator < denominator) (copiesBound : copies ≤ 2 ^ (numerator * (blockWidth + blockWidth) / denominator)) : let dimension := twoBlockDimension denominator; have dimensionPositive := ⋯; have width := CodeParameters.fieldWidth blockWidth dimension dimensionPositive; have schedulerDepth := FiniteParameters.schedulerDepth copies 1 width; have groupBitWidth := FiniteParameters.groupBitWidth 1; have orderWidth := FiniteParameters.orderWidth copies width; have routingDepth := FiniteParameters.routingDepth copies 1 dimension width; have bound := twoBlockParameterBound denominator blockWidth; dimension ≤ bound ∧ width ≤ bound ∧ schedulerDepth ≤ bound ∧ blockWidth ≤ bound ∧ IncidenceRouting.incidenceKeyWidth groupBitWidth dimension width ≤ bound ∧ blockWidth ≤ bound ∧ orderWidth + 1 ≤ bound ∧ routingDepth ≤ bound

All coefficient parameters in the canonical two-block ledger lie below twoBlockParameterBound.

theorem Algebraic.MassProduction.EqualBlock.twoBlock_overheadVolume_le (denominator blockWidth copies : ℕ) (denominatorPositive : 0 < denominator) (copiesPositive : 0 < copies) : let dimension := twoBlockDimension denominator; have dimensionPositive := ⋯; have width := CodeParameters.fieldWidth blockWidth dimension dimensionPositive; OverheadBound.overheadVolume copies 1 width (FiniteParameters.schedulerDepth copies 1 width) (FiniteParameters.routingDepth copies 1 dimension width) ≤ 2 * copies * copies * 2 ^ width + 7 * copies * 2 ^ width + 4 * 2 ^ (dimension * width)

The exact canonical record volume in the two-block case has the three expected contributions: quadratic scheduling, incidences, and resource slots.