Lower Bounds for Cycle Lengths in 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 obtain restrictions on hypothetical nontrivial cycles. For a cycle with minimum n, length L, and o odd steps, we prove the cycle-financing inequality nlog n (3^(o) − 2^(L)) ≤ L 3^(o). It bounds the formal expansion that accumulated floor losses can offset. A refinement transports these losses to a reduced base and bounds the resulting exponent-walk charge using an irrational rotation, Denjoy–Koksma estimates, and finite Ostrowski decompositions. Combined with the verified descent inputs described in the paper, the inequalities give period lower bounds of 25781, 176251, 478245, and 780239 at floors 10⁶, 26254995, 162849448, and 350000000, respectively. Separately, finite-word exclusions give at least four even steps without a descent-floor input; an exact computational classification strengthens this to eight even steps and period at least twenty-two. For cycles whose maximum is below the cube of their minimum, we also determine the complete rank order and mechanical itinerary, derive a uniform log-log grid bound, and prove the further height restriction M < m³ − m^(15/8) for m ≥ 7, where m, M are the minimum and maximum. Successive genuine return-gap contractions sharpen this to M < m³ − (1/2)m^(253/128) for m ≥ 2²⁴, and to M < m³ − (1/2)m^(127/64) for m ≥ 2¹²⁸, with a slightly stronger exponent in the latter case. A terminal word factorization identifies the expansion still uncontrolled by these contractions. Exact short-return cells identify the rounding information discarded by several relaxed no-cycle criteria. Transposed to the shortcut Collatz map through the shared parity word, the financing inequality and the walk charge reproduce the published Collatz cycle-length bounds of Eliahou and Hercher exactly and replace the constant 3/4 of Hercher’s height bound by 1/(2log 2); on the negative integers they give the financing inequality in the Juggler direction, with a Lean proof; with the 3x − 1 map verified through 2⁴⁴ by the author, that inequality gives period at least 16483927 for any further negative cycle of the shortcut Collatz map. The core inequalities and selected classifications are formalized in Lean 4. The descent computations, per-length numerical comparisons, and remaining analytic identifications are distinguished from those formal proofs. A limitation result applies to charges retaining a positive contribution at a fixed floor. Neither the exclusion of all nontrivial cycles nor universal termination is established.