The grand loop: existence of the highest weight crystal bases

Field spanning. On any fixed label space, $\mathrm{im}{F}_i=\mathrm{im}{\tilde{f}}_i$: in a string expansion $x={\sum }_n{F}_i^{(n)}{x}_n$, one has $F_{i}x={\tilde{f}}_i{\sum }_n[n+1{]}_i{F}_i^{(n)}{x}_n$, and conversely ${\tilde{f}}_{i}x=F_i{\sum }_n[n+1{]}_i^{-1}{F}_i^{(n)}{x}_n$. Both sums have the same label as $x$. The same identities hold on the negative half. Since every positive-height space is ${\sum }_i{F}_i$ of the preceding spaces, it is also ${\sum }_i{\tilde{f}}_i$ of those spaces. Induction from the highest line or the unit therefore proves that the lowering words span every field component. Together with [F2] this makes each $\mathcal{L}$ component a finite free full lattice.

The base. [base] At height zero the top and unit have norm one, raising kills them and $\mathrm{\Phi },\mathrm{\Psi }$ identify the tensor top. At degree ${\alpha }_i$, put $m=\lambda (h_i)$ and $n=\mu (h_i)$. The module lattice is $A_0{F}_i{v}_{\lambda }$ if $m>0$ and zero otherwise; the half lattice is $A_0{F}_i$. All projection, raising, basis and inverse clauses follow from these one-dimensional strings. In the tensor degree, $\mathrm{\Phi }(F_i{v}_{\lambda +\mu })=F_i{v}_{\lambda }\otimes v_{\mu }+q_i^m{v}_{\lambda }\otimes F_i{v}_{\mu }$. If $m+n>0$, adjunction gives $\mathrm{\Psi }(F_i{v}_{\lambda }\otimes v_{\mu })=d(m,1)d(m+n,1{)}^{-1}{F}_i{v}_{\lambda +\mu }$ and $\mathrm{\Psi }(v_{\lambda }\otimes F_i{v}_{\mu })=q_i^{m}d(n,1)d(m+n,1{)}^{-1}{F}_i{v}_{\lambda +\mu }$, where $d(k,1)=(1-q_i^{2k})\mathrm{/}(1-q_i^2)$ and absent vectors contribute zero. These coefficients lie in $A_0$; their residues are respectively $1,0$ if $m>0$, and $0,1$ if $m=0<n$. If $m=n=0$ the degree vanishes. Thus E, F and G hold at height one as well, and all A-O base clauses hold.

Induction hypothesis. [ih] Fix $r\ge 2$ and assume A-O at every height $<r$, simultaneously for all dominant weights in one auxiliary regular datum supplied by [F6]. All subsequent large weights and fundamental weights are taken in that datum. The transported original highest-weight and tensor modules have the same $E_i,F_i,K_i$, string operators, normalized forms and lowering words; consequently the final conclusions on them restrict to the original labels.

String components below $r$. For $u={\sum }_{n=0}^N{F}_i^{(n)}{u}_n\in {\mathcal{L}}_{\lambda -\alpha }$ with $\mathrm{\mid }\alpha \mathrm{\mid }<r$, the shift identity gives $u_N={\tilde{e}}_i^{N}u\in \mathcal{L}$. Subtract ${\tilde{f}}_i^N{u}_N=F_i^{(N)}{u}_N$ and descend on $N$; each coefficient is integral. The same argument, using H$(r-1)$, applies to the half, and also applies to $q^k\mathcal{L}$ for every integer $k$. If $u$ represents a basis word residue, induct on $N$: when ${\tilde{e}}_{i}u\in q\mathcal{L}$, extracting its coefficients gives $u_n\in q\mathcal{L}$ for all $n\ge 1$; otherwise its residue is a lower-height basis word by B or I, and C or J gives $u\equiv {\tilde{f}}_i{\tilde{e}}_{i}u(\mathrm{m}\mathrm{o}\mathrm{d}q\mathcal{L})$. Induction and component extraction then leave exactly one nonzero coefficient residue, which is a highest word residue. This proves the lower-height single-string assertion without assuming it at height $r$.

