Lexicographic product formula for weakly-canonical poset games

Let $A$ and $B$ be poset games, with $B=2^n$ for some $n\in\mathbb{N}_0$, and suppose that $B$ is weakly-canonical. Let $A\otimes B$ be their lexicographic product, whose underlying set is $A\times B$ and where $(a,b)\leq(a',b')$ if and only if $a\leq_A a'$ and, when $a=a'$, also $b\leq_B b'$. For an element $x$ of a poset, write $x_\leq$ for the principal order ideal generated by $x$, and let $\mathcal{G}$ denote the Grundy value of a poset game. Lexicographic product formula. For every $(a,b)\in A\otimes B$, multiplication and addition being the standard operations on integers,

This proposed formula is related to the paper's study of equivalences and Grundy values in ideal play on poset games. The supplied text does not establish the converse of the preceding theorem and gives this result as a question; its resolution is not provided here.