Pulling out powers of 13 in the classification map g: a Lean lemma `g(13^t*N)=13^(t+1)*(N/12)` for structured N

Context

In the published classification /[2jbmwt]/ the simplified update map is $$ g(n)=\begin{cases}13\cdot (n/12),&4\mid n,\n,&4\nmid n.\end{cases} $$

To analyze iterations, it is useful to pull out an external factor $13^t$ before applying $g$, provided the remaining factor is divisible by $12$.

Main lemma

Let $$N = 2^{2k+3},3^{\ell+1},m.$$ Then $12\mid N$, and for all $t,k,\ell,m\in\mathbb N$: $$ g(13^t,N)=13^{t+1},(2^{2k+1},3^\ell,m). $$

This is proved by:

1. showing $4\mid 13^tN$ so the if-branch of $g$ is the $13\cdot(n/12)$ branch,
2. using Nat.mul_div_assoc (since $12\mid N$) to rewrite $(13^tN)/12 = 13^t,(N/12)$,
3. rewriting $N/12$ explicitly using an ac_rfl factorization of $N$ as $12\cdot(2^{2k+1}3^\ell)\cdot m$.

Lean4 formalization

The attached file GIterateOnGoodPow13.lean compiles with no sorry.

-- see attachment

Compilation

$ cd /opt/lean/Math
$ lake env lean GIterateOnGoodPow13.lean
# success (only minor simp-linter suggestions)