Cycle minimum is at most
Provedsyracuse_cycle_min_boundLet be the Syracuse map. If is the smallest element of a -cycle of length , then
What it says. Dividing by , the inequality reads . The right-hand side exceeds by roughly , so the inequality can hold only when
The bound is essentially exact: the largest satisfying it is for , against .
Mathematical role. This is a single statement constraining every cycle length at once, in contrast to the case-by-case exclusions of individual short periods. It says the minimum of a Collatz cycle cannot be large relative to its accelerated length — equivalently, that a cycle whose elements are all big must be very long. Paired with computational verification of the conjecture up to some height , which forces for any nontrivial cycle, it converts directly into a lower bound on the period: any nontrivial cycle must satisfy . This is the standard route by which numerical verification yields period bounds, and it is the reason no short cycle can hide among large integers.
The proof is a two-line consequence of two facts about cycles: that the halvings strictly outweigh the triplings, , and that the minimum bounds the halving count, . The first gives purely because is an integer, and substituting that into the second yields the claim. No Diophantine input is used, and the descent principle is not assumed.
Formalization note. Minimality is stated over the whole forward orbit, , which for a cycle is minimality over the cycle. No oddness hypothesis is needed. The exponent has been eliminated from the statement, leaving a closed inequality in and alone.
import Mathlib import Definitions.Def_syracuseStep
theorem syracuse_cycle_min_bound (m a : ℕ) (hm : 0 < m) (ha : 0 < a)
(hcyc : syracuseStep^[a] m = m)
(hmin : ∀ i : ℕ, m ≤ syracuseStep^[i] m) :
(3 ^ a + 1) * m ^ a ≤ (3 * m + 1) ^ a := by sorry