refactor(MPS/Periodic): rename scoped Z-gauge extraction (#3386)

* refactor(MPS/Periodic): rename scoped Z-gauge extraction

* [claude-review-fix] doc(MPS/Periodic): move scope note back to LaTeX comment

Per docs/prose_style.md, maintainer-facing scope notes recording an extra
hypothesis belong in a LaTeX comment, not displayed theorem-body prose.
Reverts the irreducible-form scope restriction on thm:zgauge_equiv_periodicFT_irreducible_form to a comment.

Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>

---------

Co-authored-by: Sirui Lu <texra-ai@outlook.com>
Co-authored-by: claude[bot] <41898282+claude[bot]@users.noreply.github.com>
Co-authored-by: Claude Opus 4.8 <noreply@anthropic.com>

Author: 4 people

TNLean/MPS/Periodic/Symmetry/Theorem41Forward.lean

@@ -369,10 +369,13 @@ already known to be in irreducible form. The irreducible-form hypothesis for
 the \(p\)-blocked root is an explicit input here; it is not obtained from
 equality of MPV families.
 
-This theorem is therefore only the equal-case FT application step. The remaining
-canonicalization problem is to prove that the blocked root appearing in the
-refinement argument is in irreducible form. -/
-theorem peripheralEqualCaseZGaugeOfSameMPV_of_periodicEqualCaseFT
+This theorem is therefore only the equal-case FT application step. It does not
+prove the full `PeripheralEqualCaseZGaugeOfSameMPV` hypothesis, since that
+hypothesis does not assume irreducible form for the blocked root. The remaining
+canonicalization work is to prove the missing irreducible-form input for the
+blocked root, and then to distribute the resulting blocked `Z`-phase back to a
+left-canonical root. -/
+theorem zGaugeEquiv_of_periodicEqualCaseFT_of_irreducibleForm
     (p : ℕ) (hFT : PeriodicEqualCaseFT (blockPhysDim d p) D)
     {A : MPSTensor d D} {C : MPSTensor (blockPhysDim d p) D}
     (hC : IsIrreducibleForm C)

blueprint/src/chapter/ch22_periodic_ft.tex

@@ -1979,9 +1979,9 @@ \section{Refinement and divisibility}\label{sec:periodic_refinement}
     between $C$ and $A^{[p]}$.
 \end{definition}
 
-\begin{theorem}[Blocked equal-case Z-gauge extraction from the periodic theorem]
-    \label{thm:peripheral_equalcase_zgauge_sameMPV_of_periodicFT}
-    \lean{MPSTensor.peripheralEqualCaseZGaugeOfSameMPV_of_periodicEqualCaseFT}
+\begin{theorem}[Z-gauge equivalence from the periodic theorem]
+    \label{thm:zgauge_equiv_periodicFT_irreducible_form}
+    \lean{MPSTensor.zGaugeEquiv_of_periodicEqualCaseFT_of_irreducibleForm}
     \leanok
     \uses{thm:periodic_ft, def:irreducible_form, def:blocked_tensor,
         def:same_mpv, def:z_gauge_equiv}
@@ -1990,7 +1990,7 @@ \section{Refinement and divisibility}\label{sec:periodic_refinement}
     both in irreducible form~II, and suppose that they have the same MPV family.
     Then there exists an integer $m \ge 1$ and a $\mathbb Z_m$-gauge equivalence
     between $C$ and $A^{[p]}$.
-    % Scope note: this is only the equal-case application of the periodic
+    % Scope restriction: this is only the equal-case application of the periodic
     % Fundamental Theorem; the irreducible-form hypothesis on $A^{[p]}$ is an
     % explicit assumption, not a consequence of equality of MPV families.
 \end{theorem}