Finite two-block mass-production step

This module combines the one-copy resource bank with the absorbed overhead, instantiates the finite composition theorem, and proves the eventual mass-production bound on exact even widths.

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

Constant left after adding the recursive resource bank and the eventually negligible overhead.

Equations

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

theorem Algebraic.MassProduction.EqualBlock.twoBlock_canonicalCostBound_le (denominator blockWidth copies : ℕ) (denominatorPositive : 0 < denominator) (blockPositive : 0 < blockWidth) (overheadBound : 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; CompositionBound.overheadCostBound copies 1 blockWidth dimension width blockWidth schedulerDepth groupBitWidth orderWidth routingDepth routingDepth ≤ 2 ^ (blockWidth + blockWidth) / (blockWidth + blockWidth)) : FiniteParameters.canonicalCostBound copies 1 blockWidth (twoBlockDimension denominator) (CodeParameters.fieldWidth blockWidth (twoBlockDimension denominator) ⋯) blockWidth (twoBlockResourceBound blockWidth) ≤ twoBlockMassConstant denominator * (2 ^ (blockWidth + blockWidth) / (blockWidth + blockWidth))

Once the explicit overhead has entered the Shannon scale, the complete canonical finite cost has the same scale.

theorem Algebraic.MassProduction.EqualBlock.twoBlock_finiteComposition (numerator denominator blockWidth copies : ℕ) (denominatorPositive : 0 < denominator) (rateBelowHalf : 2 * numerator < denominator) (blockLarge : 16 ≤ blockWidth) (copiesBound : copies ≤ 2 ^ (numerator * (blockWidth + blockWidth) / denominator)) (function : ScalarFunction Bool (blockWidth + blockWidth)) : booleanMassComplexity function copies ≤ ↑(FiniteParameters.canonicalCostBound copies 1 blockWidth (twoBlockDimension denominator) (CodeParameters.fieldWidth blockWidth (twoBlockDimension denominator) ⋯) blockWidth (twoBlockResourceBound blockWidth))

Fully instantiated finite two-block composition. At this point the only remaining work for the base case is to bound the displayed explicit natural cost expression at the Shannon scale.

theorem Algebraic.MassProduction.EqualBlock.eventually_twoBlock_mass_bound (numerator denominator : ℕ) (denominatorPositive : 0 < denominator) (rateBelowHalf : 2 * numerator < denominator) : ∀ᶠ (blockWidth : ℕ) in Filter.atTop, ∀ (function : ScalarFunction Bool (blockWidth + blockWidth)) (copies : ℕ), 0 < copies → copies ≤ 2 ^ (numerator * (blockWidth + blockWidth) / denominator) → booleanMassComplexity function copies ≤ ↑(twoBlockMassConstant denominator * (2 ^ (blockWidth + blockWidth) / (blockWidth + blockWidth)))

The actual two-block mass-production bound, before padding arbitrary input lengths to the next even length.