\begin{warningpage}
We have extensively audited this manuscript using large language models, including adversarial reviews by multiple models. However, the proof is too complex for Lean formalization at the present time, and it has not yet undergone verification by a human expert.
\end{warningpage}