\section{Two limits of perturbative reasoning}\label{app:perturbative}

\subsection{An exact leading-soft model}
Assume independent soft emissions with intensity $b\,d\omega/\omega$, $b\ge0$, an infrared cutoff $\lambda$, detector resolution $E$ and hard scale $\Lambda$, with $0<\lambda<E<\Lambda$. Assume also the virtual factor $\exp[-b\ln(\Lambda/\lambda)]$. Summing any number of unobserved emissions below $E$ gives
\begin{align}
P_\lambda&=e^{-b\ln(\Lambda/\lambda)}\sum_{n=0}^{\infty}
\frac{[b\ln(E/\lambda)]^n}{n!}\nonumber\\
&=e^{-b\ln(\Lambda/\lambda)+b\ln(E/\lambda)}
=e^{-b\ln(\Lambda/E)}.
\end{align}
The series is absolutely convergent and the last expression is independent of $\lambda$. This is a self-contained cancellation in the independent-emission model. It assumes soft factorisation and the virtual factor; it does not prove either for every string-field-theory diagram, include subleading emissions, or construct the general four-dimensional observable. The missing physical and analytic steps must not be concealed by the elementary exponential identity. The finite-exponent cancellation is separately checked in Lean.

\subsection{Formal unitarity does not determine a completion}
\begin{proposition}
There exist two smooth scalar amplitudes with the same Taylor series at zero coupling such that one is unitary and the other is not for every positive coupling.
\end{proposition}
\begin{proof}
Take $S_0(g)=1$ and $S_1(g)=1+f(g)$, where $f(0)=0$ and $f(g)=e^{-1/g^2}$ for $g\ne0$. For every integer $N\ge0$, choose an integer $m$ with $2m>N$. Since $e^t\ge t^m/m!$ for $t>0$,
\[
0\le |g|^{-N}f(g)\le m!|g|^{2m-N}\longrightarrow0.
\]
Each derivative of $f$ away from zero is a finite linear combination of powers of $g^{-1}$ times $f(g)$. Induction using the displayed bound extends every derivative continuously to zero with value zero. Thus both amplitudes have the same Taylor series, the constant $1$. It satisfies the formal scalar unitarity identity to every order, whereas $S_1(g)>1$ gives $|S_1(g)|^2>1$ for $g>0$.
\end{proof}
This is a counterexample to a general inference from a perturbative series to an exact completion, not a counterexample to Sen's perturbative theorem. The flat-function smoothness argument is proved here in ordinary analysis and is not part of the finite Lean certificate. A nonperturbative completion needs additional input such as a summation prescription, analytic class, boundary conditions or an independently constructed theory.