doc(MPS/Periodic): align Theorem 4.1 source prose

[LionSR]

Motivation

• The forward Theorem 4.1 section in TNLean/MPS/Periodic/Symmetry/Theorem41Forward.lean
  and blueprint/src/chapter/ch22_periodic_ft.tex used local "pullback/root hypothesis"
  language that diverges from the source terminology in arXiv:1708.00029, lines 735–810.
• Aligning the prose to the source paper is a prerequisite for the full unconditional
  formalization of Theorem 4.1 tracked in MPS/Periodic: canonicalization hypotheses for the unconditional Thm. 4.1 #664.
• The paper source (arXiv:1708.00029, §4.1) constructs the tensor $C$ from the refinement
  isometry $W$, applies a blocked $Z$-gauge step, and obtains $\widetilde{A}$ from scalars
  $c_{j,\alpha}$ (lines 765–810); these objects had no names in the existing prose.

Description

• Modified TNLean/MPS/Periodic/Symmetry/Theorem41Forward.lean and
  blueprint/src/chapter/ch22_periodic_ft.tex (prose only; no Lean statements or proofs
  are changed).
• Replaces "W-pullback", "blocked root / root hypothesis / reconstruction" language with
  source terminology: the tensor $C$ defined from the refinement isometry $W$, the
  $p$-blocked blockTensor A p, the blocked $Z$-gauge step, and the $\widetilde{A}$
  construction from scalars $c_{j,\alpha}$ (arXiv:1708.00029, lines 765–810).
• Docstrings for PeripheralEqualCase* and PRefinementCanonicalization updated to
  describe the two-step split explicitly rather than "blocked-to-root" language.

Testing

• lake build TNLean.MPS.Periodic.Symmetry.Theorem41Forward passed.
• lake build TNLean passed.
• python3 scripts/check_reader_facing_prose.py --root . --diff-base origin/main passed.
• python3 scripts/blueprint_lean_sync.py --root . --ci passed.
• lake exe checkdecls blueprint/lean_decls passed.

---

Refs #664

Note

Low Risk
Comment and blueprint text only; no executable Lean or proof logic changes.

Overview
Documentation-only alignment of the forward Theorem 4.1 narrative with arXiv:1708.00029 (lines 735–810). Lean theorem names, statements, and proofs are unchanged.

In Theorem41Forward.lean and ch22_periodic_ft.tex, local wording is updated in parallel: "W-pullback" → the refinement-isometry tensor (C), "blocked root / root hypothesis / reconstruction" → (p)-blocked blockTensor A p, the blocked (Z)-gauge step, and the paper's (\widetilde A) construction from (c_{j,\alpha}) (lines 765–810). Docstrings for PeripheralEqualCase* and PRefinementCanonicalization now describe that two-step split explicitly instead of "blocked-to-root" language.

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

---

Note

Low Risk
Comment and LaTeX blueprint text only; no executable Lean or proof logic changes.

Overview
Documentation-only update to the forward Theorem 4.1 narrative in Theorem41Forward.lean and ch22_periodic_ft.tex. No Lean theorem names, statements, or proofs change.

Prose is retitled and rewritten to match arXiv:1708.00029 (§4.1, lines 735–810): W-pullback language becomes the refinement-isometry tensor (C), and blocked root / root hypothesis / reconstruction becomes (p)-blocked blockTensor A p, the blocked (Z)-gauge step, and (\widetilde A) built from scalars (c_{j,\alpha}). Docstrings for PeripheralEqualCase* and PRefinementCanonicalization now spell out the two-step split (equal-case (Z)-gauge, then (\widetilde A) construction) instead of “blocked-to-root” wording.

The blueprint definition PeripheralEqualCaseRootFromZGauge gains an explicit note that the formal hypothesis records only transfer-map equality (\mathcal E_C = \mathcal E_{\widetilde A^{[p]}}), weaker than the source’s blocked-tensor identity (\widetilde A^{[p]} = C).

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

[claude]

PR cleanup

Field	Before	After
Title	`doc(MPS/Periodic): align Theorem 4.1 source prose`	unchanged
Body	flat prose with `Refs #664.` header	restructured into Motivation / Description / Testing sections; Cursor Bugbot note preserved; footer changed to `Addresses #664`
Labels	(none)	added: `formalization`, `1708.00029`, `symmetry-SPT`, `follow-up`, `auto-fix-claude`, `documentation`
Issue	linked to #664

Conventions: CONTRIBUTING.md

[claude]

Review: APPROVE ✅

PR #3390: doc(MPS/Periodic): align Theorem 4.1 source prose

Summary

This is a clean documentation-only PR (no Lean statements, proofs, or types changed). It aligns the prose in Theorem41Forward.lean and ch22_periodic_ft.tex with the source paper arXiv:1708.00029, lines 735–810, by replacing opaque local terminology ("pullback," "blocked root," "root hypothesis," "blocked-to-root reconstruction") with the source paper's language: tensor (C) defined from the refinement isometry (W), (p)-blocked tensor, construction of (\widetilde A) from the scalars (c_{j,\alpha}), etc. Each updated docstring and blueprint entry now carries precise line-range citations.

