A one-quarter defect bound at a first coefficient contraction
ProvedCollatzWork.firstContractionQuarterGapcollatz-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_QuarterGapStatement import Definitions.Def_CollatzWork_QuarterGapUniversalStatement import Theorems.Thm_CollatzWork_firstContractionThirdGap import Theorems.Thm_CollatzWork_firstContraction_quarter_of_certificate import Theorems.Thm_CollatzWork_universalMechanicalQuarterCertificate
Formal statement
theorem CollatzWork.firstContractionQuarterGap : FirstContractionQuarterGapStatement := by sorry
Source