Documentation

Complexitylib.Algebraic.MassProduction.BlockInductionParameters

Equal-block induction parameters #

This module defines the request-group exponents used by one fixed-exponent induction step and proves the scheduler-capacity inequalities they satisfy. All rates and floor operations remain explicit natural-number arithmetic.

source
def Algebraic.MassProduction.BlockInduction.stepDimension (denominator : ℕ) :
ℕ

The recovery-code dimension used at every non-base induction step.

Equations
Instances For
    source
    theorem Algebraic.MassProduction.BlockInduction.stepDimension_positive {denominator : ℕ} (denominatorPositive : 0 < denominator) :
    0 < stepDimension denominator
    source
    theorem Algebraic.MassProduction.BlockInduction.stepDimension_atLeastTwo {denominator : ℕ} (denominatorPositive : 0 < denominator) :
    2 ≤ stepDimension denominator
    source
    def Algebraic.MassProduction.BlockInduction.groupRateNumerator (level denominator : ℕ) :
    ℕ

    Numerator of the group exponent in block units. It is one integer below the (k - 1)-block threshold at denominator 2 * denominator.

    Equations
    Instances For
      source
      def Algebraic.MassProduction.BlockInduction.groupRateDenominator (denominator : ℕ) :
      ℕ

      Denominator used to express the group exponent in block units.

      Equations
      Instances For
        source
        def Algebraic.MassProduction.BlockInduction.groupExponent (level denominator blockWidth : ℕ) :
        ℕ

        Floored base-two exponent of the number of request groups.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          def Algebraic.MassProduction.BlockInduction.groupCount (level denominator blockWidth : ℕ) :
          ℕ

          Exact power-of-two number of request groups at one induction step.

          Equations
          Instances For
            source
            theorem Algebraic.MassProduction.BlockInduction.groupRateNumerator_add_one (level denominator : ℕ) (levelAtLeastTwo : 2 ≤ level) (denominatorPositive : 0 < denominator) :
            groupRateNumerator level denominator + 1 = 2 * denominator * (level - 1)
            source
            theorem Algebraic.MassProduction.BlockInduction.groupRate_below_previousLevel (level denominator : ℕ) (levelAtLeastTwo : 2 ≤ level) (denominatorPositive : 0 < denominator) :
            level * groupRateNumerator level denominator < (level - 1) * (groupRateDenominator denominator * level)
            source
            theorem Algebraic.MassProduction.BlockInduction.groupCount_positive (level denominator blockWidth : ℕ) :
            0 < groupCount level denominator blockWidth
            source
            theorem Algebraic.MassProduction.BlockInduction.groupCount_le_recursiveBudget (level denominator blockWidth : ℕ) (levelPositive : 0 < level) :
            groupCount level denominator blockWidth ≤ rationalCopyBudget (groupRateNumerator level denominator) (groupRateDenominator denominator * level) (level * blockWidth)

            The group count is exactly within the recursive rational copy budget on the level * blockWidth suffix.

            source
            def Algebraic.MassProduction.BlockInduction.groupLoadExponent (denominator blockWidth : ℕ) :
            ℕ

            A single rational exponent dominates the request load left in one group. The extra half-margin absorbs the one-unit loss from adding two floors.

            Equations
            Instances For
              source
              theorem Algebraic.MassProduction.BlockInduction.requestExponent_le_group_add_load (level numerator denominator blockWidth : ℕ) (levelAtLeastTwo : 2 ≤ level) (denominatorPositive : 0 < denominator) (rateBelowLevel : (level + 1) * numerator < level * denominator) (blockLarge : 4 * denominator ≤ blockWidth) :
              numerator * ((level + 1) * blockWidth) / denominator ≤ groupExponent level denominator blockWidth + groupLoadExponent denominator blockWidth
              source
              theorem Algebraic.MassProduction.BlockInduction.requestGroupSize_le (level numerator denominator blockWidth copies : ℕ) (levelAtLeastTwo : 2 ≤ level) (denominatorPositive : 0 < denominator) (rateBelowLevel : (level + 1) * numerator < level * denominator) (blockLarge : 4 * denominator ≤ blockWidth) (copiesBound : copies ≤ 2 ^ (numerator * ((level + 1) * blockWidth) / denominator)) :
              GroupedScheduler.requestGroupSize copies (groupCount level denominator blockWidth) ≤ 2 ^ groupLoadExponent denominator blockWidth

              Every permitted batch leaves at most 2^groupLoadExponent requests in a single request group.

              source
              theorem Algebraic.MassProduction.BlockInduction.step_loadBound (level numerator denominator blockWidth copies : ℕ) (levelAtLeastTwo : 2 ≤ level) (denominatorPositive : 0 < denominator) (rateBelowLevel : (level + 1) * numerator < level * denominator) (blockLarge : 4 * denominator ≤ blockWidth) (copiesBound : copies ≤ 2 ^ (numerator * ((level + 1) * blockWidth) / denominator)) :
              GroupedScheduler.requestGroupSize copies (groupCount level denominator blockWidth) * 2 ^ CodeParameters.fieldWidth blockWidth (stepDimension denominator) ⋯ < 2 ^ (CodeParameters.fieldWidth blockWidth (stepDimension denominator) ⋯ * (stepDimension denominator - 1))

              The exact scheduler-capacity inequality for one induction step.