Documentation

Complexitylib.Algebraic.MassProduction.BlockInductionStep

Arbitrary-width block induction step #

This module pads arbitrary input widths to equal-block multiples, transports the finite-step Shannon bound back across that padding, and exposes the rate-raising theorem massProducesAt_step.

Padding arbitrary widths to equal blocks #

source
theorem Algebraic.MassProduction.BlockInduction.shannonScale_le_of_le_add (inputWidth targetWidth padding : ℕ) (inputPositive : 0 < inputWidth) (fits : inputWidth ≤ targetWidth) (upper : targetWidth ≤ inputWidth + padding) :
2 ^ targetWidth / targetWidth ≤ 2 * 2 ^ padding * (2 ^ inputWidth / inputWidth)

Compatibility name for the generic Shannon-scale padding bound.

source
def Algebraic.MassProduction.BlockInduction.blockCeil (level inputWidth : ℕ) :
ℕ

Smallest equal-block width whose complete input covers inputWidth.

Equations
Instances For
    source
    def Algebraic.MassProduction.BlockInduction.nextEqualBlockWidth (level inputWidth : ℕ) :
    ℕ

    Least multiple of level + 1 represented by the equal-block layout.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      theorem Algebraic.MassProduction.BlockInduction.inputWidth_le_nextEqualBlockWidth (level inputWidth : ℕ) :
      inputWidth ≤ nextEqualBlockWidth level inputWidth
      source
      theorem Algebraic.MassProduction.BlockInduction.nextEqualBlockWidth_le_add (level inputWidth : ℕ) :
      nextEqualBlockWidth level inputWidth ≤ inputWidth + (level + 1)
      source
      theorem Algebraic.MassProduction.BlockInduction.shannonScale_nextEqualBlockWidth_le (level inputWidth : ℕ) (inputPositive : 0 < inputWidth) :
      2 ^ nextEqualBlockWidth level inputWidth / nextEqualBlockWidth level inputWidth ≤ 2 * 2 ^ (level + 1) * (2 ^ inputWidth / inputWidth)
      source
      theorem Algebraic.MassProduction.BlockInduction.massProducesAt_step (level numerator denominator : ℕ) (levelAtLeastTwo : 2 ≤ level) (denominatorPositive : 0 < denominator) (rateBelowLevel : (level + 1) * numerator < level * denominator) (previous : MassProducesAt (groupRateNumerator level denominator) (groupRateDenominator denominator * level)) :
      MassProducesAt numerator denominator

      The manuscript's equal-block induction step on arbitrary sufficiently large input widths.