Spherical leaf stability on a closed manifold needs only countable choice

Local spherical stability is finite: cover the compact sphere leaf $B_0$ by finitely many foliation boxes, choose finitely many connecting paths and the finite overlap relations among them, and use that every based loop of the sphere is contractible; finite compact homotopy transport makes all overlap transports the identity on one common short transversal, so the local plaque data patch to a compact plaque graph for every sufficiently small transverse parameter, producing a saturated product neighbourhood of $B_0$. Every leaf in these product charts is $C^2$ diffeomorphic to the actual reference leaf. Thus the union $S$ of compact leaves $C^2$ diffeomorphic to $B_0$ is nonempty, open and saturated; the argument uses only the trivial fundamental group of the sphere homeomorphism type, not a differentiable classification theorem.

Choose a smooth metric by F6 and a finite subcover from its family of strongly convex neighborhoods. Every nonempty finite intersection contracts along unique minimizing connectors. Induct on the cover size: the intersection of its last member with the preceding union is a union of fewer such sets with contractible finite intersections, so it has finite-dimensional rational homology by the same induction. Mayer–Vietoris F3 then gives finite-dimensional homology for the full union. In particular $H_2(M;\mathbb{Q})$ is finite-dimensional, using the countable-choice metric and convexity suppliers.

Let $x\in \bar{S}$ and let $A$ be the leaf through $x$. If $A$ were intrinsically noncompact, then for every finite collection of spherical leaves $B_1,\dots ,B_n$ the in-pair item F1 would construct a positive closed transversal through $A$ avoiding all $B_i$. Its saturation F1 is open and contains $A$, so it contains $x$ and hence some spherical leaf $B$ arbitrarily near $x$; this $B$ meets the transversal while every chosen $B_i$ misses it.

The transversal in step 2.1 misses the chosen $B_i$ and meets $B$, so F6 gives $[B]$ outside their rational span. By step 1.2 finitely many spherical-leaf classes form a basis of the subspace spanned by all such classes. Apply step 2.1 to that finite family; a further sphere class outside their span is impossible. Hence $A$ is compact.

Keep the compact limiting leaf $A$ fixed as reference in F1. Because $x\in \bar{S}$, spherical leaves meet its base transversal at parameters arbitrarily near zero: a foliation box projects nearby plaque points onto that transversal. A sufficiently near compact sphere is a one-sheeted collar graph over $A$, hence C² diffeomorphic to $A$. Thus $A$ is C² diffeomorphic to $B_0$, and $x\in S$. This uses one collar radius for fixed $A$, rather than uncontrolled radii for varying spheres. Therefore $S$ is closed as well as nonempty and open, and connectedness gives $S=M$.

If the foliation admitted a spherical leaf, step 4.1 would make every leaf a compact sphere, and a compact sphere leaf is simply connected, so every loop in it is null-homotopic in its own leaf and no leaf can carry a nonzero limitwise-nullhomotopy ($\mathrm{\Pi }$) class; thus a nonzero $\mathrm{\Pi }$ leaf excludes every spherical leaf. The sphere universal-cover alternative is excluded finitely as well: a compact simply connected oriented covering surface has a finite cover of its leaf, $\chi$ multiplies by the degree, and orientable finite normal forms give $2=d(2-2g)$, forcing genus $g=0$ and degree $d=1$, so a sphere universal cover means an actual sphere leaf; alternatively a circle of sphere leaves would make $M$ a sphere bundle over a circle whose monodromy patched by a finite $C^2$ path yields a positive closed transversal, contradicting the no-transversal hypothesis. All covers, paths and relations used are finite, hence only the standing countable choice from [F5] is consumed.