A nonseparating incompressible longitudinal surface in a fibered exterior is a fiber

Use [F2] to take a neat representative, preserving boundary and incompressibility. Nonseparation is preserved by its ambient topological extension. A short oriented transverse segment through $S$ closes through its connected complement to a loop intersecting $S$ once. Thus the intersection-dual cohomology class of $S$ is primitive. By [F1], $[S]=\pm [F]$ in $H_2(E_K,\mathrm{\partial }{E}_K;\mathbb{Z})$. Every loop in $S$ may be represented in its interior and pushed slightly into its two-sided normal product, so its intersection with $S$ is zero. Its value under the fiber's meridian homomorphism is consequently zero. Therefore the inclusion lifts to the infinite cyclic fiber cover ${\tilde{E}}_K=F\times \mathbb{R}$. The lift is an embedding, since equality of two lifted image points would imply equality of their projected points on the embedded $S$.

Align the finitely many longitude boundary curves by [F3] with distinct fiber-boundary levels in the torus, extending across its collar. In the infinite cyclic cover their lifts are horizontal circles in $\mathrm{\partial }F\times \mathbb{R}$. Straighten the neat surface's smaller boundary collars to the product collars using their simultaneous half-space coordinates, fixed on the boundary curves. The projection of the lifted inclusion is now a proper map $p:(S,\mathrm{\partial }S)\to (F,\mathrm{\partial }F)$ equal to a product near boundary; every boundary restriction is a diffeomorphism. Its fundamental-group map is injective: the lifted inclusion is injective on fundamental groups by [F2] and covering injection, and $F\times \mathbb{R}\to F$ is a homotopy equivalence. The relative fundamental class of $F\times \{t\}$ generates $H_2(F\times \mathbb{R},\mathrm{\partial }F\times \mathbb{R})$ and pushes to $[F]$ downstairs. Consequently $[S]=\pm [F]$ from step 1.1 makes the relative degree of $p$ equal to $\pm 1$.

Give the compact smooth surfaces the finite triangulations of [F4], choosing matched boundary subdivisions through the actual boundary diffeomorphisms. Here is the boundary-fixed PL approximation, rather than an invocation of a relative conclusion absent from [F4]. Realize the target triangulation as a subcomplex of the simplex on its vertices and barycentrically subdivide that simplex. The subdivided target is a full subcomplex. On the open neighborhood $N$ where the total barycentric weight of its vertices is positive, normalize those weights and discard the other weights; this defines a continuous retraction $r:N\to F$ fixing $F$. Triangulate $S$ retaining a smaller product collar on which $p$ is PL. With sufficiently small simplices, vertex interpolation of $p$ in the ambient simplex gives a PL map $q$ equal to $p$ on that collar, and every segment from $p(z)$ to $q(z)$ lies in $N$, by compactness and uniform continuity. Applying $r$ to these segments is a homotopy fixed on the collar. Subdivide the source by the finite polyhedral inverse images under $q$ of the ambient simplices. On each resulting simplex, $rq$ takes values in the single face spanned by the target vertices of its ambient carrier. Interpolate its vertex values in that face to obtain a PL map $g$. Linear interpolation within the same face homotopes $rq$ to $g$; on the protected collar it is constant because $rq=p$ is already linear after subdivision. Thus $p$ is homotopic to $g$ relative to the boundary. Both homotopies are maps of pairs since the boundary is fixed. If ${\pi }_{1}S\mathrm{\ne }1$, apply the full actual classifier [F4]. Its annular-collapse alternative induces zero on relative $H_2$, contrary to the degree $\pm 1$ in step 2.1. Its finite covering alternative has absolute relative degree equal to its number of sheets, by summing the lifted oriented triangles. Thus it has one sheet and is a homeomorphism $h:S\to F$, homotopic to $p$ relative to the aligned boundary. If ${\pi }_{1}S=1$, [F5] makes $S$ a disk. Lift $p$ to the cover of $F$ for its trivial image subgroup. An infinite-sheeted cover has relative top homology zero: all coefficients of a finite two-cycle on adjacent oriented triangles agree, and connectedness forces a single coefficient on infinitely many triangles, which must vanish by finite support. A finite-sheeted cover pushes its fundamental class to its sheet number times $[F,\mathrm{\partial }F]$. Nonzero degree $\pm 1$ therefore forces this cover to have one sheet. Hence $F$ is simply connected and also a disk; its boundary map extends to a disk homeomorphism, homotopic to $p$ relative boundary by convex interpolation in disk coordinates. In either case $S$ has one boundary component. The height coordinate of its lifted inclusion can now separately be homotoped linearly to its one constant boundary height, fixed there. Combine these homotopies in $F\times \mathbb{R}$ and project to get an actual homotopy of the parametrized inclusion of $S$ to the corresponding fiber, relative to the aligned boundary. This asserts a homotopy of maps, not a projection of an arbitrary embedding isotopy.

The homeomorphism and actual boundary-relative homotopy in step 3.1 meet [F6]. Use [F7] on the pair cut along its transverse smooth surface faces and protected product collars, matching paired face subdivisions before regluing; this gives compatible finite structures retaining the already matched boundary triangulations. That theorem constructs an empty embedded product patch in the actual cut fiber product, verifies that the patch meets only one fiber face so embeds downstairs, and reduces the finite intersection system until the patch is the whole surface. Hence its ambient boundary-relative isotopy carries $S$ to the original marked fiber $F$. Restore the preliminary boundary-torus alignment and neatification if necessary. This proves both the isotopy assertion and its relative aligned-boundary refinement under the authorized AC assumptions.