Exponential live-volume bound for the two-block base case

This module places the canonical two-block record volume below one binary exponential with a fixed strict margin from the complete input width. Its endpoint is twoBlock_overheadVolume_exponential_le.

def Algebraic.MassProduction.EqualBlock.twoBlockMarginDenominator (denominator : ℕ) : ℕ

Denominator used for the common strict subunit exponent in the two-block overhead bound.

Equations

• Algebraic.MassProduction.EqualBlock.twoBlockMarginDenominator denominator = 6 * denominator

def Algebraic.MassProduction.EqualBlock.twoBlockFieldConstant (denominator : ℕ) : ℕ

Fixed multiplicative loss in the field-cardinality upper bound.

Equations

• Algebraic.MassProduction.EqualBlock.twoBlockFieldConstant denominator = 2 ^ (4 * Algebraic.MassProduction.EqualBlock.twoBlockDimension denominator + 3)

def Algebraic.MassProduction.EqualBlock.twoBlockSlotConstant (denominator : ℕ) : ℕ

Fixed multiplicative loss after raising the field cardinality to the code dimension.

Equations

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

def Algebraic.MassProduction.EqualBlock.twoBlockVolumeConstant (denominator : ℕ) : ℕ

Fixed coefficient for the complete canonical record-volume bound.

Equations

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

def Algebraic.MassProduction.EqualBlock.twoBlockParameterSlope (denominator : ℕ) : ℕ

Slope relating every concrete ledger width to the full two-block input length.

Equations

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

def Algebraic.MassProduction.EqualBlock.twoBlockCoefficientConstant (denominator : ℕ) : ℕ

Constant coefficient of the degree-ten common ledger envelope.

Equations

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

theorem Algebraic.MassProduction.EqualBlock.twoBlock_parameterBound_le (denominator blockWidth : ℕ) : twoBlockParameterBound denominator blockWidth ≤ twoBlockParameterSlope denominator * (blockWidth + blockWidth + 1)

theorem Algebraic.MassProduction.EqualBlock.twoBlock_coefficient_le (denominator blockWidth : ℕ) : have parameterBound := twoBlockParameterBound denominator blockWidth; have inputWidth := blockWidth + blockWidth; OverheadBound.coefficientEnvelope parameterBound + 5 * parameterBound ≤ twoBlockCoefficientConstant denominator * (inputWidth + 1) ^ 10

The common coefficient in the two-block ledger is a fixed constant times a degree-ten polynomial in the complete input length.

theorem Algebraic.MassProduction.EqualBlock.twoBlock_coefficient_le_monomial (denominator blockWidth : ℕ) (blockPositive : 0 < blockWidth) : have parameterBound := twoBlockParameterBound denominator blockWidth; have inputWidth := blockWidth + blockWidth; OverheadBound.coefficientEnvelope parameterBound + 5 * parameterBound ≤ twoBlockCoefficientConstant denominator * 2 ^ 10 * inputWidth ^ 10

theorem Algebraic.MassProduction.EqualBlock.twoBlock_overheadVolume_exponential_le (numerator denominator blockWidth copies : ℕ) (denominatorPositive : 0 < denominator) (rateBelowHalf : 2 * numerator < denominator) (copiesPositive : 0 < copies) (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 routingDepth := FiniteParameters.routingDepth copies 1 dimension width; have inputWidth := blockWidth + blockWidth; have marginDenominator := twoBlockMarginDenominator denominator; OverheadBound.overheadVolume copies 1 width schedulerDepth routingDepth ≤ twoBlockVolumeConstant denominator * 2 ^ ((marginDenominator - 1) * inputWidth / marginDenominator)

The common overhead exponent is strictly below one and dominates the quadratic scheduler, incidence, and resource-slot exponents.