Syracuse descent for odd numbers between 131789 and 135789
Provedsyracuse_descends_range_131789_135789Let be the Syracuse map, sending to the odd part of . For every odd with , some iterate of falls strictly below :
This is a descent statement, not a convergence statement: nothing is claimed about where the orbit eventually goes, only that it dips below its starting point.
Descent is exactly what is needed to exclude cycles. The minimum of a nontrivial cycle can never descend, so any satisfying the above is disqualified from being a cycle minimum. This is cheaper to certify than convergence, because each orbit need only be followed until its first drop below — which is automatically below — rather than all the way to .
Half the range is handled uniformly rather than by certificate: if then , so for , a single step. Only the residues need explicit orbit data, here step facts.
import Mathlib import Definitions.Def_syracuseStep
theorem syracuse_descends_range_131789_135789 (m : ℕ) (hlo : 131789 ≤ m) (hhi : m ≤ 135789) (hodd : Odd m) :
∃ t : ℕ, syracuseStep^[t] m < m := by sorry