A no-transversal leaf bounds a positive accessibility region with finite inward boundary

Reachability is open. In the last short product-chart segment of a positive path, its transverse derivative has a positive lower bound. Varying its endpoint slightly and interpolating this variation in that segment keeps the derivative positive, so every sufficiently nearby endpoint is also reachable. It is saturated: once a point of a leaf is reached by a genuine segment, F2 adjusts its endpoint to any specified point of that same leaf. Concatenation in F2 also shows forward invariance under every positive path. These arguments use actual nonempty segments, never the formal equality clause of the preorder.

A closed positive transversal meeting $L$ is already a positive return path from $L$ to $L$. Conversely F2 turns a genuine return into a positive path starting and ending at the same specified point of $L$. Smooth its closing corner in a product chart: both one-sided transverse derivatives are positive, so convolution and a sufficiently small collar interpolation keep them positive. The resulting closed immersed transverse curve still crosses $L$, since the local transverse coordinates immediately before and after that corner have opposite signs. For a smooth atlas every step can be smooth; for a $C^2$ atlas use $C^2$ convolution and interpolation.

The immersed closed curve of step 2.1 can be replaced by an embedded closed transversal meeting $L$. Keep a small interval at its chosen transverse crossing fixed. Its immersion gives a finite chart cover with uniform local injectivity, preserved by small $C^1$ perturbations: a projected coordinate has derivative of one sign bounded away from zero on each smaller interval. Outside a corresponding diagonal neighborhood, pair and triple configurations of source parameters are compact. Finitely many source-separated bumps with independent target-coordinate translations make each pair or triple value evaluation a submersion on neighborhoods of those configurations. Points of the fixed interval have distinct images; a possible coincidence involving it has another adjustable point. Include incidence with the retained image point among the finite generic conditions: another adjustable branch has source dimension one and target codimension n, so it misses that point for n>=2. After the perturbation a smaller fixed crossing interval is separated from all other branches there. On the coincidence manifold for $k=2,3$ the parameter projection has source dimension $P+k-(k-1)n$, where $P$ is parameter dimension and $n=\dim M$. F3's Sard theorem, or its lower-dimensional image clause, gives generic slice transversality. For $n\ge 3$ pair dimension $2-n<0$ gives an embedded curve. For $n=2$ pairs are isolated and compact, hence finite, and triple dimension $3-4<0$ excludes triples. At each remaining crossing, both branch directions have positive transverse-coordinate derivative; replace them in a small rectangle by two disjoint increasing graphs, switching partners and matching the order of their endpoints. Smooth the seams in the positive cone. The finitely many resolutions give disjoint embedded positive circles; retain the one containing the fixed crossing of $L$. For $n=1$, leaves are points; the compact component is a circle by [F5], and its positively oriented once-around parametrization is an embedded return. Thus a genuine return is equivalent to an embedded closed transversal.

Suppose $L$ meets no closed transversal. Steps 1.1–3.1 imply $N_L\cap L=\mathrm{\varnothing }$. Short positive segments starting at each point of $L$ show $L\subseteq \overline{N_L}$, hence $L\subseteq \mathrm{\partial }{N}_L$. In an oriented foliation box, saturation makes membership in $N_L$ constant on each plaque, and forward invariance makes the set of occupied transverse levels upward closed. Since $N_L$ is open, that set is empty, the whole interval, or an interval $(a,b)$ reaching the upper edge of the box. At a boundary point only the last case occurs. Therefore $\mathrm{\partial }{N}_L$ is exactly one plaque in a smaller box, and $\overline{N_L}$ is its positive half-box. These are smooth (respectively $C^2$) boundary charts, with positive normals pointing inward.

The boundary is closed in compact $M$. A finite cover by the smaller boxes of step 4.1 meets only finitely many boundary leaves, since each box contains exactly one boundary plaque. Each such leaf is open in the boundary and its complement is the union of the other open leaves, so it is also closed there. It is compact and has its intrinsic leaf topology: each boundary chart contains just its own local plaque and supplies the same coordinate neighborhoods as its leaf atlas. Thus the boundary is a finite union of compact leaves including $L$. Its negative half-boxes are outside the closure, so $W\mathrm{\ne }M$; its boundary is nonempty and $W$ is compact.

Every boundary leaf avoids closed transversals. Orient a hypothetical transverse circle positively; at any meeting with $\mathrm{\partial }{N}_L$, step 4.1 makes its crossing an entry into $N_L$. Positive forward invariance forbids any exit. Its transverse boundary meetings are isolated and finite by compactness, so periodicity would require an exit after an entry, a contradiction. If the foliation is taut, this argument rules out a nonempty boundary for any nonempty $N_L$. Reachability is nonempty and open; empty boundary makes it also closed. Connectedness therefore gives $N_L$ equal to its ambient component. Conversely that equality includes $L$, so steps 2.1–3.1 make every leaf met by a closed transversal. This proves the componentwise tautness criterion and the asserted boundary-leaf property.

By [F6], the region constructed in steps 4.1–6.1 satisfies the defining conditions of a dead-end component. The strict accessible-region claim follows from steps 4.1–6.1, and the openness, saturation and return claims from steps 1.1–3.1. No compactness of an intrinsically noncompact leaf or compact closure of an arbitrary mutual-accessibility class was assumed. The finite families and finite cover arguments use no full Axiom of Choice; the one generic-parameter argument inherits only the declared countable choice.