Findings by category

Category	Severity	Verdict
🔴 Proof integrity	Blocker	✅ PASS — no sorry, axiom, native_decide, or unsafeCast changes
🔴 Proof correctness	Blocker	✅ PASS — all theorem bodies, types, and proofs are untouched
🟡 Mathlib style	Requires changes	✅ PASS — docstrings follow Mathlib conventions
🔴 Type safety	Blocker	✅ PASS — no type changes
🟡 Performance	Requires changes	✅ PASS — no proof changes
🟡 Modularity & duplication	Requires changes	✅ PASS — no code changes
🟡 Documentation	Requires changes	✅ PASS — one ℹ️ advisory noted inline (see below)
🟡 Paper-gap notes	Requires changes	N/A — no paper-gap files changed

Advisory (ℹ️)

One inline comment notes that the newly added **Scope-restricted** marker on zGaugeEquiv_of_periodicEqualCaseFT_of_irreducibleForm (line 366 of Theorem41Forward.lean) does not include a reference to a docs/paper-gaps/ note, as required by the lighter-weight marker guidelines in CLAUDE.md. The scope restriction is already described in the docstring body; a standalone paper-gap note would make it formally tracked. This does not block approval.

Verdict

APPROVE. All 🔴 blocker and 🟡 required-change categories pass. The one inline comment is advisory only. The PR meaningfully improves mathematical fidelity to the source paper.

[claude]

Review: doc(MPS/Periodic): align Theorem 4.1 source prose

Verdict: APPROVE — documentation-only PR, mathematically faithful to the source.

Scope of the change

This PR touches only docstrings in TNLean/MPS/Periodic/Symmetry/Theorem41Forward.lean and prose in blueprint/src/chapter/ch22_periodic_ft.tex. No Lean theorem signatures, statements, or proofs are changed (confirmed by reading the full file: PeripheralEqualCaseZGaugeOfSameMPV, PeripheralEqualCaseRootFromZGauge, PeripheralEqualCasePeriodicFTOfSameMPV, PRefinementCanonicalization, and the thm_4_1_p_refinement_* theorems are byte-for-byte unchanged in their def/theorem bodies). The renamings are purely terminological: "$W$-pullback tensor" → "the tensor $C$ defined from $W$", "blocked root / root hypothesis / reconstruction" → "the $p$-blocked tensor blockTensor A p" and "the construction of $\widetilde A$".

Proof integrity (🔴): clean

No sorry/axiom/native_decide introduced; no proof terms altered. The conditional Prop-as-hypothesis structure (the load-bearing PeripheralEqualCase* hypotheses gating the unconditional Theorem 4.1) is preserved.

Mathematical faithfulness (🔴 proof-correctness / source comparison): verified against Papers/1708.00029/main.tex

I checked every construction the new prose names against the source proof of Theorem 4.1:

• C^{i_1,…,i_p} := ∑_i W^{(i_1,…,i_p),i} B^i — source line 742 (cited 735–743) ✓
• blocked $Z$-gauge step ZA^{(p)} = U C U^\dagger — source line 758 ✓
• A'^i_j = ∑_{u} d_{j,u} P_{j,u} A_j^i — source line 787 ✓
• A'^{(p)} = Z A^{(p)} and à = U^\dagger A' U — source line 808 ✓
• the scalars c_{j,α} are finite-order (c_{j,α}^{m_j/r_j}=1, source line 779), correctly described as the "finite-order $Z$-factor" ✓

The blueprint statement of thm:thm_4_1_p_refinement correctly remains conditional on the two construction hypotheses, and the source-comparison comment correctly states that arXiv:1708.00029 Theorem 4.1 (lines 728–731) asserts the equivalence with no extra hypotheses. The prose substitution is therefore faithful, not an over-claim.

Out of scope (per the workflow split)

Blueprint↔Lean \lean{}/\leanok/\uses{} sync and prose/AI-language quality are handled by the dedicated Blueprint Sync & Prose Review workflow; I did not assess those here. No docs/paper-gaps/ files are touched.

ℹ️ Advisory (non-blocking)

One internal citation inconsistency: the PeripheralEqualCaseZGaugeOfSameMPV docstring (Theorem41Forward.lean, ~line 357) cites the $\widetilde A$ construction as lines 760--810, whereas all five other occurrences in this PR (docstrings at ~379, 398, 423, 445, 473 and the blueprint) cite lines 765--810 for the same construction. Both ballpark the actual span (source ~758–810), but for consistency the 760 figure should likely be 765. Acceptable to merge as-is; worth a quick follow-up touch.

No 🔴 or 🟡 issues found.

[chatgpt-codex-connector]

💡 Codex Review

Here are some automated review suggestions for this pull request.

Reviewed commit: 2308049ce9

ℹ️ About Codex in GitHub

Your team has set up Codex to review pull requests in this repo. Reviews are triggered when you

• Open a pull request for review
• Mark a draft as ready
• Comment "@codex review".

If Codex has suggestions, it will comment; otherwise it will react with 👍.

Codex can also answer questions or update the PR. Try commenting "@codex address that feedback".

[claude]

Blueprint ↔ Lean & Prose Review

