Reflexive iff unit ball weakly compact

For every $f\in X^{\ast }$ and $x\in X$, $(x^{\ast \ast }\mapsto x^{\ast \ast }(f))(J_{X}x)=f(x)$. Consequently the pullback by $J_X$ of the weak-star initial topology on $X^{\ast \ast }$ is exactly the weak initial topology on $X$: both are generated by the same family $\{f:f\in X^{\ast }\}$. Since [F2] makes $J_X$ injective, it is a homeomorphism from weak $X$ onto $J_X(X)$ with the relative weak-star topology. This also covers $X=\{0\}$, when both spaces are singletons.

Isometry gives $J_X(B_X)=J_X(X)\cap B_{X^{\ast \ast }}$. Indeed $\parallel J_{X}x\parallel =\parallel x\parallel$, so both inclusions include the closed boundary $\parallel x\parallel =1$; if $X=0$, both sides are the singleton $\{0\}$.

Suppose first that $X$ is reflexive. By [F1], $J_X(X)=X^{\ast \ast }$, so step 1.2 gives $J_X(B_X)=B_{X^{\ast \ast }}$. Apply Banach–Alaoglu to the normed space $X^{\ast }$: under the ultrafilter lemma its dual ball $B_{X^{\ast \ast }}$ is weak-star compact. The homeomorphism in step 1.1 therefore transfers this compactness to weak $B_X$. This is the only direction, and the only step, that spends the ultrafilter lemma; in the selected Alaoglu proof it enters through [F9].

Conversely, suppose that $B_X$ is weakly compact. Step 1.1 makes the restriction $J_X{\mathrm{\mid }}_{B_X}$ weak-to-weak-star continuous, so [F6] makes $J_X(B_X)$ weak-star compact. The weak-star topology on $X^{\ast \ast }$ is Hausdorff by [F4], and hence [F7] makes $J_X(B_X)$ weak-star closed in $X^{\ast \ast }$. No compactness choice principle is used in this reverse implication: its compact set is the one in the hypothesis.

Goldstine [F8] says that $J_X(B_X)$ is weak-star dense in $B_{X^{\ast \ast }}$. It is contained in that ball by step 1.2 and is weak-star closed by step 2.2. Therefore $J_X(B_X)=B_{X^{\ast \ast }}$. This uses topological closure, not merely sequential closure.

Let $x^{\ast \ast }\in X^{\ast \ast }$. If $x^{\ast \ast }=0$, then $x^{\ast \ast }=J_{X}0$. If $x^{\ast \ast }\mathrm{\ne }0$, put $u^{\ast \ast }=x^{\ast \ast }\mathrm{/}\parallel x^{\ast \ast }\parallel \in B_{X^{\ast \ast }}$. Step 3.1 supplies $u\in B_X$ with $J_{X}u=u^{\ast \ast }$; scalar linearity then gives $x^{\ast \ast }=J_X(\parallel x^{\ast \ast }\parallel u)$. Thus $J_X$ is onto, so $X$ is reflexive by [F1]. This normalization treats the zero and norm-one endpoints separately and selects only one witness for the supplied $x^{\ast \ast }$, not a family of witnesses.

Steps 2.1 and 4.1 prove the two implications. HB is used through the canonical isometry [F2] and Goldstine [F8], and [F10] records exactly which additional principle that name denotes. The ultrafilter lemma is used only through Alaoglu in step 2.1; the reverse implication is choice-free once its weak compactness hypothesis and HB-backed Goldstine are supplied.