No polynomial ranking function proves termination of the Erdős 261 greedy carry

Consider the Borwein–Loring / Erdős 261 greedy map on states $(N,R)$: $(N,R)\mapsto(N+1,\,2R\bmod(N+1))$.

Theorem. For every real polynomial $P(N,R)$ and every $N_0$, it is false that for all integers $N\ge\max(N_0,2)$ and $1\le R<N$:

1. $P(N,R)\ge0$, and
2. if $R'=2R\bmod(N+1)>0$ then $P(N+1,R')<P(N,R)$.

So no global (or eventually valid) polynomial ranking function can prove that greedy orbits terminate.

Proof (discrete, via exact cycles). For $k\ge2$ and $M\ge2$ the states $((2^k-1)M-k+i,\,2^iM)$, $i=0,\dots,k$ (last one $((2^k-1)M,M)$) form a greedy segment ($k-1$ doublings, then one subtraction returning to $R=M$). Comparing $M^d$-coefficients ($d$ the total degree) along the segment gives $h(c,2)=h(c,1)$ for the top form $h$ at every $c=2^k-1$; hence the top form is $aN^d$, and $a>0$ by nonnegativity on $(2M,M)$. The 2-cycle $(3M-2,M)\to(3M-1,2M)\to(3M,M)$ then gives $P(3M,M)<P(3M-2,M)$ for large $M$, but the $M^{d-1}$-coefficient of $P(3M,M)-P(3M-2,M)$ is $2ad\,3^{d-1}>0$.

Formalization Note. $P$ is an MvPolynomial (Fin 2) ℝ evaluated at ![N, R].