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

[LionSR]

Motivation

• The declaration MPSTensor.peripheralEqualCaseZGaugeOfSameMPV_of_periodicEqualCaseFT misleadingly suggests the full PeripheralEqualCaseZGaugeOfSameMPV conclusion rather than the narrower Z-gauge equivalence extracted as an intermediate step from the periodic equal-case Fundamental Theorem. Continues the discharge plan in MPS/Periodic: canonicalization hypotheses for the unconditional Thm. 4.1 #664 (canonicalization hypotheses for the unconditional Thm. 4.1).
• Source: arXiv:1708.00029 §4.1, periodic equal-case Fundamental Theorem.

Description

• Renamed MPSTensor.peripheralEqualCaseZGaugeOfSameMPV_of_periodicEqualCaseFT to MPSTensor.zGaugeEquiv_of_periodicEqualCaseFT_of_irreducibleForm in TNLean/MPS/Periodic/Symmetry/Theorem41Forward.lean.
• Updated the Lean docstring to state explicitly that the theorem assumes irreducible form for the blocked root (blockTensor A p) and does not prove the full PeripheralEqualCaseZGaugeOfSameMPV hypothesis.
• Updated the blueprint theorem label to thm:zgauge_equiv_periodicFT_irreducible_form and revised the corresponding prose in blueprint/src/chapter/ch22_periodic_ft.tex to make the irreducible-form restriction visible to readers.
• Proof body is unchanged (hFT hC hBlock hSame).
• No compatibility alias is provided. The old name misleadingly encoded the full peripheral equal-case Z-gauge conclusion as the theorem name, obscuring the narrower scope (see docs/CONTRIBUTING.md Section Mathematical-language renames).

Testing

• lake build TNLean.MPS.Periodic.Symmetry.Theorem41Forward -q --log-level=info
• lake build TNLean -q --log-level=info
• lake exe checkdecls blueprint/lean_decls
• cd blueprint && leanblueprint checkdecls
• Blueprint sync and prose review scripts pass (blueprint_lean_sync.py, check_reader_facing_prose.py).
• Builds report only pre-existing warnings (known unfinished periodic Case-3 statement and style warnings in imported files).

---

Addresses #664

---

Note

Low Risk
Documentation and naming only; mathematical content and proof term are unchanged, with blueprint Lean decl sync updated accordingly.

Overview
Renames the Lean theorem from peripheralEqualCaseZGaugeOfSameMPV_of_periodicEqualCaseFT to zGaugeEquiv_of_periodicEqualCaseFT_of_irreducibleForm so the name matches what it actually proves (blocked Z-gauge equivalence under explicit irreducible-form hypotheses), not the broader PeripheralEqualCaseZGaugeOfSameMPV Prop.

The docstring now states that this step only applies the periodic equal-case FT and does not discharge the full peripheral Z-gauge hypothesis, which omits irreducible form on the blocked root; remaining work is irreducible-form for blockTensor A p and blocked-to-root phase distribution.

Blueprint (ch22_periodic_ft.tex): theorem label thm:zgauge_equiv_periodicFT_irreducible_form, title/prose aligned with the narrower scope; \lean link updated. Proof unchanged (hFT hC hBlock hSame); no compatibility alias for the old name.

^{Reviewed by Cursor Bugbot for commit ed40137. Bugbot is set up for automated code reviews on this repo. Configure here.}

[claude]

PR cleanup

