Fate Contagion and Termination Criteria for the Juggler Map

The Juggler map sends an even positive integer to the integer part of its square root and an odd positive integer to the integer part of its three-halves power. We prove that every nonempty set A closed under taking preimages satisfies ∑_(n ∈ A, n ≤ x)1/n ≥ c(log x)^(λ), for all sufficiently large x and every 0 < λ < λ_(ideal), where λ_(ideal) ≈ 0.4927 is the root of 2^(−λ) + (1/3)(3/4)^(λ) = 1. Thus every realized cycle basin and the set of unbounded orbits, if nonempty, obey this lower bound. Two proofs are given. The first combines exact inverse intervals, a monotone parity sweep, classical exponential-sum estimates and six disjoint parity productions, and reaches every λ < λ^(**) ≈ 0.4926, an explicitly specified root. The second uses two productions and no exponential sum: the fibers whose parity share is far from 1/2 have finite total logarithmic mass, by a continued-fraction lock, so the production coefficient may be averaged. That proof is formalized in Lean 4 with no hypothesis for every λ ≤ 100/203, which exceeds λ^(**).For any fixed N₀ ≥ 2 such that every start in [1, N₀] reaches 1, universal termination is equivalent to an eventual-entry statement: all but O(y(log y)^(−e)) odd starts in (y, 2y] enter [1, N₀], for some e > 1 − λ_(ideal); the threshold 103/203 is machine-checked. We give sufficient parity-cylinder and exponential-moment hypotheses at depth O(log log y) for a stronger statement with a time bound. These hypotheses remain unproved. A first-letter decomposition identifies the contribution of failures beginning with two odd steps, and an abstract production model describes possible improvements of the exponent. A separate appendix gives a conditional exponent 0.5392. The contagion theorem, the reductions that use it and the combinatorial layer are formalized in Lean 4 at the exponents stated; the analytic estimates of the first route are mathematical arguments outside the formalization, and the numerical experiments are observations. Neither universal termination nor the exclusion of a nontrivial cycle or an unbounded orbit is established.