The proved choice cost of the ultrafilter lemma

This item records only the choice cost established by proofs already present in the library.

The Axiom of Choice implies Zorn's lemma, and the converse implication is also proved here (The Axiom of Choice and Zorn's lemma are equivalent). The proof of the ultrafilter lemma applies Zorn's lemma to the partially ordered set of filters extending a given filter (The ultrafilter lemma, from the Axiom of Choice: every filter extends to an ultrafilter). Consequently the present development proves

$\mathrm{A}\mathrm{C}⟹\text{every filter extends to an ultrafilter}\mathrm{.}$

That is an upper bound on this proof, not a lower bound on the statement. Nothing in the argument proves that the ultrafilter lemma implies AC, that it is provable in ZF, or that it is not provable in ZF. Those questions require the later Boolean-algebra and symmetric-model machinery. Until those proofs are built, no Foundations item may use the recorded model results as a substitute.

The distinction matters downstream. A theorem that assumes an ultrafilter may cite that assumption directly. A theorem that constructs one using The ultrafilter lemma, from the Axiom of Choice: every filter extends to an ultrafilter inherits the AC-based proof supplied here. Neither case licenses an unproved assertion about the least possible choice principle.