Finite excursion chain with a terminal budget descends
ProvedCollatzWork.excursionChain_terminal_descentcollatz-work-import
Let be the shortcut Collatz map: for even and for odd . Write for its -fold iterate, with . Write for the assertion that for some . Let be a finite list of segments of natural numbers, with . Starting from , define successive endpoints by applying . Assume each segment satisfies . Write , , and , with empty products 1.
Let and . Assume and . Then
The segment and terminal envelopes and cumulative budget are hypotheses; no all-root coverage is asserted.
Preamble
import Std import Init.Grind.Ordered.Module import Definitions.Def_CollatzWork_ConvergenceStatement import Definitions.Def_CollatzWork_ExcursionBudgetStatement import Theorems.Thm_CollatzWork_excursionChainEnvelope import Theorems.Thm_CollatzWork_terminalEnvelope_compose import Theorems.Thm_CollatzWork_excursionBudgetDescent
Formal statement
theorem CollatzWork.excursionChain_terminal_descent (segments : List ExcursionSegment)
(root steps B E : Nat) (hroot : 3 ≤ root)
(hchain : ExcursionChain root segments)
(hterminal : E * shortcutIter steps (shortcutIter (excursionSteps segments) root) <
B * (shortcutIter (excursionSteps segments) root + 3))
(hbudget : 2 * (excursionNumerator segments * B) ≤
excursionDenominator segments * E) :
shortcutIter (excursionSteps segments + steps) root < root := by sorry
Source