doc(periodic): update final overlap route gap (#3272)

Co-authored-by: Sirui Lu <texra-ai@outlook.com>

Author: LionSR

docs/paper-gaps/1708_periodic_overlap_route_alignment.tex

@@ -25,7 +25,7 @@ \section{Scope}
 \leanid{Papers/1708.00029/main.tex}. Paper-level umbrella:
 \href{https://github.com/LionSR/TNLean/issues/619}{issue \#619}; proposition-level
 subtracking: \href{https://github.com/LionSR/TNLean/issues/81}{issue \#81};
-the remaining Case-3 contraction and phase-assembly obligation is tracked by
+the remaining Case-3 contraction and phase construction is tracked by
 \href{https://github.com/LionSR/TNLean/issues/873}{issue \#873}.}
 
 The source proposition is \emph{equal-or-orthogonal-generalized}.\footnote{Stated
@@ -121,7 +121,7 @@ \section{Sector non-repetition via the blocked fixed-point structure}
 \leanid{sectorBlocks_not_gaugePhaseEquiv_of_ne}). With this hypothesis and the
 corner-isometry data, the spectral proof is now formalized.
 
-\section{Sector-match case: propagation and the phase assembly}
+\section{Sector-match case: propagation and the phase construction}
 
 \textbf{Source.}\footnote{\cite{DeLasCuevas2017Irreducible}, Appendix~A,
 lines 961--1117; the initial blocked equation \emph{eq:Nm} appears at
@@ -149,12 +149,14 @@ \section{Sector-match case: propagation and the phase assembly}
 \leanid{periodicOverlap_gaugeEquiv_of_sector_match} in \leanid{Case3.lean}.}
 The statements track this two-stage structure: the $T^l$ + Theorem~2.10
 staircase, followed by the $\Omega_u$ contraction and the
-$\kappa/\theta/\phi$ phase assembly. The top-level theorem now invokes these
-assembly lemmas and is proved modulo the two remaining leaf obligations. The
+$\kappa/\theta/\phi$ phase construction. The top-level theorem now invokes these
+component lemmas and is proved modulo the single remaining leaf
+\leanid{repeatedBlocks_of_blockedSectorGaugePhase}. The
 docstrings have been realigned to cite the source equation labels and line
 ranges (replacing earlier published-version labels such as ``A.8'' and
 ``A.14--A.18'' that do not occur in the local source), and the
-$\kappa/\theta/\phi$ phase assembly is now stated explicitly as load-bearing.
+$\kappa/\theta/\phi$ phase construction is now stated explicitly as
+load-bearing.
 
 \textbf{Formalized single-site inputs.} The single-site off-diagonal
 decomposition is now formalized from the cyclic adjoint-shift
@@ -197,20 +199,29 @@ \section{Sector-match case: propagation and the phase assembly}
 inverse cyclic indexing convention.
 
 \textbf{Remaining Case-3 input.} After these single-site inputs, the open
-Case-3 leaf is the contraction and phase-assembly step:
+Case-3 leaf is the contraction and gauge construction:
 \begin{itemize}
-  \item \emph{Per-sector corner unitaries}: upgrading the compression LinearEquiv
-    $\varphi_u$ to a multiplicative $\ast$-isomorphism with a unitary intertwiner
-    $U_v=P_uU_vQ_v$ on $\mathrm{Fin}\,D$ (\emph{eq:Cvprop}); and the $m$-factor
-    cyclic $\Omega_u$-contraction with the $\eta$ bookkeeping (the two-site
-    \leanid{tensor_proportional} is its $m=2$ shadow) plus the $\kappa/\theta/\phi$
-    telescoping into the global unitary $U=\sum_u e^{i\phi_{u+q}}P_uU_{u+q}Q_{u+q}$.
+  \item The $m$-factor cyclic $\Omega_u$-contraction with the $\eta$ bookkeeping:
+    starting from the common right inverses for the injective tensors $F_u$,
+    contract the cyclic product in lines~1041--1068 to obtain the uniform
+    product-tensor identity \emph{eq:resultprop}.
+  \item The final normalization and gauge construction: use the proved scalar
+    extraction theorem to obtain $\kappa_v$ with $\prod_v\kappa_v=1$, prove
+    $|\kappa_v|=1$ from the left-canonical normalization, apply the finite-cycle
+    coboundary lemma to write $\kappa_v=e^{i(\phi_v-\phi_{v+1})}$, and assemble
+    the global unitary
+    $U=\sum_u e^{i\phi_{u+q}}P_uU_{u+q}Q_{u+q}$.
 \end{itemize}
-This is the remaining obligation for the repeated-blocks assembly
+This is the remaining obligation for the repeated-blocks
 theorem.\footnote{Formal declaration:
-\leanid{repeatedBlocks_of_blockedSectorGaugePhase}.} The one-step
-transport theorem is closed by the single-site overlap theorem above together
-with the overlap-to-gauge theorem and the proved sector primitivity.\footnote{
+\leanid{repeatedBlocks_of_blockedSectorGaugePhase}.} The tensor-product scalar
+extraction and product-one normalization have already been isolated in
+\leanid{PiTensorProductPhase.exists_kappa_of_piTensorProduct_eq_smul} and
+\leanid{PiTensorProductPhase.exists_kappa_product_one_of_piTensorProduct_eq_root_smul};
+the finite-cycle phase choice is isolated in
+\leanid{exists_fin_complex_unit_cyclic_coboundary_shift_of_prod_eq_one}. The
+one-step transport theorem is closed by the single-site overlap theorem above
+together with the overlap-to-gauge theorem and the proved sector primitivity.\footnote{
 The formal declarations are
 \leanid{sectorGaugePhaseEquiv_succ_of_cyclicTransport} and
 \leanid{gaugePhaseEquiv_of_overlap_norm_tendsto_one_of_irreducible_TP}.}