Scope: Category A (blueprint ↔ Lean equivalence and status accuracy) and Category B (prose quality per docs/prose_style.md) only.

Category A — Blueprint ↔ Lean equivalence

All \lean{...} tags in the changed .tex file resolve to unchanged Lean declaration signatures. Every \leanok on statements and proofs remains valid — no Lean signatures were touched. Hypotheses, conclusions, quantifiers, and indexing all match between the blueprint and Lean for every entry in the diff.

One source-reference inconsistency was found: the new PeripheralEqualCaseZGaugeOfSameMPV docstring cites the $\widetilde A$ construction as "lines 760--810" while the blueprint definition def:peripheral_equalcase_root_from_zgauge and the zGaugeEquiv_of_periodicEqualCaseFT_of_irreducibleForm docstring (both also changed in this PR) cite the same construction as "lines 765--810". See inline comment.

Category B — Prose quality

Two issues in changed or PR-adjacent text:

1. The new PeripheralEqualCaseZGaugeOfSameMPV docstring title uses \(Z\) (correct) but the body preserves `Z`-gauge witness with Z in backticks, treating a mathematical symbol as a Lean identifier. The PR introduced this inconsistency by updating the title while leaving the body unchanged. See inline comment with a one-line suggestion.

2. The blueprint proof sketch for thm:thm_4_1_p_refinement_forward_blocked_equalcase (left unchanged by the PR) now uses $A'$ while every surrounding definition and theorem statement was updated by this PR to use $\widetilde A$ for the same object. The notation $A'$ is also the Lean variable name, making it Lean jargon in blueprint prose (§1 ban). See inline comment with a drop-in suggestion.

---

Summary: 1 Category A source-reference inconsistency, 2 Category B prose issues (1 backtick symbol, 1 variable-name inconsistency). All three introduced or exposed by this PR's changes.

[claude]

Review: APPROVE ✅

PR #3390: doc(MPS/Periodic): align Theorem 4.1 source prose

Summary

This is a documentation-only PR: no Lean theorem signatures, statements, or proofs are changed. The PR aligns prose in Theorem41Forward.lean module headers/docstrings and ch22_periodic_ft.tex blueprint text with source paper arXiv:1708.00029, lines 735–810. Local "pullback," "blocked root," and "reconstruction" language is replaced by the paper's terminology: tensor (C) from the refinement isometry (W), the (p)-blocked tensor, the (Z)-gauge step, and construction of (\widetilde A) from scalars (c_{j,\alpha}).

Findings by category

Category	Severity	Verdict
🔴 Proof integrity	Blocker	✅ PASS — no sorry, axiom, native_decide, or unsafeCast changes
🔴 Proof correctness	Blocker	✅ PASS — all theorem bodies, types, and proofs are untouched
🟡 Mathlib style	Requires changes	✅ PASS — docstrings follow Mathlib conventions; \(...\) for math symbols, backticks for Lean identifiers
🔴 Type safety	Blocker	✅ PASS — no type changes
🟡 Performance	Requires changes	✅ PASS — no proof changes
🟡 Modularity & duplication	Requires changes	✅ PASS — no code changes
🟡 Documentation	Requires changes	✅ PASS — docstrings have precise line-range citations; source constructions are properly qualified with irreducibility scope
🟡 Paper-gap notes	Requires changes	N/A — no paper-gap files changed

Resolved from previous review cycle

• 760/765 line-range inconsistency: Outdated — now 765--810 uniformly across all docstrings.
• Backtick-Z vs \(Z\): Resolved — Z uses \(Z\) throughout (title and body).
• Irreducibility qualification: Resolved — PeripheralEqualCaseRootFromZGauge docstring explicitly states "In the irreducible-form subcase treated in arXiv:1708.00029, lines 765--810" and "The formal statement keeps this construction as a conditional input for arbitrary A; it does not assert the irreducible block data of A as hypotheses."
• Blueprint A' → \widetilde A in proof sketches: Fixed in second commit.

Verdict

APPROVE. All 🔴 blocker and 🟡 required-change categories pass. No new issues found. The PR faithfully aligns documentation with the source paper.

[claude]

Review: doc(MPS/Periodic): align Theorem 4.1 source prose

Verdict: APPROVE.

This is a documentation-only PR touching TNLean/MPS/Periodic/Symmetry/Theorem41Forward.lean (module/docstring text) and blueprint/src/chapter/ch22_periodic_ft.tex (theorem titles, proof prose, comments). No Lean statements, definitions, theorem signatures, or proof terms are modified, and no sorry/axiom/native_decide is introduced. The proof-integrity, type-safety, performance, and Mathlib-style categories are therefore not engaged. Blueprint-tag sync (\lean/\leanok/\uses) and general prose quality are out of scope here (handled by the Blueprint Sync & Prose Review workflow); no docs/paper-gaps/ note is changed.

Mathematical faithfulness of the new docstring/blueprint claims (in scope)

The renamed prose now attributes explicit formulas to the source. I checked each against Papers/1708.00029/main.tex and they are faithful:

