diff --git a/symmetric_tensor_categories_fiber_v2.txt b/symmetric_tensor_categories_fiber_v2.txt
index 546874d..b0e8b6f 100644
--- a/symmetric_tensor_categories_fiber_v2.txt
+++ b/symmetric_tensor_categories_fiber_v2.txt
@@ -44,7 +44,7 @@
 \providecommand{\sVec}{}\renewcommand{\sVec}{\operatorname{sVec}}
 \providecommand{\Vec}{}\renewcommand{\Vec}{\operatorname{Vec}}
 \setlist{nosep}
-\setlength{\emergencystretch}{1em}
+\setlength{\emergencystretch}{4em}
 
 \title{Fiber functors for finite symmetric tensor categories\\
        in positive characteristic}
@@ -181,10 +181,12 @@ implies the finite part of all the consequences we discuss.
 
 \subsection*{Proof outline}
 
-We build a chain of $n$ copies of a functor $\Phi_n$, each time
-adding a fresh Verlinde factor while forcing the original
-$\mathcal C$ factor to shrink into its small Frobenius-exact part.
-The four ingredients are:
+We iteratively apply a semilinear higher Frobenius functor $\Phi$,
+each application adding one fresh Verlinde factor while forcing
+the original $\mathcal C$ factor to shrink into its Frobenius-exact
+subcategory.  After at most $N$ iterations, where $N$ is the number
+of simple objects of $\mathcal C$, all first components land in the
+Serre closure of that subcategory.  The essential ingredients are:
 
 \begin{enumerate}[label=\textbf{Step \arabic*.},ref=step:\arabic*]
   \item \textbf{Restricted tilting modulo a Steinberg module.}
@@ -216,10 +218,11 @@ The four ingredients are:
         Frobenius-exact tensor subcategory $\mathcal C_{\mathrm{ex}}$.
 \end{enumerate}
 
-Four steps then finish: replace the Serre-closure factor by a fixed
-small Verlinde level (via Etingof--Ostrik for $p>2$, Etingof--Gelaki
-for $p=2$), combine all factors into one big tensor product, kill
-the scalar twist, and observe that the resulting functor is faithful.
+After these four steps, a few more tasks finish the argument:
+replace the Serre-closure factor by a fixed small Verlinde level
+(via Etingof--Ostrik for $p>2$, Etingof--Gelaki for $p=2$); combine
+all factors into one big tensor product and remove the total scalar
+twist; and verify that the resulting functor is faithful.
 
 Sections \ref{sec:groundwork}--\ref{sec:serre-finish} carry out the
 four steps.  Section \ref{sec:consequences} records the standard
@@ -727,10 +730,12 @@ $\Phi(af) = a^q\Phi(f)$ for scalars $a\in k$.
 \end{lemma}
 
 \begin{proof}
-The monoidal constraint comes from the $E$-equivariant reordering
-$(X\otimes Y)^{\otimes q}\cong X^{\otimes q}\otimes Y^{\otimes q}$
+The monoidal constraint is the $E$-equivariant reordering
+\[
+  (X\otimes Y)^{\otimes q}\cong X^{\otimes q}\otimes Y^{\otimes q}
+\]
 with the diagonal action on the right, applied through the internal
-monoidal extension of Coulembier--Flake (2026, Section 3.3.2).
+monoidal extension of Coulembier--\hspace{0pt}Flake (2026, Section 3.3.2).
 Additivity can be checked directly: in the expansion of
 $(X\oplus Y)^{\otimes q}$, a nonconstant colouring of tensor
 positions has a proper stabiliser in $E$, so the sum over its