The dual-canonical, canonical and quasi-canonical Fock bases

The two triangular charts. Fix a total order refining the finite-cut Bruhat order. Construct a fixed vector with leading term $M_A$ by descending elimination on its lower support. Suppose its bar discrepancy has largest remaining term $r{M}_B$; involutivity gives $r+\bar{r}=0$, since every higher discrepancy has already vanished. Write $r={\sum }_{n>0}{r}_n(s^n-s^{-n})$. There is a unique $c_{+}={\sum }_{n>0}{r}_n{s}^n$ in $s\mathbb{Z}[s]$ with $c_{+}-{\bar{c}}_{+}=r$, and a unique $c_{-}=-{\sum }_{n>0}{r}_n{s}^{-n}$ in $s^{-1}\mathbb{Z}[s^{-1}]$ with the same property. Adding the relevant $c_{\pm }{M}_B$ removes this discrepancy and changes only smaller ones. Finite descending elimination constructs the two charts, with uniqueness by the same largest-coefficient argument. This explicitly retains conjugation in the fixed-vector equation $c=B_{\psi }\bar{c}$. Each chart is integral unitriangular, hence an integral basis.

Rectification of the ground components. On a column cancel the simultaneous $i,i+1$ occurrences; concatenate the column words and cancel $-+$ pairs. In reverse tensor order this is the lower rule with ordinary column reading. Weakly increasing rows are stable: a changed entry violating the neighboring row inequality would have an equal neighboring entry giving a later surviving $+$ or earlier surviving $-$, contrary to the selected extremum; if that neighboring sign is cancelled, column strictness gives its matching mate in the same intervening strip and cancels the selected sign too. Apply this matching successively across neighboring columns, including unequal heights. The only highest tableau in this closed set is ground: starting at the rightmost column, absence of unmatched minus forces consecutive bottom entries from the alphabet minimum; induct leftward using row inequalities on the overlap, while a gap above it gives an unmatched minus with no right-hand mate. Raising decreases the entry sum to its finite lower bound, so the whole closed standard set is the reverse lower ground component. For the original lower order read columns from the right and align their tops; the same argument gives the reverse-standard set. Insert its reverse-column word by bumping the smallest larger entry. Adjacent insertions differ by the Knuth moves $acb\leftrightarrow cab$ for $a\le b<c$ and $bac\leftrightarrow bca$ for $a<b\le c$. Cancelling the three-letter signatures for each adjacent alphabet pair preserves their unmatched counts and selected sign, and the changed entry follows its bump path, so insertion commutes with crystal edges. Reverse insertion, bumping the largest smaller entry in the backward column word, reverses each successive bump path and preserves the row and column inequalities. Thus the two procedures are inverse, weight preserving, send ground to ground and identify ${\mathrm{R}\mathrm{e}\mathrm{v}}^{\mathrm{\Lambda }}$ with ${\mathrm{S}\mathrm{t}\mathrm{d}}^{\mathrm{\Lambda }}$ in the asserted lower charts.

The Gram matrices. Put $B=B_{\psi }$ with $\psi M_j={\sum }_i{B}_{ij}{M}_i$, and write $S_{ij}=⟨M_i,M_j⟩$. The normalization $⟨M_i,\psi M_j⟩={\delta }_{ij}$ says $SB=I$, since the second argument is linear. Therefore $S=B^{-1}$, with no transpose. Exactly the same equation holds for $C({\tilde{M}}_i,M_j)$, since its second argument is also linear, so its matrix is again $B^{-1}$. Involutivity says $B\bar{B}=I$, hence $B^{-1}=\bar{B}$.

The quasi-canonical family and the inverse charts. Let $U$ be the coefficient matrix of $L$ in $M$, with columns labelled by vectors, and set $D=U^{-1}$. The coefficient of $L_A$ in $M_B$ is $D_{A,B}=d_{A,B}(s)$, while $U_{A,B}=p_{A,B}(-s)$. The coefficient matrix of $P$ is $D^{\mathsf{T}}$, whose inverse is $U^{\mathsf{T}}$. These identities prove both displayed quasi-canonical expansions with the stated index positions and show integrality. The fixed-chart equation is $B_{\psi }\bar{U}=U$, where coefficient conjugation sends $s$ to $s^{-1}$.

Cuts and integrality. All four families are computed weight by weight from the same triangular equations, so they are Laurent-integral bases of each finite cut. Since the embeddings of [F1] preserve the monomial basis and the bar, they preserve these equations and hence the four families; on the highest constituent the normalized source pairing is $C_0$ up to the explicit weight rescaling proved in the global-basis comparison.

