High mean two-adic valuation at least 8917/5626 forces a positive Syracuse cycle to be one
Provedsyracuse_cycle_eq_one_of_mean_valuation_ge_8917_over_5626Let T(n)=oddpart(3n+1). For arbitrary positive natural numbers m,p, suppose T^p(m)=m. Put K=sum_{i=0}^{p-1} v_2(3T^i(m)+1). If 8917p<=5626*K, then m=1.
The theorem covers the unbounded family of actual positive Syracuse cycles satisfying this high-mean condition. Its public type has no external baseline, margin, minimum-state, least-period, symmetry, divisibility-by-four, finite state bound or period-cap hypothesis. The proof imports the existing public Proved no-cycle-below-2310000 theorem, uses the effective four-window product threshold C=2786502 (not an orbit-state lower bound), and supplies the closed arithmetic certificate at exponent5626; that certificate does not require p=5626.
The strict complementary necessary condition for actual nontrivial cycles is 5626K<8917p. This new source packet has not been compiled, accepted or published. It does not assert that every possible cycle meets the high-mean condition, eliminate the remaining6291/9971 arithmetic pair, prove global word nondivisibility, exclude all cycles, close the unbounded tail or establish Collatz convergence.
import Mathlib import Definitions.Def_syracuseStep import Theorems.Thm_syracuse_no_cycle_below_2310000 set_option autoImplicit false set_option maxRecDepth 100000 set_option maxHeartbeats 0 set_option exponentiation.threshold 200000 open scoped BigOperators universe u
theorem syracuse_cycle_eq_one_of_mean_valuation_ge_8917_over_5626 (m p : ℕ) (hm : 0 < m) (hp : 0 < p)
(hcyc : syracuseStep^[p] m = m)
(hhigh : 8917 * p ≤ 5626 * (∑ i ∈ Finset.range p,
(3 * syracuseStep^[i] m + 1).factorization 2)) :
m = 1 := by sorry