Finite general position for a leafwise loop

Cover the compact image of $f$ by finitely many surface charts with convex coordinate disks, and subdivide the parameter circle finely enough that every segment maps into one such disk. Coordinate straight-line interpolation replaces each segment by its endpoint chord, through a homotopy fixing all segment endpoints. Near the base parameter, work in a chart centered at $x$. Replace a sufficiently short central interval by a nonconstant straight segment through $x$, with endpoints $x-\delta v$ and $x+\delta v$ for a fixed nonzero coordinate vector $v$; join those endpoints to the old endpoints in that same convex disk. Linear interpolation on this interval fixes its middle value $x$ throughout. Subdivide again if needed. This gives a based polygonal loop that is regular and straight on a fixed base collar; constant original loops are included by inserting this small based detour.

Vary the remaining finitely many vertices in small coordinate disks, fixing that entire base collar, to make every edge nonconstant and the incoming and outgoing tangent vectors at each other vertex noncollinear. Here is the finite genericity justification: for a fixed vertex and nonzero outgoing vector, varying its incoming neighboring vertex changes the incoming coordinate direction through an open subset of the plane, followed by an invertible coordinate-change differential. Collinearity is therefore a regular scalar equation in the joint vertex parameters, off the already excluded zero-edge locus; the zero-edge equations have codimension two. At a fixed base-collar endpoint the other neighboring vertex remains adjustable and gives the same scalar rank test. Insert an extra adjustable vertex if necessary so this holds at every corner. F2 makes these bad loci $C^1$ submanifolds of positive codimension; F3 makes their parameter images null. Choose arbitrarily small parameters outside their finite union. Each vertex movement and its edge-chord adjustment is a homotopy in a convex chart, still fixing the base collar.

Round the finitely many corners without losing regularity. In a vertex chart first make each incident edge exactly linear near the vertex: its Taylor remainder is $O(t^2)$ with derivative $O(t)$, so a cutoff on an interval of length $\delta$ changes its derivative by $O(\delta )$ and keeps it nonzero. If the two resulting directed velocities are $a,b$, choose a smooth function $\rho$ on $[-\delta ,\delta ]$, zero and one on end collars, with $\rho (-t)=1-\rho (t)$. Define the replacement from the incoming endpoint by integrating $(1-\rho (t))a+\rho (t)b$. Since the integrals of $\rho$ and $1-\rho$ are both $\delta$, the replacement reaches the outgoing endpoint and agrees with both straight edges on end collars. Its derivative never vanishes: noncollinearity excludes zero from the segment $[a,b]$. Shrink the chart and interval so its image stays in the convex disk. Coordinate straight-line homotopy relative to the two endpoints realizes the replacement; no corner is rounded at the basepoint, where the fixed collar was already straight. The result is a regular $C^2$ loop $g_0$, based-homotopic to $f$.

There is a uniform source separation scale $\eta >0$ for this immersion, stable under sufficiently small $C^1$ perturbations. Indeed cover the parameter circle by finitely many small intervals on which a target-coordinate projection of $g_0$ has derivative of one sign bounded away from zero. F4 gives injectivity on those intervals for all close maps. A Lebesgue scale for that finite cover excludes all coincidences with source distance below $\eta$. Choose nested closed base collars $J\subset \mathrm{int}{J}^{+}$ inside the fixed straight interval, with the diameter of $J^{+}$ below $\eta \mathrm{/}3$. Keep the entire $J$ fixed. The compact pair configurations with distance at least $\eta$ contain at most one parameter in $J^{+}$; triple configurations with all pair distances at least $\eta$ also contain at most one. Thus each relevant pair has at least one fully adjustable parameter outside $J^{+}$, and each triple has at least two.

Build one finite parameter family $g_v$ using source bumps supported off $J$, independent two-coordinate target translations in the actual surface charts, and composition of these translation factors. For each possible pair or triple coincidence choose disjoint source intervals around its adjustable parameters, with bumps equal to one there and target-chart margins containing their compact images. Finitely many configuration neighborhoods cover the compact pair and triple coincidence sets. At $v=0$, moving one adjustable image spans the two normal directions to the pair diagonal; moving two adjustable images spans the four normal directions to the triple diagonal, even when the third image is fixed. These are transverse-to-diagonal assertions, not a false full submersion claim for all values of a family with a fixed branch. Uniform smallness and the finite compact covers preserve the rank tests near all possible coincidences. Off those neighborhoods the original value configurations miss the closed diagonals by a positive margin, so small perturbations produce no new incidences there. Every member remains immersed and retains the separation estimate of step 4.1.

In a common target chart, the pair difference equation has two independent parameter derivatives. F2 makes its total zero set a $C^2$ manifold of dimension $P+2-2=P$, where $P$ is the parameter dimension. Critical values of its parameter projection are null by F3; at a regular parameter, elementary linear algebra identifies projection regularity with surjectivity of the two-source-parameter difference derivative. The slice coincidences are therefore transverse isolated pairs. The corresponding triple difference equation has four independent parameter derivatives; its zero manifold has dimension $P+3-4=P-1$, so its parameter image is null by F3 and good slices have no triples. These statements are applied on open separated-configuration neighborhoods; their finite or countable coordinate covers are covered by F3's null-union clause. If desired also exclude another branch hitting the fixed image $x$: outside the fixed base collar the same adjustable-value equation has source dimension one and target codimension two, giving zero-manifold dimension $P-1$ and a null parameter image; the fixed straight collar has only its specified preimage of $x$. Choose one arbitrarily small parameter outside these null exceptional sets. No unsupported four-direction rank test using only one moved branch is used.

For this parameter the double-pair set is closed in the compact separated pair configuration space and discrete by step 6.1, hence finite; no near-diagonal coincidence exists by step 4.1. The loop is regular and has no triple image. The homotopy $g_{tv}$ fixes every point of $J$, in particular the basepoint $x$, and joins $g_0$ to this final loop. Composing it with the based homotopies of steps 1.1–3.1 proves the statement. The source bumps all vanish near the basepoint; their cores were never required to cover that fixed collar. Target chart operations stay in $S$, hence in the given leaf when $S$ is a leaf. All chart and parameter families are finite; only the explicitly cited Sard/null machinery inherits countable choice.