Lower-height tensor control. Extract the string coefficients of two lattice inputs of factor heights $<r$ by step 2.1. For each pair of nonzero highest coefficients $h,h^{\mathrm{\prime }}$, the full divided-string rectangle ${\sum }_{j,k}{A}_0{F}_i^{(j)}h\otimes F_i^{(k)}{h}^{\mathrm{\prime }}$ lies in the tensor lattice, since each divided position is an iterate of ${\tilde{f}}_i$. The rank-one lemma [F5] proves stability of this rectangle and its residue rule, and linearity gives stability for the original inputs. For basis residues, the single-string assertion of step 2.1 gives the strict/non-strict tensor comparisons and their partial inverses. A lower-height module basis residue killed by every raising must be its top: otherwise its recursive lowering predecessor and C$(r-1)$ supply a nonzero raising. Hence a tensor basis residue of lower factor heights killed by all raisings has first factor $v_{\lambda }$. Moreover, on a top-second tensor, lowering agrees modulo $q$ with lowering the first factor whenever that first lowering is nonzero; iterating this rule along a word that survives in the first factor gives the same word on the tensor top modulo $q$.

Large-weight estimates. Write $T_i=q_i^{-1}{K}_i{E}_i$. On $F_i^{(n)}{u}_n$ with top integer $a$, its coefficient to the preceding position is $q_i^{a-2n+1}[a-n+1{]}_i=q_i^{1-n}(1-q_i^{2(a-n+1)})\mathrm{/}(1-q_i^2)$, whose inverse lies in $A_0$ for admissible $n\ge 1$. If $T_{i}u\in q^N\mathcal{L}$ in the preceding degree, step 2.1 extracts each $u_n\in q^N\mathcal{L}$ for $n\ge 1$. For fixed degree and fixed $m$, the differences between ${\tilde{f}}_i^{m}u$, $F_i^{(m)}u$ and between ${\tilde{e}}_i{F}_i^{(m)}u$, $F_i^{(m-1)}u$ involve only these positive components with Gaussian coefficients of bounded pole order; the second comparison requires $m\le ⟨h_i,\mathrm{w}\mathrm{t}(u)⟩$, so the top term is not killed at its bottom. Taking $N$ larger than those finitely many pole orders makes both differences lie in $q\mathcal{L}$. Now for $e_i^{\mathrm{\prime }}Q=0$, the commutator gives $T_i(Q{v}_{\lambda })=-(1-q_i^2{)}^{-1}{q}_i^{2⟨h_i,\lambda +{\alpha }_i+\mathrm{w}\mathrm{t}Q⟩}(e_i^{\mathrm{\prime }\mathrm{\prime }}Q)v_{\lambda }$. The last vector has degree below $r$; express it in a fixed finite set of half lowering words and apply L$(r-1)$ to obtain a pole bound independent of $\lambda$. The displayed power makes this arbitrarily small when $\lambda$ is large. Applying the two comparisons to each fixed half string $F_i^{(n)}Q$ proves the large-weight operator congruences needed at degrees $r-1$ and $r$, uniformly on any specified finite family of vectors. Finally ${\pi }_{\lambda }$ is a field isomorphism at degree $\alpha$ when $\lambda (h_j)\ge \mathrm{\mid }\alpha \mathrm{\mid }$: the highest-weight quotient ideal is generated by $F_j^{(\lambda (h_j)+1)}{v}_{\lambda }$, which are highest vectors by the rank-one formula and $[E_i,F_j]=0$ for $i\mathrm{\ne }j$. Their generated submodules have degrees at least $\lambda (h_j)+1$, so they cannot meet that degree.

E(r). The height-$r$ module lattice is the sum of ${\tilde{f}}_i$ of height-$r-1$ components. By naturality, $\mathrm{\Phi }{\tilde{f}}_i={\tilde{f}}_i\mathrm{\Phi }$. E$(r-1)$ puts each preceding image in the tensor lattice; every tensor summand there has both factor heights $<r$, so step 3.1 proves the required lowering stability on those inputs. Thus $\mathrm{\Phi }\mathcal{L}(\lambda +\mu {)}_{\lambda +\mu -\alpha }\subseteq \mathcal{L}(\lambda )\otimes \mathcal{L}(\mu )$.

