Finite equal-block induction step

This module bounds the recursive resource bank, instantiates the finite composition theorem, and proves the eventual mass-production estimate on input widths that are exact equal-block multiples.

Recursive resource bank

def Algebraic.MassProduction.BlockInduction.stepResourceBound (recursiveConstant level blockWidth : ℕ) : ℕ

Previous-level Shannon-scale bound supplied to every resource function.

Equations

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

def Algebraic.MassProduction.BlockInduction.stepResourceConstant (denominator recursiveConstant : ℕ) : ℕ

Full-input coefficient contributed by the recursive resource bank.

Equations

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

theorem Algebraic.MassProduction.BlockInduction.step_resourceTerm_le (level denominator blockWidth recursiveConstant : ℕ) (levelAtLeastTwo : 2 ≤ level) (denominatorPositive : 0 < denominator) (blockPositive : 0 < blockWidth) : ResourceEvaluation.resourceBitCount (stepDimension denominator) (CodeParameters.fieldWidth blockWidth (stepDimension denominator) ⋯) * stepResourceBound recursiveConstant level blockWidth ≤ stepResourceConstant denominator recursiveConstant * (2 ^ stepInputWidth level blockWidth / stepInputWidth level blockWidth)

Multiplying the previous level's Shannon-scale resource complexity by the number of encoded resource bits remains at the full-input Shannon scale.

The finite and eventual induction steps

theorem Algebraic.MassProduction.BlockInduction.step_finiteComposition (level numerator denominator blockWidth copies recursiveConstant : ℕ) (levelAtLeastTwo : 2 ≤ level) (denominatorPositive : 0 < denominator) (rateBelowLevel : (level + 1) * numerator < level * denominator) (blockLarge : 4 * denominator ≤ blockWidth) (suffixLarge : 16 ≤ stepSuffixWidth level blockWidth) (copiesBound : copies ≤ 2 ^ (numerator * stepInputWidth level blockWidth / denominator)) (function : ScalarFunction Bool (stepInputWidth level blockWidth)) (resourceComplexity : let dimension := stepDimension denominator; have dimensionPositive := ⋯; let width := CodeParameters.fieldWidth blockWidth dimension dimensionPositive; have split := InputSplit.splitFunction function; ∀ (member : Fin (ResourceEvaluation.resourceBitCount dimension width)), booleanMassComplexity (CompositionBound.canonicalResourceFunction ⋯ ⋯ split member) (groupCount level denominator blockWidth) ≤ ↑(stepResourceBound recursiveConstant level blockWidth)) : booleanMassComplexity function copies ≤ ↑(FiniteParameters.canonicalCostBound copies (groupCount level denominator blockWidth) blockWidth (stepDimension denominator) (CodeParameters.fieldWidth blockWidth (stepDimension denominator) ⋯) (stepSuffixWidth level blockWidth) (stepResourceBound recursiveConstant level blockWidth))

Fully instantiated finite composition for one equal-block induction step, assuming a uniform recursive bound for each induced suffix function.

def Algebraic.MassProduction.BlockInduction.stepMassConstant (denominator recursiveConstant : ℕ) : ℕ

Sum of the recursive resource coefficient and one overhead unit.

Equations

• Algebraic.MassProduction.BlockInduction.stepMassConstant denominator recursiveConstant = Algebraic.MassProduction.BlockInduction.stepResourceConstant denominator recursiveConstant + 1

theorem Algebraic.MassProduction.BlockInduction.step_canonicalCostBound_le (level denominator blockWidth copies recursiveConstant : ℕ) (levelAtLeastTwo : 2 ≤ level) (denominatorPositive : 0 < denominator) (blockPositive : 0 < blockWidth) (overheadBound : let dimension := stepDimension denominator; have dimensionPositive := ⋯; have width := CodeParameters.fieldWidth blockWidth dimension dimensionPositive; have groups := groupCount level denominator blockWidth; have schedulerDepth := FiniteParameters.schedulerDepth copies groups width; have groupBitWidth := FiniteParameters.groupBitWidth groups; have orderWidth := FiniteParameters.orderWidth copies width; have routingDepth := FiniteParameters.routingDepth copies groups dimension width; CompositionBound.overheadCostBound copies groups blockWidth dimension width (stepSuffixWidth level blockWidth) schedulerDepth groupBitWidth orderWidth routingDepth routingDepth ≤ 2 ^ stepInputWidth level blockWidth / stepInputWidth level blockWidth) : FiniteParameters.canonicalCostBound copies (groupCount level denominator blockWidth) blockWidth (stepDimension denominator) (CodeParameters.fieldWidth blockWidth (stepDimension denominator) ⋯) (stepSuffixWidth level blockWidth) (stepResourceBound recursiveConstant level blockWidth) ≤ stepMassConstant denominator recursiveConstant * (2 ^ stepInputWidth level blockWidth / stepInputWidth level blockWidth)

Once the overhead has entered one Shannon-scale unit, adding the recursive resource bank gives the complete canonical bound.

theorem Algebraic.MassProduction.BlockInduction.eventually_step_mass_bound (level numerator denominator : ℕ) (levelAtLeastTwo : 2 ≤ level) (denominatorPositive : 0 < denominator) (rateBelowLevel : (level + 1) * numerator < level * denominator) (previous : MassProducesAt (groupRateNumerator level denominator) (groupRateDenominator denominator * level)) : ∃ (nextConstant : ℕ), ∀ᶠ (blockWidth : ℕ) in Filter.atTop, ∀ (function : ScalarFunction Bool (stepInputWidth level blockWidth)) (copies : ℕ), 0 < copies → copies ≤ 2 ^ (numerator * stepInputWidth level blockWidth / denominator) → booleanMassComplexity function copies ≤ ↑(nextConstant * (2 ^ stepInputWidth level blockWidth / stepInputWidth level blockWidth))

Equal-multiple induction step: a previous-level eventual theorem gives the next level for all sufficiently large equal block widths.