A one-third defect bound at a first coefficient contraction
ProvedCollatzWork.firstContractionThirdGapcollatz-work-import
Let be the shortcut Collatz map: for even and for odd . Write for its -fold iterate, with . Let count the odd inputs among the first shortcut steps, and let ; recursively for an even input and for an odd input. For , define , , and . A first coefficient contraction at time means , , and for every . Its existence is a hypothesis.
Let , with , and assume a first coefficient contraction at and . Then
The conclusion applies to an existing first crossing whose endpoint has not fallen below its start. It does not prove existence of a first crossing.
Preamble
import Std import Init.Grind.Ordered.Module import Definitions.Def_CollatzWork_ConvergenceStatement import Definitions.Def_CollatzWork_FirstContractionStatement import Definitions.Def_CollatzWork_QuarterGapStatement import Theorems.Thm_CollatzWork_mechanicalCoarseBound import Theorems.Thm_CollatzWork_orbitAffine import Theorems.Thm_CollatzWork_mechanicalEnvelope
Formal statement
theorem CollatzWork.firstContractionThirdGap : FirstContractionThirdGapStatement := by sorry
Source