Choice and convention ledger for paracompactness, Stone's theorem, and partitions of unity

Paracompactness here means the open-cover refinement property alone; Hausdorffness is not hidden in the word. It is therefore stated in the regularity, normality, shrinking, and partition-of-unity results that use it. The proofs of Every paracompact Hausdorff space is normal and its regularity predecessor use families of all eligible neighbourhoods, so they make no simultaneous choice. The cover-shrinking construction is recorded under the Axiom of Choice, and the partition theorem records Choice and Dependent Choice separately: Choice handles cover assignments, while the cited Urysohn construction is carried out under Dependent Choice.

The accessible primary text of Ornstein's proof has two distinct parts. Part (A) well orders the cover, removes closures of selected dyadic balls, and obtains a point-finite refinement. Part (B) renames that point-finite cover, assigns controlled-radius balls to their first containing member, and upgrades it to a locally finite refinement. Its local-finiteness test uses point-finiteness of the Part (A) output, so the locally finite lemma depends on the point-finite lemma. Stone's theorem is proved here under Choice as a sufficient assumption only; no exact-strength claim is made.