Splitting at the last color change. For a nonpure word ${\tilde{f}}_{i_1}\cdots {\tilde{f}}_{i_r}$ take $t<r$ with $i_t\mathrm{\ne }{i}_{t+1}=\cdots =i_r$, put ${\lambda }_0={\mathrm{\Lambda }}_{i_t}$ and take $\mu$ large. The repeated tail acts only on the second factor of $v_{{\lambda }_0}\otimes v_{\mu }$, because ${\lambda }_0(h_{i_r})=0$. The resulting tensor is $E_{i_t}$-highest, since $E_{i_t}$ commutes with that different-color tail; its next lowering equals $F_{i_t}{v}_{{\lambda }_0}\otimes \text{tail}+q_{i_t}{v}_{{\lambda }_0}\otimes F_{i_t}\text{tail}$. The second term lies in $q$ times the tensor lattice, and the first has both factor heights positive. Applying the remaining prefix uses only the lower factor-height rules of step 3.1. Consequently the full tensor word is congruent to a product of basis word residues, or zero, with both factor heights strictly between $0$ and $r$. This decomposition is used for large total weight ${\lambda }_0+\mu$, not for an arbitrary $\lambda$ lacking such a dominant subtraction.

M(r), L(r) and large-weight lattice isomorphism. For $P\in \mathcal{L}(\mathrm{\infty })$ of degree at most $r-1$, take $\mu$ large and apply $\mathrm{\Phi }$ to the large-weight lowering congruence of step 3.2. E(r), already proved, carries its error into $q$ times the tensor lattice; L$(r-1)$ and E$(r-1)$ put $P(v_{\lambda }\otimes v_{\mu })$ in that lattice. The retraction $S$ sends the tensor lattice onto $\mathcal{L}(\lambda )$: it extracts the second top coefficient. It commutes with lowering modulo $q$ on these inputs by step 3.1: string tensors with a positive-degree second factor are killed both before and after lowering, while a second top gives the first-factor lowering or a zero first-factor endpoint. Applying $S$ therefore gives M(r). Iterating along a word gives integrality of its projection and equality with the module word modulo $q$. Hence $\mathcal{L}(\lambda {)}_{\lambda -\alpha }={\pi }_{\lambda }(\mathcal{L}(\mathrm{\infty }{)}_{-\alpha })+q\mathcal{L}(\lambda {)}_{\lambda -\alpha }$; Nakayama on the finitely generated quotient proves L(r). Nonzero projected word residues are precisely $\mathcal{B}(\lambda )$. For large $\lambda$, step 3.2 makes ${\pi }_{\lambda }$ a field isomorphism; L(r) then makes it a lattice isomorphism and hence a bijection on nonzero word residues, before any independence claim at height $r$.

Tensor-lattice decomposition. At total degree $\alpha$ of height $r$, put $T=(\mathcal{L}(\lambda )\otimes \mathcal{L}(\mu ){)}_{\lambda +\mu -\alpha }$ and $T^{\mathrm{\prime }}={\sum }_i{\tilde{f}}_i{T}_{\lambda +\mu -\alpha +{\alpha }_i}+v_{\lambda }\otimes \mathcal{L}(\mu {)}_{\mu -\alpha }$. Step 3.1 gives $T^{\mathrm{\prime }}\subseteq T$ on the preceding degrees. An interior product basis residue has both factor heights below $r$ and positive first height; the top detection and partial inverse in step 3.1 give a nonzero raising and write it as the lowering of its predecessor. Thus every interior tensor lies in $T^{\mathrm{\prime }}+qT$. The second-top boundary is generated by module lowering words tensored with $v_{\mu }$; each nonzero such residue is congruent to its word on $v_{\lambda }\otimes v_{\mu }$ by step 3.1, and that tensor word belongs to the lowering-image part of $T^{\mathrm{\prime }}$. Zero word residues already lie in $qT$. The remaining boundary is exactly $v_{\lambda }\otimes \mathcal{L}(\mu {)}_{\mu -\alpha }$. Hence $T=T^{\mathrm{\prime }}+qT$.

