The equal-block induction

This module assembles the equal-block induction from its explicit parameter and scheduler bounds. At level k, the input is split into one prefix block of width m and a suffix of width k * m; successive steps cover every fixed rational exponent below one.

All positivity and size conditions are ordinary hypotheses. No instances are declared here.

Iterating the equal-block step

def Algebraic.MassProduction.BlockInduction.ProducesAtLevel (level : ℕ) : Prop

Level k of the manuscript induction: all rational rates strictly below k / (k + 1) have eventual mass production.

Equations

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

theorem Algebraic.MassProduction.BlockInduction.producesAtLevel_one : ProducesAtLevel 1

theorem Algebraic.MassProduction.BlockInduction.producesAtLevel_succ (previousLevel : ℕ) (previousLevelPositive : 0 < previousLevel) (previous : ProducesAtLevel previousLevel) : ProducesAtLevel (previousLevel + 1)

theorem Algebraic.MassProduction.BlockInduction.producesAtLevel_all (level : ℕ) (levelPositive : 0 < level) : ProducesAtLevel level

theorem Algebraic.MassProduction.BlockInduction.massProducesAt_of_rateBelowOne (numerator denominator : ℕ) (denominatorPositive : 0 < denominator) (rateBelowOne : numerator < denominator) : MassProducesAt numerator denominator

Eventual mass production at every fixed rational exponent strictly below one. A concrete level numerator + 1 already suffices.

From eventual bounds to the every-length headline theorem

theorem Algebraic.MassProduction.BlockInduction.massProducesAtAllLengths_of_eventual (numerator denominator : ℕ) (production : MassProducesAt numerator denominator) : MassProducesAtAllLengths numerator denominator

Compatibility name for the generic eventual-to-all-length padding theorem.

theorem Algebraic.MassProduction.BlockInduction.exponentialMassProduction : ExponentialMassProduction

The formal counterpart of the manuscript's main theorem.