diff --git a/mutually_unbiased_bases_dim6_v2.txt b/mutually_unbiased_bases_dim6_v2.txt
index c9604fc..5e0611b 100644
--- a/mutually_unbiased_bases_dim6_v2.txt
+++ b/mutually_unbiased_bases_dim6_v2.txt
@@ -892,8 +892,10 @@ A feasible completion is a unit-modulus matrix
 \]
 with first row and first column all one. Its seed displacements, in
 radians, are
-\(s=(s_a,s_{b_0},\ldots,s_{b_3},s_{c_0},\ldots,s_{c_3})\in\R^9\);
-the varied entries are
+\[
+ s=(s_a,s_{b_0},\ldots,s_{b_3},s_{c_0},\ldots,s_{c_3})\in\R^9;
+\]
+and the varied entries are
 $a e^{is_a}$, $b_j e^{is_{b_j}}$, $c_i e^{is_{c_i}}$. The shared entry
 appears exactly once in $s$. In zero-based row-major phase indexing
 these positions are
@@ -2164,7 +2166,9 @@ Suppose two Root records $(P,r_P)$, $(Q,r_Q)$ satisfy
 \]
 for a certified upper distance $d_{PQ}$. Then the union
 $\mathcal S(P,r_P)\cup\mathcal S(Q,r_Q)$ is contained in
-$\mathcal S(P,\max\{r_P,d_{PQ}+r_Q+\text{allowance}\})$.
+\[
+ \mathcal S\bigl(P,\ \max\{r_P,\ d_{PQ}+r_Q+\text{allowance}\}\bigr).
+\]
 \end{lemma}
 
 \begin{proof}
@@ -3375,19 +3379,10 @@ unsuccessful proposals of a local Root cover that are followed by
 subdivision. A0 reported such a diagnostic in this run; its terminal
 unresolved count was nevertheless zero.
 
-The finite bounds of the control flow are as follows. Before filtering,
-the nondecreasing five-bin lists for the seed cover number at most
-$\binom{116}{5}=160{,}389{,}488$; for any fixed shared bin the four
-ordered tail bins number at most
-$\binom{115}{4}=6{,}913{,}340$. The former bound is below the signed
-32-bit limit. Pair traversals in the cover use range loops and 64-bit
-counters; all bin differences lie between $-111$ and $111$, and their
-nine-coordinate square sum is at most $9\cdot 111^2$. A retains
-nonfinal unitary grid lists only through grid~$32$; grid~$64$ has at
-most $64^4/8=2{,}097{,}152$ cell tests per seed. Further tests are
-bounded by the $1{,}000{,}000$ extra-node cap, and the deepest grid is
-$512$. Reaching the cap or the deepest grid without a certificate
-records an unresolved seed.
+The finite bounds governing this control flow --- the bin counts, the
+range of stored differences, the grid~$64$ cell-test count, and the
+extra-node and deepest-grid caps --- are stated and checked at the end
+of Section~\ref{sec:completion}.
 
 Reaching the C-stage bin cap of $2{,}000{,}000$ retained bins, exceeding
 the cluster center count of $2048$, or exhausting the graph work cap
@@ -3530,28 +3525,13 @@ would require a fresh execution of the affected stage, but the logical
 structure of the certificate is unchanged.
 
 The theorem and its proof complete the computer-assisted upper bound.
-For the record we restate the main conclusion:
-
-\begin{theorem}[Main]\label{thm:main-final}
-Under the arithmetic and compiler conditions of
-Appendix~\ref{sec:rounding}, the fresh complete execution documented in
-Section~\ref{execute:observed} certifies that there are no four pairwise
-mutually unbiased orthonormal bases in $\C^6$. Consequently $N(6)=3$,
-combining Theorem~\ref{execute:finite-theorem} (upper bound) with
-Lemma~\ref{lem:three-mub-six} (three exist).
-\end{theorem}
-
-The theorem does not modify earlier uses of Theorem~\ref{thm:main}; it
-shows that the two statements of the computer-assisted result are the
-same.
-
 
 % =====================================================================
 \section{Conclusion of the proof}
 \label{sec:conclusion}
 % =====================================================================
 
-We have now completed the proof of Theorem~\ref{thm:main-final}. The
+We have now completed the proof of Theorem~\ref{thm:main}. The
 overall argument is the following chain of strictly finer covers, each
 preserving every exact candidate solution.