Field	Before	After
Title	refactor(MPS/Periodic): rename scoped Z-gauge extraction	unchanged (already compliant)
Body	## Summary / ## Checks non-template structure	restructured to ### Motivation / ### Description / ### Testing + Addresses #664 footer; Cursor Bugbot block preserved verbatim
Labels	(none)	added: formalization, 1708.00029, symmetry-SPT, follow-up, auto-fix-claude (copied from issue #664)
Issue	linked to #664	comment posted on #664

Conventions: CONTRIBUTING.md

[claude]

Review summary

0 equivalence mismatches, 0 stale \leanok, 1 prose issue

Category A — Blueprint ↔ Lean equivalence ✅

The rename is clean end to end.

• \lean{MPSTensor.zGaugeEquiv_of_periodicEqualCaseFT_of_irreducibleForm} resolves to the correct declaration.
• All four hypotheses in the blueprint ("periodic equal-case FT at the blocked dimension", "$C$ in irreducible form II", "$A^{[p]}$ in irreducible form II", "same MPV family") are present in the Lean signature as hFT, hC, hBlock, hSame, with matching strength.
• The conclusion ($\exists m \ge 1$ and $\mathbb Z_m$-gauge equivalence) matches the Lean return type exactly.
• The \leanok on the statement is valid: no sorry in the proof body (hFT hC hBlock hSame).
• No stale references to the old label thm:peripheral_equalcase_zgauge_sameMPV_of_periodicFT or old Lean name remain in the blueprint or source tree.
• The \uses entries accurately reflect the Lean proof's dependencies.

Category B — Prose quality 🟡 (1 issue, see inline)

The scope note about what this theorem does not prove was previously a LaTeX comment and is now displayed as prose inside the theorem statement body. Per docs/prose_style.md, maintainer-facing restriction notes belong in LaTeX comments, not in displayed mathematical prose. See the inline comment for the suggested fix.

[claude]

Category B — scope note displayed as theorem body prose

The old version kept this remark as a LaTeX comment (% Scope note: ...). The new version promotes it to displayed prose inside the \begin{theorem} block:

    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.

Per docs/prose_style.md §"Source-faithful terminology and formulas":

a maintainer-facing note records the extra hypothesis, missing implication, or auxiliary reformulation. In the blueprint this note should be a LaTeX comment, not displayed mathematical prose.

This note tells the reader what the theorem does not prove relative to another Lean definition — exactly the kind of auxiliary restriction that must stay in a comment. Move it back:

    % Scope restriction: this applies the periodic FT with an explicit
    % irreducible-form assumption on $A^{[p]}$; it does not follow from
    % equality of MPV families alone.

The corresponding remark in the Lean docstring (which the style guide explicitly allows for maintainer-facing notes) can stay as is.

[claude]

Review: refactor(MPS/Periodic): rename scoped Z-gauge extraction — APPROVE

This is a documentation-and-naming-only PR. I verified it against all 🔴/🟡 categories and found no blocking or change-requiring issues.

What was checked

Proof integrity (🔴) — clean. No new sorry/axiom/native_decide etc. The proof body of the renamed theorem is unchanged: hFT hC hBlock hSame.

Proof correctness (🔴) — verified. The renamed theorem MPSTensor.zGaugeEquiv_of_periodicEqualCaseFT_of_irreducibleForm (TNLean/MPS/Periodic/Symmetry/Theorem41Forward.lean:378) type-checks as before:

• PeriodicEqualCaseFT (blockPhysDim d p) D unfolds (EqualCaseFTHyp.lean:56–60) to ∀ {X Y}, IsIrreducibleForm X → IsIrreducibleForm Y → SameMPV X Y → ∃ m, 0 < m ∧ ZGaugeEquiv m X Y.
• Applying hFT to hC : IsIrreducibleForm C, hBlock : IsIrreducibleForm (blockTensor A p), hSame : SameMPV C (blockTensor A p) instantiates X := C, Y := blockTensor A p, yielding exactly the stated conclusion ∃ m, 0 < m ∧ ZGaugeEquiv m C (blockTensor A p).

Naming / faithfulness — the rename is an improvement. The new name zGaugeEquiv_of_periodicEqualCaseFT_of_irreducibleForm reflects the actual hypothesis set (irreducible form of both C and blockTensor A p), whereas the old peripheralEqualCaseZGaugeOfSameMPV_of_periodicEqualCaseFT suggested it discharged the broader PeripheralEqualCaseZGaugeOfSameMPV Prop (which does not assume irreducible form for the blocked root). Omitting a @[deprecated] alias is correct here per docs/CONTRIBUTING.md §Mathematical-language renames, since the old name encoded a misleading scope; the reason is stated in the PR body. The updated docstring now states the irreducible-form restriction explicitly.

Consistency — no dangling references. The blueprint label was renamed thm:peripheral_equalcase_zgauge_sameMPV_of_periodicFT → thm:zgauge_equiv_periodicFT_irreducible_form with the matching \lean{...}. No remaining references to the old theorem or label exist in the tracked tree (the only residual hits are in the untracked .trusted-actions/ snapshot, which is not part of this PR).

Type safety / performance / modularity / paper-gap notes — N/A. No type-level, performance, or structural changes; no docs/paper-gaps/ files touched.

Advisory (ℹ️, non-blocking)

The docstring header still reads "Scope-restricted blocked Z-gauge extraction…" but does not point to a docs/paper-gaps/*.tex note as the lighter-weight **Scope restriction (...):** marker convention recommends. This is pre-existing (not introduced by this PR) and outside the PR's stated scope (#664), so it does not block merge — worth a follow-up if a paper-gap note for this restriction is ever written.

Verdict: APPROVE. Minimal, well-scoped rename that improves naming faithfulness with no proof or correctness impact.

[claude]

Review: APPROVE ✅

All categories pass. This is a clean naming/documentation fix that correctly disambiguates a scope-restricted theorem from the broader hypothesis whose name it formerly carried.

Summary

• Old name: peripheralEqualCaseZGaugeOfSameMPV_of_periodicEqualCaseFT misleadingly suggested the theorem proves PeripheralEqualCaseZGaugeOfSameMPV (which only requires IsIrreducibleForm C).
• New name: zGaugeEquiv_of_periodicEqualCaseFT_of_irreducibleForm correctly reflects the actual hypotheses (periodic equal-case FT + irreducible form on both C and blockTensor A p) and the conclusion (Z-gauge equivalence).
• The proof body is unchanged (hFT hC hBlock hSame). No consumers broken — the theorem is not referenced elsewhere in TNLean/.
• The blueprint changes align the label, \lean{} tag, and prose with the renamed Lean theorem, and promote the scope note from a LaTeX comment to visible text.
• The \leanok remains appropriate: the Lean statement faithfully matches the updated blueprint statement, which now explicitly states the irreducible-form assumption on A^{[p]}.

No issues found in any review category.

[claude]

Review fix applied

Addressed thread: blueprint/src/chapter/ch22_periodic_ft.tex — Category B: scope note displayed as theorem body prose.

The scope restriction on Theorem thm:zgauge_equiv_periodicFT_irreducible_form (Lean: MPSTensor.zGaugeEquiv_of_periodicEqualCaseFT_of_irreducibleForm) was promoted to displayed prose inside the theorem block in this PR. Per docs/prose_style.md ("Source-faithful terminology and formulas"), a maintainer-facing note recording an extra hypothesis must be a LaTeX comment, not displayed mathematical prose. The note tells the reader what the theorem does not prove relative to the PeripheralEqualCaseZGaugeOfSameMPV hypothesis — exactly the auxiliary-restriction case the style guide keeps in a comment.

Reverted to:

    % 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.

The visible theorem statement (hypotheses + conclusion) is unchanged and still faithfully matches the renamed Lean theorem, so \leanok remains appropriate.

Scope: blueprint LaTeX comment only — no Lean code changed, so no lake build required and no Mathlib Audit applies. Committed in ed40137.