Limitwise-nullhomotopy predicate on based loops

Assume Countable Choice ${\mathrm{A}\mathrm{C}}_{\omega }$. Let $F$ be a transversely oriented codimension-one foliation, $L$ a leaf, $x\in L$, and $j$ one of its two sides. For a based loop $f:S^1\to L$ whose class belongs to $N_j(L,x)$, and for a chosen sufficiently short normal fence on side $j$, define the representative-level predicate $Q_j(f)$ to hold when every sufficiently small positive normal displacement $f_{ϵ}$ is null- homotopic in its leaf. At this stage $Q_j$ is a predicate on a specified loop and fence; no representative-independence is part of this definition.

For clarity, a displacement is obtained by starting at a chosen positive point of the base transversal and continuing the loop plaque by plaque through a finite chart subdivision. Within each chart its transverse label is held fixed; the fence specifies the nearby endpoint in that plaque. Since $[f]\in N_j$, the return map is the identity on a sufficiently short interval on side j, so these displacements are closed loops. The quantifier means: there exists ε₀>0 such that every displacement with 0<ε<ε₀ is nullhomotopic in its own leaf. No uniform bound on the filling disks is part of the definition.