Divisibility budget for a repeated affine block
ProvedCollatzWork.affineRepetitionBoundcollatz-work-import
Let with , and with . Assume for every . Then
The positive shifted initial value bounds repetitions of a fixed affine rule. Degenerate parameters remain covered when they satisfy the stated hypotheses.
Preamble
import Std import Init.Grind.Ordered.Module import Definitions.Def_CollatzWork_AffineRepetitionStatement import Theorems.Thm_CollatzWork_finiteRepetitionBound
Formal statement
theorem CollatzWork.affineRepetitionBound : AffineRepetitionBoundStatement := by sorry
Source