Compact manifold fundamental groups have finite generators without choice

First construct a compatible metric from finite data. Compactness supplies finitely many coordinate balls $V_i$ whose closures lie in larger coordinate balls with charts ${\phi }_i$; take their coordinate images concentric balls of radii $r_i<R_i$. A continuous radial function ${\chi }_i$ equals one on ${\bar{V}}_i$, decreases linearly to zero before the larger chart boundary, and is zero elsewhere on $M$. The finitely many functions ${\chi }_i$ and ${\chi }_i{\phi }_i$, extended by zero, are continuous because their coordinate supports are compactly contained in the charts. Their combined map $F$ into a finite Euclidean space is injective: for $x$, choose $i$ with $x\in V_i$, so ${\chi }_i(x)=1$; equality $F(x)=F(y)$ forces ${\chi }_i(y)=1$ and ${\phi }_i(x)={\phi }_i(y)$, hence $x=y$. A continuous injection of a compact space into a Hausdorff space is a homeomorphism onto its image: images of closed subsets are compact and hence closed. Therefore $d(x,y)=\mathrm{\mid }F(x)-F(y)\mathrm{\mid }$ is a compatible metric. All choices so far are finite.

Choose a finite cover of $M$ by contractible coordinate balls. It has a positive Lebesgue number $\lambda$: for a finite open cover the functions $x\mapsto d(x,M\setminus U)$, with the empty-complement case assigned a positive constant, are continuous; their finite maximum is everywhere positive and has a positive minimum on compact $M$. A sufficiently small number below that minimum makes every set of diameter less than $\lambda$ lie in some member, by taking a point in the set and using the corresponding distance bound. Choose $0<ϵ<\lambda \mathrm{/}10$. There is a finite cover by smaller coordinate balls $B_j$ of $d$-diameter less than $ϵ$, because one can shrink a coordinate neighborhood inside a metric ball of radius less than $ϵ\mathrm{/}2$ and then take a finite subcover. Choose $0<\delta <ϵ$ that is a Lebesgue number for this second finite cover. Any pair of points of distance less than $\delta$ can therefore be joined inside one $B_j$ by its straight coordinate path, of diameter less than $ϵ$.

Compactness gives a finite $\delta \mathrm{/}4$-net of anchors $a_0=o,a_1,\dots ,a_s$, with the basepoint added first. For each unordered distinct anchor pair of distance less than $\delta$, put an edge in a finite graph and map it to the straight coordinate path in the least-index $B_j$ containing that pair; the reverse orientation uses the reversed path. Map each vertex to its anchor. For any $x\in M$, let $a(x)$ be the least-index anchor at distance less than $\delta \mathrm{/}4$. Join $x$ to $a(x)$ by the straight path in the least-index $B_j$ containing them. These connectors have diameter less than $ϵ$ and are defined by finite lists and the chart formulas, without choosing a family of paths. At $o$ take the constant connector.

Let $\mathrm{\ell }$ be any based loop in $M$. Uniform continuity on its compact interval gives a finite subdivision such that each segment has image diameter less than $\delta \mathrm{/}4$. Write its successive endpoints as $x_i$ and anchors as $a_i=a(x_i)$. Then $d(a_i,a_{i+1})<3\delta \mathrm{/}4$, so the selected graph has an edge between successive distinct anchors; repeated anchors give the constant path. The loop formed by this edge, the original loop segment and the two endpoint connectors is contained in a set of diameter less than $4ϵ$: each connector and edge has diameter less than $ϵ$, and its initial or terminal point lies within $\delta \mathrm{/}4$ of an endpoint of the original short segment. This entire small loop therefore lies in one of the contractible coordinate balls of step 2.1. Contract it there. Gluing these finitely many homotopies, with adjacent connectors cancelling, shows that $\mathrm{\ell }$ is based homotopic to the resulting graph edge loop at $a_0=o$. Thus the fundamental-group map of the component of this finite graph containing $a_0$ is onto.

Choose a spanning tree of that finite graph component by its finite vertex order. For every oriented edge outside the tree, follow the tree path from the base vertex to its initial vertex, traverse the edge, and return along the tree path from its terminal vertex. These finitely many loops generate all graph edge loops: insert the corresponding tree paths at successive vertices of an edge loop; the intervening inverse tree paths cancel, and a tree-edge loop contracts by deleting immediate reversals. Step 4.1 then makes their images generate ${\pi }_1(M,o)$. All graph data, covers, nets and tree paths were finite; a loop uses its own one finite subdivision and finite homotopy construction. No infinite family of generators, partitions or primitives was selected. This proves the statement without AC.