The reverse-bar adjoint calculation. Let $\omega$ be the linear anti-automorphism $E_i\mapsto F_i$, $F_i\mapsto E_i$, $D_a\mapsto D_a$; reversing products preserves the toral mixed, commutator and Serre relations. Write $H_i=D_i{D}_{i+1}^{-1}$. The source coproduct has $\mathrm{\Delta }{E}_i=1\otimes E_i+E_i\otimes H_i$, $\mathrm{\Delta }{F}_i=F_i\otimes 1+H_i^{-1}\otimes F_i$. Put $\mathcal{A}=\mathrm{f}\mathrm{l}\mathrm{i}\mathrm{p}\circ (\omega \otimes \omega )$. Direct substitution gives $\mathcal{A}\mathrm{\Delta }{E}_i=F_i\otimes 1+H_i\otimes F_i=\bar{\mathrm{\Delta }}{F}_i$ and $\mathcal{A}\mathrm{\Delta }{F}_i=1\otimes E_i+E_i\otimes H_i^{-1}=\bar{\mathrm{\Delta }}{E}_i$; the toral coproduct is unchanged. Hence $\mathcal{A}\mathrm{\Delta }(u)=\bar{\mathrm{\Delta }}(\omega u)$ and $\mathcal{A}\bar{\mathrm{\Delta }}(u)=\mathrm{\Delta }(\omega u)$ on the generated algebra. Applying the anti-automorphism $\mathcal{A}$ to $\mathrm{\Delta }(u)\mathrm{\Theta }=\mathrm{\Theta }\bar{\mathrm{\Delta }}(u)$ gives $\mathcal{A}(\mathrm{\Theta })\bar{\mathrm{\Delta }}(\omega u)=\mathrm{\Delta }(\omega u)\mathcal{A}(\mathrm{\Theta })$. Its degree-zero term is one and flip with $E\mathrm{/}F$ exchange preserves the positive-first/negative-second completion. The exact normalized uniqueness of [F3] therefore gives $\mathcal{A}(\mathrm{\Theta })=\mathrm{\Theta }$. On each ordered minuscule wedge factor the $E_i,F_i$ matrices are mutually transpose and the $D_a$ matrices are diagonal, so transpose realizes $\omega$. Consequently transposing the original two-factor bar and reversing factors gives the reverse-factor bar in the same tableau labelling. The same statement for successive prefixes follows from the coproduct factorization and parenthesization independence of [F1], [F3]; thus $\tilde{B}=B^{\mathsf{T}}$. In raw full-tensor labels this also reads $({\tilde{E}}_i{)}^{\mathsf{T}}=\overline{F_i}$, $({\tilde{F}}_i{)}^{\mathsf{T}}=\overline{E_i}$, where the bar acts on matrix coefficients and conjugates all toral weight powers. Finally ${\tilde{B}}^{\mathsf{T}}{B}^{-1}B=B=\overline{B^{-1}}$, so $C(\tilde{\psi }x,\psi y)=\overline{C(x,y)}$. This adjoint calculation uses the two ordinary tensor bars independently of charge transpose.

The sesquilinear delta identity. By step 2.1 the coefficient matrices are $U$ for $L$ and $D^{\mathsf{T}}$ for $P$, with $D=U^{-1}$. Thus the pairing matrix is ${\overline{D^{\mathsf{T}}}}^{\mathsf{T}}{B}^{-1}U=\bar{D}{B}^{-1}U$. The fixed-chart equation $B\bar{U}=U$ gives $B^{-1}U=\bar{U}$, so this product is $\bar{D}\bar{U}=I$. This proves $⟨P_A,L_B⟩={\delta }_{AB}$ directly, including coefficient conjugation.

The reverse-factor delta identities. Let $\tilde{U}$ and $V$ be the coefficient matrices of $\tilde{L}$ and $T$. Since $B\bar{V}=V$, their pairing matrix is ${\tilde{U}}^{\mathsf{T}}{B}^{-1}V={\tilde{U}}^{\mathsf{T}}\bar{V}$. Both $\tilde{U}-I$ and $\bar{V}-I$ have coefficients in $s\mathbb{Z}[s]$, so this matrix lies in $I+s\mathrm{Mat}(\mathbb{Z}[s])$. Step 2.3 makes each entry bar fixed, because the vectors being paired are fixed. The only bar-fixed polynomial in $s\mathbb{Z}[s]$ is zero, proving $C({\tilde{L}}_A,T_B)={\delta }_{AB}$. Replacing the positive charts by $\tilde{T}$ and $L$ gives a matrix in $I+s^{-1}\mathrm{Mat}(\mathbb{Z}[s^{-1}])$ and the same bar argument, proving $C({\tilde{T}}_A,L_B)={\delta }_{AB}$.

Conclusion. The four families $L,T,P$ and their reverse-factor counterparts are well-defined Laurent-integral bases of the finite Fock cuts with the stated triangular charts and delta pairings, and the reverse ground component is identified with ${\mathrm{S}\mathrm{t}\mathrm{d}}^{\mathrm{\Lambda }}$ by rectification. All later comparisons with the library upper family use the explicit weight rescaling of the global-basis theorem, never the bare names of the families.