• The tensor C — def:p_refinement_pullback_irreducible_form and the docstrings on evalWord_sum_smul_ofFn / pRefinementCanonicalization_pullback: C^{i_1,…,i_p} := ∑_i W^{(i_1,…,i_p),i} B^i matches the paper (main.tex:742).
• def:peripheral_equalcase_root_from_zgauge and the docstring on PeripheralEqualCaseRootFromZGauge: A'^i_j = ∑_u d_{j,u} P_{j,u} A_j^i matches main.tex:787; A'^{(p)} = Z A^{(p)} and à = U†A'U match main.tex:808.
• The c_{j,α} scalars are correctly described as finite-order phases (c_{j,α}^{m_j/r_j}=1, main.tex:784).

Scope of the conditional hypotheses (previously flagged, now addressed)

The concern raised earlier by chatgpt-codex-connector — that the source construction (periodic blocks A_j, scalars c_{j,α}) presupposes A in irreducible form II (main.tex:751, "we can assume without loss of generality that A is in irreducible form II"), whereas the Lean Prop PeripheralEqualCaseRootFromZGauge accepts arbitrary A — is now explicitly handled. Both the docstring and def:peripheral_equalcase_root_from_zgauge state that the source description is the intended irreducible-form subcase and that the formal statement keeps the construction as a conditional input without asserting the block data for arbitrary A. This honestly reflects the gap between the conditional Lean hypothesis and the source argument. The two earlier claude threads (line-range 765--810 consistency; \(Z\)-gauge vs backtick Z at line 355) are likewise addressed by the current text. I have resolved these three bot threads.

Minor, non-blocking

The cited range 765--810 for the Ã construction begins slightly after the source's own start of that argument — the reduction to irreducible form and the thm:bdequal Z-gauge equality run from main.tex:751, with the c_{j,α}/A'_j construction at 787–808. The bracket is a reasonable approximation and the consistency issue with the earlier 760 typo is resolved; flagging only for awareness.

No blocking or change-requiring issues. The prose changes are mathematically accurate and improve the correspondence with arXiv:1708.00029.

[chatgpt-codex-connector]

💡 Codex Review

Here are some automated review suggestions for this pull request.

Reviewed commit: 211edc403e

ℹ️ About Codex in GitHub

Your team has set up Codex to review pull requests in this repo. Reviews are triggered when you

• Open a pull request for review
• Mark a draft as ready
• Comment "@codex review".

If Codex has suggestions, it will comment; otherwise it will react with 👍.

Codex can also answer questions or update the PR. Try commenting "@codex address that feedback".

[claude]

Review Summary — PR #3390 (doc(MPS/Periodic): align Theorem 4.1 source prose)

Verdict: REQUEST_CHANGES

This is a documentation-only PR aligning the forward Theorem 4.1 narrative in Theorem41Forward.lean and ch22_periodic_ft.tex with terminology from arXiv:1708.00029, lines 735–810. No Lean statements, proofs, or logic change. The three previously-resolved bot threads (irreducibility qualification, line-number inconsistency 760→765, backtick Z → \(Z\)) have all been properly addressed in the current commit.

Issues found

#	Category	Severity	Location	Summary
1	Documentation	🟡 Must fix	ch22_periodic_ft.tex, lines 2009–2012 (def:peripheral_equalcase_root_from_zgauge)	"This is the construction in [lines 765–810]" describes the paper's full construction (including the stronger blocked-tensor identity (\widetilde A^{(p)} = C)), but the Lean definition PeripheralEqualCaseRootFromZGauge only asserts the weaker channel-level conclusion transferMap C = transferMap (blockTensor A' p). The existing qualification addresses irreducibility scope but not the conclusion-strength gap.

What's clean

