Two-block base-case parameters

This module fixes the recovery-code dimension for the equal-block base case, proves the scheduler-capacity inequality below rate one half, and bounds the one-copy resource bank at the full two-block Shannon scale.

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

A concrete recovery-code dimension for the two-block base case. The factor three leaves a strict direction-capacity margin at every rational rate strictly below one half.

Equations

• Algebraic.MassProduction.EqualBlock.twoBlockDimension denominator = 3 * denominator

theorem Algebraic.MassProduction.EqualBlock.twoBlockDimension_positive {denominator : ℕ} (denominatorPositive : 0 < denominator) : 0 < twoBlockDimension denominator

theorem Algebraic.MassProduction.EqualBlock.twoBlockDimension_atLeastTwo {denominator : ℕ} (denominatorPositive : 0 < denominator) : 2 ≤ twoBlockDimension denominator

theorem Algebraic.MassProduction.EqualBlock.twoBlock_loadExponent (numerator denominator prefixWidth width : ℕ) (denominatorPositive : 0 < denominator) (rateBelowHalf : 2 * numerator < denominator) (widthPositive : 0 < width) (packingRate : prefixWidth ≤ (twoBlockDimension denominator + 1) * width) : numerator * (prefixWidth + prefixWidth) / denominator + width < width * (twoBlockDimension denominator - 1)

Exact exponent inequality behind the two-block scheduler. It uses only the information-rate lower bound forced by successful prefix packing.

theorem Algebraic.MassProduction.EqualBlock.twoBlock_loadBound (numerator denominator prefixWidth copies : ℕ) (denominatorPositive : 0 < denominator) (rateBelowHalf : 2 * numerator < denominator) (copiesBound : copies ≤ 2 ^ (numerator * (prefixWidth + prefixWidth) / denominator)) : GroupedScheduler.requestGroupSize copies 1 * 2 ^ CodeParameters.fieldWidth prefixWidth (twoBlockDimension denominator) ⋯ < 2 ^ (CodeParameters.fieldWidth prefixWidth (twoBlockDimension denominator) ⋯ * (twoBlockDimension denominator - 1))

For one request group, every allowed two-block batch has enough projective directions for the least admissible field selected by CodeParameters.

def Algebraic.MassProduction.EqualBlock.twoBlockResourceBound (blockWidth : ℕ) : ℕ

The concrete Shannon bound supplied to every one-copy resource circuit in the two-block base case.

Equations

• Algebraic.MassProduction.EqualBlock.twoBlockResourceBound blockWidth = 27 * 2 ^ blockWidth / blockWidth

theorem Algebraic.MassProduction.EqualBlock.twoBlock_resourceTerm_le (denominator blockWidth : ℕ) (denominatorPositive : 0 < denominator) (blockPositive : 0 < blockWidth) : ResourceEvaluation.resourceBitCount (twoBlockDimension denominator) (CodeParameters.fieldWidth blockWidth (twoBlockDimension denominator) ⋯) * twoBlockResourceBound blockWidth ≤ 216 * CodeParameters.resourceConstant (twoBlockDimension denominator) * (2 ^ (blockWidth + blockWidth) / (blockWidth + blockWidth))

The recursive resource bank already lies at the sharp Shannon scale for the complete two-block input.