Documentation

Complexitylib.Algebraic.MassProduction.EqualBlock

Exact parameters for the equal-block induction #

This module assembles the two-block base case of the fixed-exponent induction. Rates remain natural fractions, block lengths remain integral, and all floor and ceiling operations are explicit.

Padding arbitrary lengths to the next even length #

source
def Algebraic.MassProduction.EqualBlock.halfCeil (inputWidth : ℕ) :
ℕ

Ceiling of half the input width, used as the common padded block width.

Equations
Instances For
    source
    def Algebraic.MassProduction.EqualBlock.nextEvenWidth (inputWidth : ℕ) :
    ℕ

    The least even width represented as two copies of halfCeil.

    Equations
    Instances For
      source
      theorem Algebraic.MassProduction.EqualBlock.inputWidth_le_nextEvenWidth (inputWidth : ℕ) :
      inputWidth ≤ nextEvenWidth inputWidth
      source
      theorem Algebraic.MassProduction.EqualBlock.nextEvenWidth_le_add_two (inputWidth : ℕ) :
      nextEvenWidth inputWidth ≤ inputWidth + 2
      source
      theorem Algebraic.MassProduction.EqualBlock.shannonScale_nextEvenWidth_le (inputWidth : ℕ) (inputPositive : 0 < inputWidth) :
      2 ^ nextEvenWidth inputWidth / nextEvenWidth inputWidth ≤ 8 * (2 ^ inputWidth / inputWidth)
      source
      theorem Algebraic.MassProduction.EqualBlock.massProducesAt_of_rateBelowHalf (numerator denominator : ℕ) (denominatorPositive : 0 < denominator) (rateBelowHalf : 2 * numerator < denominator) :
      MassProducesAt numerator denominator

      The complete two-block base case P₁: every fixed rational rate below one half has eventual mass production for arbitrary positive input lengths.