[to do] fully iterative definition of goodstein HOS

[MphLee]

Let's switch to the symbolic dynamic version, aka the shift goodstein condition \(\sigma({\bf h})\cdot s={\bf h}\cdot \sigma({\bf h})\).
Maybe we the right way to go is by obtaining the \(A\)-equivariant shift goodstein as a normal equation inside the structure \({\rm Hom}_{\rm Mon}(A,M)^J\): \({\rm ev}_u(\sigma({\bf h}))\cdot s={\bf h}\cdot {\rm ev}_u(\sigma({\bf h}))\).
A quick check \(({\rm ev}_u(\sigma({\bf h}))\cdot s)_j=({\rm ev}_u(\sigma({\bf h})))_j\cdot s_j   \) the problem is that \(({\rm ev}_u(\sigma({\bf h})))_j\) is not defined in any meaningful way unless we move to another codomain by transporting the equation along the function \[u^*: {\rm Hom}_{\rm Mon}(A,M)^J\to{\rm Hom}_{\rm Mon}(\mathbb N,M)^J\]
but then it just is a rephrasing of the previous definition that doesn't add anything of value... it seems
\[\forall a\in A.\, u^*(\sigma({\bf h}))\cdot a^*(s)=a^*({\bf h})\cdot u^*(\sigma({\bf h}))\]
or maybe isn't... since there is a canonical map \(EV({\bf x},a)=a^*({\bf x})\)
\[EV: {\rm Hom}_{\rm Mon}(A,M)^J\times A\to{\rm Hom}_{\rm Mon}(\mathbb N,M)^J\]
define then for \(M=G\) the map \(\mathcal F ({\bf h}, a)=EV(\sigma{\bf h},u)\cdot EV(s,a)\cdot EV(\sigma{\bf h},u)^{-1} \) and ask for \(\bf h\) solutions of
\[\forall a.\,\mathcal F({\bf h},a)=EV({\bf h},a)\]
Apply curry to the second variable, obtain that \(A\)-equivariant goodstein maps are solutions of \[{\bar {\mathcal F}}({\bf h})=\bar{EV}({\bf h})\]