Nakayama upgrade. The quotient $T\mathrm{/}{T}^{\mathrm{\prime }}$ is finitely generated, and step 5.2 says $T\mathrm{/}{T}^{\mathrm{\prime }}=q(T\mathrm{/}{T}^{\mathrm{\prime }})$. Nakayama [F8] makes it zero. Thus the tensor decomposition is an exact lattice equality at height $r$, with the first-top boundary $v_{\lambda }\otimes \mathcal{L}(\mu )$; it does not require a basis of either factor at height $r$.

A(r) and H(r). Fix $i,\alpha$ and a finite set of dominant weights containing the desired $\tau$ and all ${\mathrm{\Lambda }}_j$. Finite full lattices give a common pole bound $N$ for raising on these components and on the half. Steps 3.2 and 5.1 extend that bound to every sufficiently large weight. The same bound applies to raising on the total-degree tensor lattice: interior inputs are already integral by step 3.1; at a boundary, extracting the positive string coefficients of the raised factor in $q^{-N}\mathcal{L}$ uses only preceding degrees, and applying the rank-one rectangles bounds their tensor raising by $q^{-N}$. If $N>0$, a pure-color word raises integrally by rank one. For a nonpure word at large weight ${\mathrm{\Lambda }}_j+\mu$, step 4.2 splits its tensor lift into an integral interior residue plus $qT$. Raising therefore lies in $T+q^{1-N}T=q^{1-N}T$, and applying $\mathrm{\Psi }$ in raised degree uses F$(r-1)$ to improve its module bound to $q^{1-N}$. For any fixed $\tau$ and word $u$, if $u\in q\mathcal{L}(\tau )$ the old bound already improves by one; otherwise its tensor word is congruent to $u\otimes v_{\mu }$. The improved bound at large $\tau +\mu$, followed by E$(r-1)$, bounds the raising of that tensor word by $q^{1-N}T$. The $qT$ error also raises into $q^{1-N}T$. Extracting the positive string coefficients of $u$ into $q^{-N}\mathcal{L}(\tau )$ and using the rank-one top-second rule gives ${\tilde{e}}_i(u\otimes v_{\mu })\equiv ({\tilde{e}}_{i}u)\otimes v_{\mu }(\mathrm{m}\mathrm{o}\mathrm{d}{q}^{1-N}T)$; extracting the second top then improves the bound for $u$. The large-weight operator congruence and lattice isomorphism similarly improve the half bound. All three bounds thus improve from $N$ to $N-1$; repeating finitely many times gives $N=0$, proving A(r), H(r). Component extraction as in step 2.1 now holds at height $r$, so all tensor lattice inputs of total height $r$ are stable under both operators by the same rectangle argument.

I(r), O(r) and B(r). For a nonpure negative-half word use the interior tensor splitting of step 4.2, apply the rank-one tensor raising rule and the lower-height clauses B and G, then transport through the large-weight projection of step 3.2; the pure-color case is rank one, giving I(r). For O(r), take a surviving word residue in $V(\lambda )$: tensoring with a large second top gives the residue $u\otimes v_{\mu }$; raising on a top-second tensor is congruent to ${\tilde{e}}_{i}u\otimes v_{\mu }$ by the rank-one rule, and comparing with the large-weight negative-half raising calculation, applying $\mathrm{\Phi }$ and then $S$, gives O(r). Then I(r), O(r) and the residue-image statement of step 5.1 give B(r), with no same-height C or F premise.

The module lattice pairing. String extraction is justified by A(r). Homogeneous top string components of different positions are orthogonal, because repeated contravariance reduces their pairing to a highest vector paired with a positive $F_i$-power, which is zero; at equal position $n$ with top rank-one weight $a$, the exact norm factor is $q_i^{n(a-n)}{\left(\genfrac{}{}{0px}{}{a}{n}\right)}_i\in 1+q{A}_0$. For a positive-height pair, recursively write one input as ${\tilde{f}}_i$ of a lower-height input, extract both strings and apply these unit norm ratios; this gives $⟨\mathcal{L}(\lambda ),\mathcal{L}(\lambda )⟩\subseteq A_0$ and $⟨{\tilde{f}}_{i}u,v⟩\equiv ⟨u,{\tilde{e}}_{i}v⟩<mrow><mi\; mathvariant="normal">m</mi><mi\; mathvariant="normal">o</mi><mi\; mathvariant="normal">d</mi></mrow>q$. At $n=0$ or $a=0$ the endpoint terms are zero, so no finite-string identity is misused.

