Schur functions form an orthonormal integral basis

Fix $\lambda ⊢d$ with $n=\mathrm{\ell }(\lambda )>0$ and apply [F5] with $r=n$. In the determinant expansion, a permutation $\sigma \in S_n$ contributes $\mathrm{sgn}(\sigma ){\prod }_i{h}_{{\alpha }_i}$, where ${\alpha }_i={\lambda }_i-i+\sigma (i)$. If some ${\alpha }_i<0$, that term is zero by [F5]; otherwise ${\sum }_i{\alpha }_i=d$, and sorting the nonnegative ${\alpha }_i$ and omitting zeros gives a partition $\nu ⊢d$ with ${\prod }_i{h}_{{\alpha }_i}=h_{\nu }$. The identity permutation contributes $h_{\lambda }$ with coefficient one. For $\sigma \mathrm{\ne }\mathrm{i}\mathrm{d}$, some initial set $\{1,\dots ,k\}$ is not preserved, so ${\sum }_{i\le k}\sigma (i)>{\sum }_{i\le k}i$; for every $k$, the same sum is at least ${\sum }_{i\le k}i$. Hence ${\sum }_{i\le k}{\alpha }_i\ge {\sum }_{i\le k}{\lambda }_i$ for all $k$, strictly for some $k$. Sorting the nonnegative ${\alpha }_i$ can only increase each prefix sum, so every nonzero nonidentity term has $\nu ⊳\lambda$.

For $d>0$, combine equal terms in step 1.1 to write $s_{\lambda }={\sum }_{\nu ⊢d}{c}_{\lambda \nu }{h}_{\nu }$, where $c_{\lambda \lambda }=1$ and $c_{\lambda \nu }=0$ unless $\nu =\lambda$ or $\nu ⊳\lambda$. The dominance poset of the finite set of partitions of $d$ has a linear extension (successively remove a minimal element), making this coefficient matrix triangular with diagonal one. Its off-diagonal part is nilpotent, so the finite inverse $I-N+N^2-\cdots$ has integer entries. Thus the $s_{\lambda }$ form a $\mathbb{Z}$-basis because the $h_{\nu }$ do by [F4]. For $d=0$, [F2] gives only $\mathrm{\varnothing }$, and [F5] gives $s_{\mathrm{\varnothing }}=1$, the basis of ${\mathrm{\Lambda }}^0=\mathbb{Z}$.

Fix $d\ge 0$ and index the finite partition set by $P_d$. The basis result of step 2.1 and the $h$-basis [F4] give invertible rational matrices $A,B$ with $s_{\lambda }={\sum }_{\alpha \in P_d}{A}_{\lambda \alpha }{h}_{\alpha }={\sum }_{\beta \in P_d}{B}_{\lambda \beta }{m}_{\beta }$. Comparing the two degree-$(d,d)$ Cauchy expansions in [F6] gives $A^{\mathsf{T}}B=I$. By [F7], the pairing matrix is $(⟨s_{\lambda },s_{\mu }{⟩}_H{)}_{\lambda ,\mu }=A{B}^{\mathsf{T}}=I$, since $B=(A^{\mathsf{T}}{)}^{-1}$. This proves orthonormality without assuming symmetry of the Hall form. In degree zero both bases consist of $1$, so the pairing is $⟨1,1{⟩}_H=1$; in degree one, $s_{(1)}=h_1$ and the same kernel calculation gives $⟨s_{(1)},s_{(1)}{⟩}_H=1$.

If $\mathrm{\mid }\lambda \mathrm{\mid }\mathrm{\ne }\mathrm{\mid }\mu \mathrm{\mid }$, gradedness in [F7] gives zero pairing, and bilinearity makes any zero input pair to zero. The proof treats the least degree $d=0$, the minimal Jacobi–Trudi size $n=\mathrm{\ell }(\lambda )$, and every finite partition set at each $d$. The determinant terms, matrix inverse, and linear extension of a finite poset use only finite operations; no form of the axiom of choice is used.