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 of positive integers closed under taking preimages satisfies ∑_(n ∈ A, n ≤ x)1/n ≥ c(log x)^(37/50) for all sufficiently large x. Thus any realized cycle basin or nonempty class of unbounded orbits must have this divergent logarithmic mass. Five disjoint actual predecessor families, with initial words E, OE, OOEE, OOOEE and OOEOE, supply the recursion. The two five-letter families enter through the averaged fair-share theorem of the companion Paper B (its Theorem 6.3), an AI-assisted written proof that has not been independently reviewed; the deduction from that theorem, and the recursion, are kernel-checked in Lean.Without the two five-letter families the exponent is 5/8, and that result is now machine-checked end to end: Lean proves the actual OOEE production from its summable poor-fiber tail, and Appendix E gives the written argument. The earlier two-production route remains an elementary Lean baseline at 100/203.For a fixed verified target [1, N₀], universal termination is equivalent to an eventual-entry statement: all but O(y(log y)^(−e)) odd starts in (y, 2y] enter that target, for some e > 13/50; the machine-checked threshold, which does not use Paper B, is 3/8. The rate itself remains unproved. Parity-cylinder, live-pressure and scale-averaged pressure bounds are sufficient arithmetic inputs; none is established here. Earlier finite-production and localized-discrepancy arguments are retained with their original scope, and the numerical experiments remain observations. Neither universal termination nor exclusion of every nontrivial cycle or unbounded orbit is established.