The large-weight pairing normalization, corrected. If $Q$ has degree $-\nu$ and $P=F_{i}R$ with actual weight $-\nu +{\alpha }_i$, the exact commutator gives $⟨F_{i}Rv,Qv⟩=(1-q_i^2{)}^{-1}[⟨Rv,(e_i^{\mathrm{\prime }}Q)v⟩-q_i^{2⟨h_i,\lambda -\nu +{\alpha }_i⟩}⟨Rv,(e_i^{\mathrm{\prime }\mathrm{\prime }}Q)v⟩]$; inducting on height with $⟨F_{i}R,Q⟩=⟨R,e_i^{\mathrm{\prime }}Q⟩$ in the half shows that, for $\nu ={\sum }_i{n}_i{\alpha }_i$, the constant term is $C_{\nu }⟨P,Q⟩$ with $C_{\nu }={\prod }_i(1-q_i^2{)}^{-n_i}\in 1+q{A}_0$, so $⟨Pv,Qv⟩\equiv C_{\nu }⟨P,Q⟩$ modulo any prescribed $q$-order once every $\lambda (h_i)$ is large. The other term at each stage carries a large positive power of $q_i$, and its remaining lower-degree pairing is a finite polynomial in the variables $q_j^{2\lambda (h_j)}$ with bounded coefficients, uniformly for the finitely many vectors of a component; Kashiwara's constant-term lemma in §4 has the consistent constant term, and the printed factor direction of the corresponding grand-loop clause is not used.

A finite alternative for the half form. The recurrence in step 8.1 also constructs the half form without choice: on any fixed degree the module pairing is a polynomial in $x_i=q_i^{2\lambda (h_i)}$ with rational-function coefficients, by repeated first-letter removal. Its polynomial is unique, since a polynomial vanishing on all sufficiently large integer labels is zero (apply the finite root bound successively to the independent variables). Divide its constant term by $C_{\nu }$ to define $B_0(P,Q)$, and put it zero on unequal root degrees. If either half vector is zero, every module pairing is zero, so this is well defined on the actual half. The recurrence gives $B_0(F_{i}R,Q)=B_0(R,e_i^{\mathrm{\prime }}Q)$ and $B_0(1,1)=1$; symmetry follows from the module forms. Thus uniqueness of the normalized half form identifies $B_0$ with [F7]'s form. To prove nondegeneracy without its AC premise, first derive $e_i^{\mathrm{\prime }}{e}_j^{\mathrm{\prime }\mathrm{\prime }}=q_i^{a_{ij}}{e}_j^{\mathrm{\prime }\mathrm{\prime }}{e}_i^{\mathrm{\prime }}$ on words: commuting both sides past $F_k$ uses the two skew relations; the remaining coefficients agree because $q_j^{a_{ji}}=q_i^{a_{ij}}$, and induction starts at $1$. If a positive-degree $P$ is killed by every $e_i^{\mathrm{\prime }}$, then every $e_j^{\mathrm{\prime }\mathrm{\prime }}P$ has smaller degree and is also killed by every $e_i^{\mathrm{\prime }}$. Induction makes all $e_j^{\mathrm{\prime }\mathrm{\prime }}P=0$. The commutator then gives $E_{i}P=P{E}_i$ for every $i$. At large weight $P{v}_{\lambda }$ is therefore a highest vector of strictly lower label; its cyclic submodule cannot contain $v_{\lambda }$, by triangular highest-weight support, so simplicity forces $P{v}_{\lambda }=0$. Field injectivity from step 3.2 gives $P=0$. Finally a nonzero radical vector $P$ would have all $e_i^{\mathrm{\prime }}P$ in the lower-degree radical by the adjunction and symmetry; induction gives $e_i^{\mathrm{\prime }}P=0$ for all $i$, contradicting this separation. This supplies a choice-free form on each finite component whenever that qualification is needed. The declared inherited AC dependency is conservative; no additional simultaneous choice is required for finite duality or for the projection clauses.

