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. 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.The author used large language models throughout the development of this work, including drafting and revising the prose, proposing and developing proof arguments, writing Lean formalizations, and designing and implementing computations.