The weight, ${\epsilon }_i$ and ${\phi }_i$ formulas for the tensor product crystal

The two integer pairs $(p,a)$ and $(s,r)$ determine the strings and the pairings: $p-a=⟨h_i,wt(b_1)⟩$ and $r-s=⟨h_i,wt(b_2)⟩$ by [F3], the $i$-string of $b_1$ has $p+a+1$ vertices and that of $b_2$ has $s+r+1$ vertices by [F3], and any $i$-string contains a unique top (a vertex with ${\tilde{e}}_i=0$) and a unique bottom (a vertex with ${\tilde{f}}_i=0$).

One application of ${\tilde{e}}_i$ to $b_1\otimes b_2$. If $p\ge s$, the non-strict comparison selects the first factor and ${\tilde{e}}_i(b_1\otimes b_2)={\tilde{e}}_i{b}_1\otimes b_2$ (or $0$ if $a=0$), so the pair $(p,a)$ becomes $(p+1,a-1)$ in the first factor and $s$ is unchanged; if $p<s$, the strict inequality selects the second factor, the pair $(s,r)$ becomes $(s-1,r+1)$ and $(p,a)$ is unchanged. Every application is a genuine existing edge of the corresponding factor precisely in the displayed case, by [F1] and the definition of ${\epsilon }_i,{\phi }_i$ in [F3].

Computation of ${\epsilon }_i(b_1\otimes b_2)=:\epsilon$. Case $p\ge s$: by step 1.2 every ${\tilde{e}}_i$-step acts on the first factor of the current pair, and the first factor offers exactly $a$ applicable steps before the next raising maps its top to $0$; each such step keeps the comparison $p^{\mathrm{\prime }}\ge s$ true because $p$ only increases, so exactly $a$ steps are possible and $\epsilon =a={\epsilon }_i(b_1)$. Case $p<s$: the first $s-p$ steps act on the second factor, decreasing $s$ to $p$ (each needs $s^{\mathrm{\prime }}>0$, and $s^{\mathrm{\prime }}>p\ge 0$ throughout), after which the comparison is $\ge$ and the remaining $a$ steps act on the first factor; exactly $a+s-p$ steps are possible and $\epsilon =a+(s-p)={\epsilon }_i(b_2)-⟨h_i,wt(b_1)⟩$ because $s-p+a=a+s-p$ and $p-a=⟨h_i,wt(b_1)⟩$ by step 1.1. Hence in both cases $\epsilon =\max (a,s-p+a)=\max ({\epsilon }_i(b_1),{\epsilon }_i(b_2)-⟨h_i,wt(b_1)⟩)$, which is (b).

Computation of ${\phi }_i(b_1\otimes b_2)=:\phi$. If $p>s$, every ${\tilde{f}}_i$-step while the comparison stays strict acts on the first factor and lowers $p$ by one and raises $a$ by one, keeping $s$ fixed, so after $p-s$ steps the comparison is an equality; each of those steps is an existing edge because the current $p^{\mathrm{\prime }}$ satisfies $p^{\mathrm{\prime }}>s\ge 0$, so $p^{\mathrm{\prime }}\ge 1$. From then on the non-strict comparison selects the second factor, which offers exactly $r$ steps before reaching its bottom. If $p\le s$, all ${\tilde{f}}_i$-steps act on the second factor, $r$ steps in all. Hence $\phi =r+\max (0,p-s)=\max ({\phi }_i(b_2),{\phi }_i(b_1)+⟨h_i,wt(b_2)⟩)$ because $p-s+r=p+⟨h_i,wt(b_2)⟩$ by $r-s=⟨h_i,wt(b_2)⟩$, which is (c).

The branch and tie assertions (d). The step counts of steps 2.1 and 2.2 also identify the branch of the first application: for $\epsilon$ the first maximum entry $a$ is attained for $p\ge s$, including equality, whereas the first application of ${\tilde{f}}_i$ uses the first factor only for $p>s$; the second entry is attained for $p<s$ and equals $s-p+a={\epsilon }_i(b_2)-⟨h_i,wt(b_1)⟩$; the first application of ${\tilde{e}}_i$ uses the first factor exactly for $p\ge s$ and of ${\tilde{f}}_i$ exactly for $p>s$, as displayed in [F1]. In particular the maximal value alone does not determine the ${\tilde{f}}_i$-branch, while the strict/non-strict split fixes it.

The partial-inverse property (e). Suppose $p>s$ and $b^{\mathrm{\prime }}:={\tilde{f}}_i(b_1\otimes b_2)={\tilde{f}}_i{b}_1\otimes b_2\mathrm{\ne }0$; then ${\phi }_i({\tilde{f}}_i{b}_1)=p-1\ge s$ by [F3], so the ${\tilde{e}}_i$-rule selects the first factor at $b^{\mathrm{\prime }}$ and ${\tilde{e}}_i{b}^{\mathrm{\prime }}={\tilde{e}}_i{\tilde{f}}_i{b}_1\otimes b_2=b_1\otimes b_2$. Suppose $p\le s$ and $b^{\mathrm{\prime }}:=b_1\otimes {\tilde{f}}_i{b}_2\mathrm{\ne }0$; then ${\tilde{f}}_i{b}_2\mathrm{\ne }0$ and ${\epsilon }_i({\tilde{f}}_i{b}_2)=s+1>p$ by [F3], so the ${\tilde{e}}_i$-rule selects the second factor and ${\tilde{e}}_i{b}^{\mathrm{\prime }}=b_1\otimes {\tilde{e}}_i{\tilde{f}}_i{b}_2=b_1\otimes b_2$. The converse is the same computation read backwards, and at the tie $p=s$ the split ${\tilde{e}}_i$ non-strict, ${\tilde{f}}_i$ strict is exactly what makes both readings consistent; this is the partial-inverse axiom already established in [F2], verified here from the explicit two-case logic.

Iteration along the string and the choice audit. By [F3] each existing ${\tilde{f}}_i$-edge raises ${\epsilon }_i$ by one and lowers ${\phi }_i$ by one, and by step 4.1 the displayed operators are a consistent partial-inverse structure on $B_1\otimes B_2$; iterating, ${\epsilon }_i({\tilde{f}}_i^n(b_1\otimes b_2))={\epsilon }_i(b_1\otimes b_2)+n$ and ${\phi }_i({\tilde{f}}_i^n(b_1\otimes b_2))={\phi }_i(b_1\otimes b_2)-n$ for all $n\le {\phi }_i(b_1\otimes b_2)$, which is (f), and the maximal such $n$ is ${\phi }_i(b_1\otimes b_2)$ by [F3]. All steps were finite checks on the two integer pairs $(p,a)$ and $(s,r)$ and the two factor strings; no choice principle is used.