Polynomial overhead absorption for the two-block base case #
This module combines the two-block finite ledger with its strict exponential volume bound and proves that the complete non-resource overhead is eventually at most one Shannon-scale unit.
Fixed coefficient multiplying the polynomial-times-subunit-exponential upper bound for every non-resource gate.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
Algebraic.MassProduction.EqualBlock.twoBlock_overhead_le_of_growth
(numerator denominator blockWidth copies : ℕ)
(denominatorPositive : 0 < denominator)
(rateBelowHalf : 2 * numerator < denominator)
(blockPositive : 0 < blockWidth)
(copiesPositive : 0 < copies)
(copiesBound : copies ≤ 2 ^ (numerator * (blockWidth + blockWidth) / denominator))
(growthBound :
twoBlockOverheadConstant denominator * (blockWidth + blockWidth) ^ 10 * 2 ^ ((twoBlockMarginDenominator denominator - 1) * (blockWidth + blockWidth) / twoBlockMarginDenominator denominator) ≤ 2 ^ (blockWidth + blockWidth) / (blockWidth + blockWidth))
:
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)
Pointwise composition of the exact ledger, record-volume estimate, and polynomial coefficient estimate.
theorem
Algebraic.MassProduction.EqualBlock.eventually_twoBlock_overhead_le
(numerator denominator : ℕ)
(denominatorPositive : 0 < denominator)
(rateBelowHalf : 2 * numerator < denominator)
:
∀ᶠ (blockWidth : ℕ) in Filter.atTop, ∀ (copies : ℕ),
0 < copies →
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;
CompositionBound.overheadCostBound copies 1 blockWidth dimension width blockWidth schedulerDepth groupBitWidth
orderWidth routingDepth routingDepth ≤ 2 ^ (blockWidth + blockWidth) / (blockWidth + blockWidth)
The polynomial ledger is eventually absorbed by its strict binary exponent margin, uniformly over every permitted batch at the fixed rate.