• All Lean docstrings correctly use \(...\) for mathematical Z/\widetilde A notation and backticks only for genuine Lean identifiers (C, blockTensor A p, A').
• Line-number citations are now consistent (all cite 765–810 for the (\widetilde A) construction, and 735–743 for the (C) tensor).
• The split of the forward proof into two explicit obligations ((Z)-gauge extraction + (\widetilde A) construction) is clearly documented in both Lean and blueprint prose.
• No banned software-engineering terms or LLM-writing patterns in the new text.
• No proof integrity issues — no sorry, axiom, or native_decide in changed code.
• All CI checks pass (build, prose checker, blueprint sync, checkdecls).

Resolution required

Add a sentence to the blueprint definition at def:peripheral_equalcase_root_from_zgauge noting that the formal hypothesis tracks only the transfer-map equality (the channel-level weakening), while the source proof derives the stronger blocked-tensor identity. This is the same concern raised in the still-unresolved thread by @chatgpt-codex-connector.

[claude]

Review summary — PR #3390 doc(MPS/Periodic): align Theorem 4.1 source prose

Scope of change: documentation only. Every hunk in TNLean/MPS/Periodic/Symmetry/Theorem41Forward.lean lies inside /-- … -/ docstrings; no Lean theorem signature, proof term, definition body, type, or instance is touched. The blueprint changes in ch22_periodic_ft.tex are theorem titles, definition prose, and proof prose. The terminology shift ("W-pullback" → the tensor $C$ from the refinement isometry $W$; "blocked root / root hypothesis / reconstruction" → the $p$-blocked blockTensor A p, the blocked $Z$-gauge step, and the $\widetilde A$ construction from $c_{j,\alpha}$, arXiv:1708.00029 lines 735–810) is consistent across the two files.

In-scope categories

• 🔴 Proof integrity: N/A — no proof bodies changed; no sorry/axiom/native_decide introduced.
• 🔴 Proof correctness: N/A — no proof terms or tactic blocks changed.
• 🔴 Type safety: N/A — no signatures, universes, or instances changed.
• 🟡 Performance: N/A — no elaboration-affecting changes.
• 🟡 Modularity/duplication: clean. Retained pullback occurrences are genuine Lean identifier references (pRefinementCanonicalization_pullback, pRefinementCanonicalization_pullback_of_irreducibleForm) and the blueprint label thm:p_refinement_pullback_irreducible_form; correctly left unrenamed since the declarations themselves are unchanged.
• 🟡 Documentation: the prose is more precise than before and ties each conditional Prop (PeripheralEqualCaseZGaugeOfSameMPV, PeripheralEqualCaseRootFromZGauge, PeripheralEqualCasePeriodicFTOfSameMPV, PRefinementCanonicalization) to a specific source passage.

Previously raised bot threads

• 760-vs-765 line citation (claude) — fixed: all occurrences now read 765–810; no 760 remains.
• backtick `Z` vs \(Z\) in PeripheralEqualCaseZGaugeOfSameMPV (claude) — fixed.
• "qualify by irreducibility" on def:peripheral_equalcase_root_from_zgauge (codex) — addressed by the added hedge (ch22_periodic_ft.tex:2013–2015): "the definition above keeps the construction as a conditional input and does not assert these block data for arbitrary $A$."

Open item deferred to the Blueprint Sync & Prose Review workflow

The one unresolved bot thread (codex, ch22_periodic_ft.tex:2012, def:peripheral_equalcase_root_from_zgauge) is well-founded: the source proves the tensor-level identity $\widetilde A^{(p)}=C$ (arXiv:1708.00029 / Papers/1708.00029/main.tex:748–749 — "we will construct an $\tilde A$ for which even $\tilde A^{(p)}=C$" — and lines 808–810), whereas the \lean{}-tagged PeripheralEqualCaseRootFromZGauge concludes only the channel-level weakening transferMap C = transferMap (blockTensor A' p). The phrase "This is the construction in [lines 765–810]" attaches the source attribution to the weaker conclusion without a one-clause note that the formalized hypothesis is the channel-level weakening of $\widetilde A^{(p)}=C$. This is a blueprint↔Lean faithfulness/prose matter, which is explicitly out of scope for this review and handled by the dedicated Blueprint Sync & Prose Review workflow; I have left that thread unresolved for it to adjudicate, and have not duplicated it inline.

Verdict

All in-scope categories (proof integrity, correctness, type safety, performance, modularity, Lean documentation; no paper-gap notes touched) are clean for this documentation-only change. Approving. The remaining open codex thread is a legitimate prose-faithfulness nuance but belongs to the Blueprint Sync workflow's domain.

[claude]

Review summary

Category A (blueprint ↔ Lean equivalence): 0 issues

Every \lean{...} tag touched by this PR was checked against the corresponding Lean signature:

Blueprint entry	Lean declaration	Result
thm:p_refinement_pullback_irreducible_form	pRefinementCanonicalization_pullback_of_irreducibleForm	✓ match
def:peripheral_equalcase_zgauge_sameMPV	PeripheralEqualCaseZGaugeOfSameMPV	✓ match
thm:zgauge_equiv_periodicFT_irreducible_form	zGaugeEquiv_of_periodicEqualCaseFT_of_irreducibleForm	✓ match
def:peripheral_equalcase_root_from_zgauge	PeripheralEqualCaseRootFromZGauge	✓ match
def:peripheral_equalcase_periodicFT_sameMPV	PeripheralEqualCasePeriodicFTOfSameMPV	✓ match
thm:peripheral_equalcase_sameMPV_zgauge_reduction	peripheralEqualCase_periodicFT_of_sameMPV	✓ match
thm:p_refinement_forward_equalcase_reduction	pRefinementCanonicalization_of_peripheralEqualCase_periodicFT_of_sameMPV	✓ match
thm:thm_4_1_p_refinement_forward_blocked_equalcase	thm_4_1_p_refinement_forward_of_peripheralEqualCase_periodicFT_of_sameMPV	✓ match
thm:thm_4_1_p_refinement	thm_4_1_p_refinement	✓ match
thm:thm_4_1_p_refinement_forward	thm_4_1_p_refinement_forward	✓ match

All \leanok statement tags resolve to declarations whose Lean signatures match the blueprint statements on quantifiers, hypotheses, and conclusions. All proof \leanok tags were spot-checked and no new sorry or admit is introduced. All \notready tags in scope are unaffected.

Also resolved the now-outdated claude thread about the "760 vs 765" line-number discrepancy — that discrepancy is fixed in the latest commit (all references now consistently cite "lines 765--810").

---

Category B (prose quality): 1 issue

One violation of §2 ("Data as a vague collection word") in the blueprint, flagged inline on blueprint/src/chapter/ch22_periodic_ft.tex line 2015.

"does not assert these block data for arbitrary $A$"

The style guide §2 bans "data" as a vague collection word and requires naming the specific objects or displaying the tuple. The $A_j$ and $c_{j,\alpha}$ are listed two lines above, so the fix is to name them directly. Suggestion posted inline.

---

Count: 0 equivalence mismatches, 0 stale \leanok, 1 prose issue (§2 "data").

[claude]

[claude-review-fix] Addressed: channel-level vs blocked-tensor identity gap

Both unresolved threads on blueprint/src/chapter/ch22_periodic_ft.tex:2012 flagged the same documentation gap on def:peripheral_equalcase_root_from_zgauge (MPSTensor.PeripheralEqualCaseRootFromZGauge):

The prose says "This is the construction in [lines 765–810]", but the cited passage (arXiv:1708.00029, lines 808–810) constructs $\widetilde A$ with the stronger blocked-tensor identity $\widetilde A^{(p)} = C$, whereas the Lean definition only asserts the channel-level consequence $\mathcal E_C = \mathcal E_{\widetilde A^{[p]}}$ (transfer-map equality). The existing irreducibility-scope qualification did not cover this conclusion-strength gap.

Fix

Appended a clarifying sentence to the definition prose noting that the cited source obtains $\widetilde A^{[p]} = C$, while the formal hypothesis records only its channel-level consequence $\mathcal E_C = \mathcal E_{\widetilde A^{[p]}}$, and that this conditional input is therefore the transfer-map weakening of the source construction, not the full blocked-tensor equality.

This matches what the Lean definition actually states:

def PeripheralEqualCaseRootFromZGauge (d D p : ℕ) : Prop :=
  ∀ {A : MPSTensor d D} {C : MPSTensor (blockPhysDim d p) D} {m : ℕ},
    IsIrreducibleForm C → 0 < m → ZGaugeEquiv m C (blockTensor A p) →
      ∃ A' : MPSTensor d D,
        (∑ i : Fin d, (A' i)ᴴ * A' i = 1) ∧
        transferMap C = transferMap (blockTensor A' p)

The conclusion is transfer-map equality, not the blocked-tensor identity.

Source citation

arXiv:1708.00029 (De Las Cuevas et al., Irreducible forms of matrix product states), lines 765–810: the phase-distribution construction redistributes the scalars $c_{j,\alpha}$ into $A'_j$ and sets $\widetilde A = U^\dagger A' U$, with the blocked identity $\widetilde A^{(p)} = C$ established at lines 808–810.

Scope

Documentation only — LaTeX blueprint prose. No Lean signature, proof, or definition body changed, so lake build is unaffected. No Mathlib lemmas involved.

Commit: 9fbbd34

[claude]

Review-fix iteration 2

Addressed the unresolved threads on blueprint/src/chapter/ch22_periodic_ft.tex (definition def:peripheral_equalcase_root_from_zgauge / MPSTensor.PeripheralEqualCaseRootFromZGauge):

1. Channel-level vs. blocked-tensor qualification (codex P2 + claude threads, line ~2012)

The opening phrase "This is the construction in \cite[lines~765--810]{DeLasCuevas2017Irreducible}" overstated the link: the source (arXiv:1708.00029, lines 765–810, with the blocked-tensor identity at 808–810) builds $\widetilde A$ with $\widetilde A^{[p]} = C$, while the Lean definition only assumes the channel-level consequence $\mathcal E_C = \mathcal E_{\widetilde A^{[p]}}$ (transfer-map equality). Reworded the opening to "This channel-level hypothesis is the transfer-map reading of the construction in …", so the definition is presented as the transfer-map weakening rather than the full source construction. This complements the existing paragraph (already present) recording that the source obtains $\widetilde A^{[p]} = C$ whereas the formal hypothesis records only its channel-level consequence.

2. Prose §2 — "Data as a vague collection word" (Category B, line ~2015)

Replaced "does not assert these block data for arbitrary $A$" with the explicit objects: "does not assert these block scalars $c_{j,\alpha}$ and matrices $A'_j$ for arbitrary $A$", per docs/prose_style.md §2.

No Lean sources were touched (blueprint prose only), so lake build was not required. No \lean/\leanok tags changed; all Category A blueprint↔Lean signature matches remain intact.

Note: rebased onto a concurrent upstream commit that independently fixed the same "data" wording; the channel-level qualification and the explicit-objects phrasing are both retained.

[claude]

Review: APPROVE ✅

PR #3390: doc(MPS/Periodic): align Theorem 4.1 source prose

Scope

This is a documentation-only PR: every change in Theorem41Forward.lean is inside /-- … -/ docstrings, and every change in ch22_periodic_ft.tex is theorem/definition titles, proof prose, or LaTeX comments. No Lean theorem signatures, statements, proof terms, or types are changed. The PR aligns the forward Theorem 4.1 narrative with arXiv:1708.00029, lines 735–810, replacing opaque local terminology ("W-pullback," "blocked root / root hypothesis / reconstruction") with the source paper's language: tensor (C) from the refinement isometry (W), the (p)-blocked tensor, the (Z)-gauge step, and the construction of (\widetilde A) from scalars (c_{j,\alpha}).

Findings by category

Category	Severity	Verdict
🔴 Proof integrity	Blocker	✅ PASS — no sorry, axiom, or native_decide changes
🔴 Proof correctness	Blocker	✅ PASS — all theorem bodies, types, and proofs are untouched
🟡 Mathlib style	Requires changes	✅ PASS — docstrings follow Mathlib conventions; \(...\) for math, backticks for Lean identifiers
🔴 Type safety	Blocker	✅ PASS — no signature changes
🟡 Performance	Requires changes	✅ PASS — no proof changes
🟡 Modularity & duplication	Requires changes	✅ PASS — no code changes
🟡 Documentation	Requires changes	✅ PASS — all changed definitions/theorems have thorough docstrings with precise line-range citations; the channel-level vs blocked-tensor identity gap is explicitly documented in both Lean and blueprint prose
🟡 Paper-gap notes	Requires changes	N/A — no paper-gap files changed

Resolved from prior review cycles

All previously-unresolved bot threads (PRRT_kwDORK8b986LY-Zm and PRRT_kwDORK8b986LY9Lt) are now addressed by the later commits (9fbbd34, 4656ca2), which added explicit documentation of the channel-level vs blocked-tensor identity gap at def:peripheral_equalcase_root_from_zgauge (lines 2017–2022 of the blueprint). Both threads have been resolved.

Source-citation accuracy

Verified each cited construction against Papers/1708.00029/main.tex:

• Tensor (C) (lines 735–743): C^{i_1,…,i_p} = ∑_i W^{(i_1,…,i_p),i} B^i matches main.tex:742.
• Blocked equal-case FT thm:bdequal (lines 643–656): correctly cited as the source of the (Z)-gauge step.
• Construction of (\widetilde A) (lines 765–810): A'_j{}^i = ∑_u d_{j,u} P_{j,u} A_j^i (line 787), A'^{(p)} = Z A^{(p)} and \widetilde A = U^\dagger A' U (line 808). All correctly attributed.
• The scalars c_{j,\alpha} are correctly described as finite-order phases.
• The channel-level weakening (transfer-map equality vs blocked-tensor identity) is explicitly documented in both Lean (Theorem41Forward.lean:390–404) and blueprint (ch22_periodic_ft.tex:2017–2022).

Verdict

APPROVE. All 🔴 blocker and 🟡 required-change categories pass. No new issues found. The prior review cycle's concerns are fully addressed. This PR meaningfully improves mathematical fidelity to the source paper.

[LionSR]

The requested prose issue is addressed in commit 096432d: the phrase "block data" now names the blocks $A_j$, scalars $c_{j,\alpha}$, and matrices $A'_j$, while preserving the channel-level weakening note.

@claude review

[claude]

Review: doc(MPS/Periodic): align Theorem 4.1 source prose

Documentation-only PR (66/54 additions in Theorem41Forward.lean docstrings, 75/54 in ch22_periodic_ft.tex prose). No Lean statements, signatures, or proof bodies change. I verified this against the diff: every +/- line touches a docstring, module doc, or LaTeX environment body.

Proof integrity / correctness / type safety / performance (🔴/🟡)

No code is modified, so these categories are not implicated. No new sorry, axiom, or kernel-bypass is introduced.

Faithfulness check against the source (the substantive concern)

The realignment renames local "W-pullback / blocked root / reconstruction" terminology to the paper's objects (the tensor C from the refinement isometry W, the p-blocked blockTensor A p, the blocked Z-gauge step, and the Ã construction). I checked each renamed object against Papers/1708.00029/main.tex:

• C definition. def:p_refinement_pullback_irreducible_form and the evalWord_sum_smul_ofFn docstring now state Cᵅ := ∑_i W_{α,i} Bⁱ. This matches Papers/1708.00029/main.tex:741-742: C^{i_1,…,i_p} := ∑_{i=1}^d W^{(i_1,…,i_p),i} B^i. ✓
• Ã construction. The PeripheralEqualCaseRootFromZGauge docstring and def:peripheral_equalcase_root_from_zgauge describe A'^i_j = ∑_u d_{j,u} P_{j,u} A_j^i, A'^{(p)} = ZA^{(p)}, and à = U^† A' U. This matches main.tex:786-810. ✓
• Channel-level weakening (faithfulness rule). The source proves the strong blocked-tensor identity Ã^{(p)} = C (main.tex:752: "we will construct an à for which even Ã^{(p)}=C"), whereas the Lean definition MPSTensor.PeripheralEqualCaseRootFromZGauge only asserts transferMap C = transferMap (blockTensor A' p), i.e. E_C = E_{Ã^{[p]}}. The blueprint now explicitly records this as the transfer-map weakening (ch22_periodic_ft.tex: "the formal hypothesis above records only its channel-level consequence … not the full blocked tensor equality"), and qualifies the construction as the intended irreducible-form subcase rather than asserting the block scalars c_{j,α} for arbitrary A. This correctly satisfies the CLAUDE.md faithfulness rule for a stricter/weaker-than-source formal statement. ✓

Citation consistency

All cited line ranges are now internally consistent: 735--743 for the C definition, 765--810 for the Ã construction (6 occurrences), 812--818 for the reverse direction. The previously-flagged 760 vs 765 discrepancy and the backtick-Z inconsistency are gone from the added text.

Out of scope (handled by Blueprint Sync & Prose Review)

Blueprint↔Lean tag sync and general prose/banned-AI-language quality are deferred to the dedicated workflow and not assessed here. No docs/paper-gaps/ files are touched, so the paper-gap-note criteria do not apply.

Resolved threads

I resolved the two previously-unresolved bot threads — chatgpt-codex-connector's P2 "qualify the source construction as channel-level" and claude's "channel-level vs blocked-tensor identity gap" — as both are addressed by the new qualifying paragraph at ch22_periodic_ft.tex lines 2013–2022.

Verdict: APPROVE. No 🔴 or 🟡 issues. The prose faithfully tracks Papers/1708.00029/main.tex:730-810, and the channel-level-vs-source-identity weakening is now explicitly documented per the faithfulness rule.

[claude]

Claude finished @LionSR's task in 2m 11s —— View job

---

Review — prose fix for the "block data" wording

• Read the updated blueprint and Lean docstring prose
• Verify the "block data" → named-objects fix
• Confirm the channel-level weakening note is preserved
• Post review

Verdict: looks good ✅ (documentation-only; PR already merged into main as ffbbbc4)

What I checked

I reviewed the merged state of def:peripheral_equalcase_root_from_zgauge in blueprint/src/chapter/ch22_periodic_ft.tex and the matching docstring in Theorem41Forward.lean.

1. §2 "data as a vague collection word" — fixed. The blueprint clause now names the specific objects:

"…keeps the construction as a conditional input and does not assert these block scalars $c_{j,\alpha}$ and matrices $A'_j$ for arbitrary $A$."

The periodic block $A_j$ is named two lines above (for each periodic block $A_j$, the scalars $c_{j,\alpha}$ define matrices $A'_j$), so all three objects ($A_j$, $c_{j,\alpha}$, $A'_j$) are now explicit per docs/prose_style.md §2. No bare \bdata\b collection word remains in the changed region (the one surviving use, refinement data at line 1960, immediately names its tuple $(A,W)$, so it is compliant).

2. Channel-level weakening note — preserved. The closing paragraph is intact and correctly distinguishes the two strengths:

"The cited source moreover obtains the blocked-tensor identity $\widetilde A^{[p]} = C$, whereas the formal hypothesis above records only its channel-level consequence $\mathcal E_C = \mathcal E_{\widetilde A^{[p]}}$ … the transfer-map weakening of the source construction, not the full blocked tensor equality."

This matches the Lean def PeripheralEqualCaseRootFromZGauge, whose conclusion is transferMap C = transferMap (blockTensor A' p). Consistent with the CLAUDE.md faithfulness rule.

3. Consistency of the rest. Line-range citations are uniform (765--810 for the $\widetilde A$ construction, 735--743 for $C$); no stray 760--810, no backtick-Z. Retained pullback occurrences are genuine Lean identifier references (pRefinementCanonicalization_pullback), correctly left unrenamed.

Minor, non-blocking advisories (optional follow-up)

• Lean docstring still says "block data". Theorem41Forward.lean:404 reads "it does not assert the irreducible block data of A as hypotheses." The blueprint counterpart was updated to name $c_{j,\alpha}$/$A'_j$; for symmetry the Lean docstring could do the same (the objects are already named in the paragraph just above, so this is purely cosmetic). docs/prose_style.md §2 applies to docstrings as well as .tex.
• Reverse-direction terminology. ch22_periodic_ft.tex:2169–2176 still uses "blocked-to-root reconstruction" in the reverse-direction section, which this PR did not touch (forward-direction scope only). Not a defect here, but a candidate for a future alignment pass so the chapter's forward/reverse halves share vocabulary.

No proof-integrity, faithfulness, or blueprint↔Lean equivalence concerns. The requested change is correctly in place.

[chatgpt-codex-connector]

💡 Codex Review

Here are some automated review suggestions for this pull request.

Reviewed commit: 4656ca2648

ℹ️ About Codex in GitHub

Your team has set up Codex to review pull requests in this repo. Reviews are triggered when you

• Open a pull request for review
• Mark a draft as ready
• Comment "@codex review".

If Codex has suggestions, it will comment; otherwise it will react with 👍.

Codex can also answer questions or update the PR. Try commenting "@codex address that feedback".

[chatgpt-codex-connector]

Align the Z-gauge orientation with the source construction

The source formula quoted here needs the finite-order matrix acting on the blocked root, but the hypothesis below is ZGaugeEquiv m C (blockTensor A p). By the definition of ZGaugeEquiv m X Y, that supplies a Z commuting with and multiplying the first argument X (here C), not A^{(p)}, so the periodic-block scalars c_{j,α} for the blocks of A are not available unless an orientation/inversion step is added or the equivalence is flipped.

Useful? React with 👍 / 👎.