Field-dual lattice transfer and special F(r). Choose an $A_0$-basis $P_k$ of $\mathcal{L}(\mathrm{\infty }{)}_{-\nu }$ and let $Q_j$ be its field dual under the nondegenerate field form of [F7], $⟨P_k,Q_j⟩={\delta }_{kj}$; define $\mathcal{L}(\mathrm{\infty }{)}_{-\nu }^{\vee }:={\sum }_j{A}_0{Q}_j$; the $Q_j$ need not lie in $\mathcal{L}(\mathrm{\infty })$. Their existence uses the nondegenerate field form of [F7], which inherits AC; choosing this one finite basis and its uniquely determined dual uses no additional choice principle. The corrected comparison of step 8.1 gives $⟨P_{k}v,Q_{j}v⟩\equiv {\delta }_{kj}<mrow><mi\; mathvariant="normal">m</mi><mi\; mathvariant="normal">o</mi><mi\; mathvariant="normal">d</mi></mrow>q$ because $C_{\nu }\equiv 1$; the pairing matrix is therefore invertible over $A_0$ by [F8], the large-weight field/lattice isomorphism gives ${\pi }_{\lambda }(\mathcal{L}(\mathrm{\infty }{)}^{\vee })=\mathcal{L}(\lambda {)}^{\vee }$, and $(\mathcal{L}(\lambda {)}^{\vee }{)}^{\vee }=\mathcal{L}(\lambda )$. For $\mu$ large, decompose the tensor lattice as in step 5.2; the lowering-image part passes through $\mathrm{\Psi }$ by F$(r-1)$. Pair the remainder $v_{\lambda }\otimes \mathcal{L}(\mu )$ with every $u\in \mathcal{L}(\lambda +\mu {)}^{\vee }$; writing $u=P{v}_{\lambda +\mu }$ with $P\in \mathcal{L}(\mathrm{\infty }{)}^{\vee }$, only the extreme toral term of $\mathrm{\Delta }P$ can pair with a first top, and its scalar is $q^{{\sum }_i{n}_i{d}_i\lambda (h_i)}\in A_0$ while $P{v}_{\mu }\in \mathcal{L}(\mu {)}^{\vee }$; adjointness therefore places $\mathrm{\Psi }$ of that remainder in the double dual $\mathcal{L}(\lambda +\mu )$, proving special F(r) for large $\mu$ without assuming unimodularity.

J(r). For a nonpure lowering word use its fundamental/large-weight interior tensor residue of step 4.2, whose two factor heights are $<r$. If its raised negative-half residue is nonzero, large-weight raising compatibility and the lower clause G make the tensor raised residue nonzero, and the lower tensor partial inverse gives $b_{\mathrm{t}\mathrm{e}\mathrm{n}\mathrm{s}\mathrm{o}\mathrm{r}}={\tilde{f}}_i{\tilde{e}}_i{b}_{\mathrm{t}\mathrm{e}\mathrm{n}\mathrm{s}\mathrm{o}\mathrm{r}}$; applying $\mathrm{\Psi }$ to this degree-$r$ congruence using special F(r) of step 9.2, and using the large-weight lattice isomorphism and operator congruences of step 3.2, gives $b={\tilde{f}}_i{\tilde{e}}_{i}b$ in $U_q^{-}$. The pure-color word uses the exact infinite-string identity ${\tilde{e}}_i{\tilde{f}}_i=\mathrm{i}\mathrm{d}$. This uses no same-height self-duality, general F or N.

C(r). If ${\tilde{f}}_{i}b=b^{\mathrm{\prime }}\mathrm{\ne }0$ with $b$ at preceding height, step 2.1 represents $b$ by a single highest string position modulo $q$. Since raising now preserves the lattice, shifting that position back gives ${\tilde{e}}_i{b}^{\mathrm{\prime }}=b$; the nonzero image excludes its bottom endpoint. Conversely suppose ${\tilde{e}}_i{b}^{\mathrm{\prime }}=b\mathrm{\ne }0$. By step 5.1 lift $b^{\mathrm{\prime }}$ to a half word residue $c$. O(r) from step 7.1 gives ${\pi }_{\lambda }({\tilde{e}}_{i}c)=b\mathrm{\ne }0$. By J(r), $c={\tilde{f}}_i{\tilde{e}}_{i}c$; applying the lowering projection congruence M(r) gives $b^{\mathrm{\prime }}={\tilde{f}}_{i}b$.

