Padding mass-production bounds

This module packages the generic padding argument used by mass-production theorems. It compares Shannon scales across a bounded width increase and shows that every eventual rational-rate bound extends to all positive input lengths.

theorem Algebraic.MassProduction.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)

A floor-stable comparison of Shannon scales when the larger width adds at most padding variables.

theorem Algebraic.MassProduction.MassProducesAt.allLengths {numerator denominator : ℕ} (production : MassProducesAt numerator denominator) : MassProducesAtAllLengths numerator denominator

Padding by the fixed cutoff converts an eventual theorem into an every-positive-length theorem.