Banach–Alaoglu versus sequential Alaoglu

Three conclusions on dual balls have deliberately different hypotheses and proof costs.

• Banach–Alaoglu assumes the ultrafilter lemma and gives weak-star compactness for the dual ball of every normed space. It does not turn an arbitrary net into a sequence.
• When the predual is separable, A separable predual has weak-star sequentially compact dual ball combines the same compactness assumption with an explicit metric on the bounded ball; the compact-metric implication used there is choice-free.
• Dual unit ball has extreme points is stated under full AC because the implemented Krein–Milman branch uses Zorn and AC-backed Hahn–Banach in addition to the ultrafilter lemma needed for Alaoglu.

The companion counterexample shows that the first bullet cannot in general be strengthened to sequential compactness. No converse choice-theoretic claim is made here. In particular, the historical assertion that an appropriate Krein–Milman principle together with the ultrafilter lemma yields AC remains an unresolved source obligation in this run and is not recorded, cited, or used as a theorem. These distinctions also apply at the endpoints: the zero predual has a singleton dual ball satisfying all three conclusions trivially, while nonseparable preduals are where compactness and sequential compactness can separate.