N(r). N(r) is the residue surjectivity of step 5.1 together with injectivity: if two surviving preimages have the same module image, raise by an index $i$ that does not kill that common image, use O(r) and the lower clause N$(r-1)$ to see that the raised negative-half residues agree, and apply J(r) to conclude that the two preimages were equal.

D(r) and K(r). Take a finite linear relation among the residue classes of the lowering words at height $r$ and apply each ${\tilde{e}}_i$: below $r$ the raised residues form an independent basis, and the partial-inverse statement makes the surviving preimages under each ${\tilde{e}}_i$ distinct, so every positive-degree word residue has a nonzero raising edge — in $V(\lambda )$ it is a ${\tilde{f}}_i$-predecessor and the string-component argument gives the inverse, in $U_q^{-}$ the identity ${\tilde{e}}_i{\tilde{f}}_i=\mathrm{i}\mathrm{d}$ on the lattice does. Hence every coefficient of the relation vanishes; recursive definitions give spanning, so D(r) and K(r) hold.

General F(r) and G(r). Once D$(r)$ and K$(r)$ and the partial inverse are proved, a residue killed by all ${\tilde{e}}_i$ in positive height is zero, by independence of the raised predecessor residues. If a field vector has all raisings in the lattice, take its minimal $q$-pole $N$; if $N>0$, its normalized nonzero residue is killed by all raisings, a contradiction, so the vector lies in the lattice. Applying this to $\mathrm{\Psi }$ of an arbitrary tensor lattice element, whose raisings lie in the lattice by tensor stability at height $r$ and F$(r-1)$, proves general F(r). For a tensor basis residue, if every raising vanishes then its $\mathrm{\Psi }$-image vanishes by the same residue detection; otherwise the tensor partial inverse, the lower clause G and the commutation of $\mathrm{\Psi }$ with the operators produce a basis word or zero, which is G(r).

Conclusion. Steps 1.2, 4.1, 5.1, 6.2, 7.1 and 10.1-12.1 prove A(r)-O(r) for every $r$ by induction, so all clauses hold at all heights. The direct sums of the free components are free without a simultaneous choice: enumerate $A_0$ by its rational-polynomial fractions and each component by its finitely many ordered word generators, and take the first finite tuple in that enumeration which is a basis; such a tuple exists by [F2]. These least-index choices give a basis of the graded direct sum. Thus $\mathcal{L}(\lambda )$ is a free $A_0$-module by [F2] with $\mathbb{Q}(q){\otimes }_{A_0}\mathcal{L}(\lambda )=V(\lambda )$ by step 1.1, stable under both operators by A(r); $\mathcal{B}(\lambda )$ is a $\mathbb{Q}$-basis of $\mathcal{L}(\lambda )\mathrm{/}q\mathcal{L}(\lambda )$ with the graded decomposition and operator stability by B, D and the definition, and the partial-inverse axiom is C(r); hence $(\mathcal{L}(\lambda ),\mathcal{B}(\lambda ))$ is a crystal basis in the sense of Crystal lattices, crystal bases and their crystals. The rank equality ${\dim }_{\mathbb{Q}(q)}V(\lambda {)}_{\mu }=\mathrm{\#}\mathcal{B}(\lambda {)}_{\mu }$ follows from the lattice splitting and D(r), and the negative-half statements give $\mathcal{B}(\mathrm{\infty })$ with the same properties, with the formal ${\phi }_i$ of The crystal graph, ${\epsilon }_i$, ${\phi }_i$ and the weight function. The transported labels are the original ones by [F6]. No global $\mathbb{Z}[q,q^{-1}]$-freeness, tensor-crystal theorem or $A_0$-perfectness premise is used; AC is inherited from the field-form supplier used in step 9.2, as declared in [F9].