Choice ledger for Baire, Urysohn, Stone, and Tychonoff

Ledger: separable complete metric Baire is a theorem of $\mathrm{Z}\mathrm{F}$; complete metric Baire is DC; compact-Hausdorff Baire is exactly DMC; Baireness of products of compact Hausdorff spaces is DC; DMC implies Urysohn's lemma; failure of Urysohn separation implies failure of DMC and bounded Tietze extension; the local positive implication does not provide a countermodel; Stone follows from AC, while the separate DC supplier states, relative to the consistency of ZF, that DC is consistent with a metrizable space having an open cover with no locally finite open refinement; the stronger per-cover effective refinement assertion for discrete metrizable spaces implies AC; compact Hausdorff products and cofinite products have the strength of BPI; compact $T_1$ and arbitrary compact products have the strength of AC. DC implies DMC; DMC-to-DC over $\mathrm{Z}\mathrm{F}$ remains open.

• Baire rows. Separable complete metric spaces are Baire in ZF is ZF, whereas Dependent Choice is equivalent to the complete-metric Baire principle over ZF proves over ZF that the unrestricted complete-metric Baire principle is equivalent to DC; DMC makes every compact Hausdorff space Baire gives DMC implies compact-Hausdorff Baire, Compact Hausdorff Baire implies DMC gives the converse and Compact Hausdorff Baire is equivalent to DMC packages the equivalence; DC is equivalent to Baireness of compact-Hausdorff products is the product row, which is DC and not merely DMC.

• Urysohn rows. DMC implies Urysohn's lemma proves the positive implication, and A failure of Urysohn separation forces failure of DMC proves its contraposition. A Urysohn separation obstruction also obstructs bounded Tietze extension proves that any supplied normal-space separation obstruction also obstructs bounded Tietze extension; it asserts no countermodel existence. The converse comparison is posed as a question in The converse from Urysohn separation to DMC: a comparison question.

• Stone rows. Stone's theorem, under choice: every metric space is paracompact is the AC row. The separate Relative consistency of DC with failure of Stone's theorem is the existing DC-comparison supplier. No BPI-to-Stone nonimplication is supplied here. Effective metacompactness for discrete metric spaces implies AC proves the effective strengthening with a refinement map; the distinction from the ordinary theorem is explained in The proved Stone theorem and its effective strengthening.

• Tychonoff rows. Cofinite products and compact Hausdorff products have the strength of BPI (Products of cofinite spaces are compact exactly under BPI, and the compact Hausdorff equivalence cited there); compact $T_1$ products and arbitrary compact products have the strength of AC (The compact T1 product theorem is equivalent to AC, The arbitrary compact product theorem is equivalent to AC).

• Principle rows. DC implies DMC. A consistent BPI counterexample theory obstructs a proof of DMC gives only the conditional criterion: if ZF+BPI+not Urysohn is consistent, ZF+BPI cannot prove DMC. No consistency of that counterexample theory is established by that corollary; the base-theory qualifications and the separate reversal question are in DMC, Multiple Choice, and AC qualifications and DMC versus DC over ZF remains open. No strict DMC-versus-DC claim over $\mathrm{Z}\mathrm{F}$ is made anywhere in this ledger.