doc(MPS/ParentHamiltonian): align PGVWC boundary-word terminology#3277
Conversation
|
You have reached your Codex usage limits for code reviews. You can see your limits in the Codex usage dashboard. |
claude
Bot
changed the title
claude
Bot
added
formalization
|
PR cleanup
Conventions: CONTRIBUTING.md |
![claude[bot]](https://avatars.githubusercontent.com/in/1236702?s=60&v=4){kind=small}
There was a problem hiding this comment.
Review Summary
This is a clean terminology-only PR. All 17 additions and 18 deletions are confined to docstrings (Lean module/theorem docstrings), blueprint prose, and the paper-gap note. No theorem signatures, proof terms, \lean{} tags, or \leanok markers were modified.
Per-category findings
-
🔴 Proof integrity: No changes. No
sorry,axiom, or proof bypasses introduced. -
🔴 Proof correctness: No proof terms modified. All statements preserved verbatim.
-
🟡 Mathlib style: The terminology substitution is correct and improves precision:
"word-indexed"→"cut-adapted"/"boundary-crossing"— eliminates the ambiguous "word-indexed" which could refer to any word, and replaces it with terminology describing what kind of word (cut-adapted coordinates)."formal word variables"→"cut-adapted words"/"blocked-word form"— removes the confusing "formal" (which has dual meanings of "formal proof system" and "in form only") and replaces it with precise descriptors."site-indexed matrices"→"boundary-indexed matrices"— more consistent with the paper's own notation (the source uses boundary indices (i_1, i_{m+1}))."local boundary-crossing coordinate form"→"cut-adapted boundary-crossing form"— drops the vague "local" and uses the specific "cut-adapted."
No banned software-engineering terms or LLM writing patterns appear in the new text. The new terminology is mathematical and source-faithful.
-
🔴 Type safety: No type changes.
-
🟡 Performance: No performance-affecting changes.
-
🟡 Modularity & duplication: No modularity concerns.
-
🟡 Documentation: Docstrings maintain coverage. The changes clarify rather than degrade the mathematical exposition.
-
🟡 Paper-gap notes: The changes to
cpgsv21_block_diagonal_parent_ground_space.texare terminology-only substitutions ("local coordinates"→"cut-adapted coordinates","blocked words obtained by opening the source boundary-index comparison"). The note remains a self-contained mathematical account perdocs/paper-gaps/policy.tex: it introduces notation in §1, states the source assertion in §2, isolates the boundary in §4, and gives a clear verdict in §5 ("not a source-error claim"). The classification as a scope-restriction/conditional-derivation note is unchanged.
Tools verified
blueprint_lean_sync.py --ci— passed (2830/2847 declarations synced, 99.4%)git diff --check— no whitespace errors- No existing review threads or PR comments to resolve
Verdict
APPROVE. No 🔴 or 🟡 issues found.
There was a problem hiding this comment.
Blueprint ↔ Lean sync and prose review (categories A and B only).
Category A — Blueprint ↔ Lean equivalence and status
No \lean{...} tags were added, removed, or changed. No \leanok or \notready status tags were touched. No theorem statements or Lean signatures were modified. The PR makes no change to the mathematical content of any formalized result, so there are no equivalence or status issues to flag.
0 equivalence mismatches, 0 stale \leanok, 0 missing tags.
Category B — Prose quality
Changed prose in blueprint/src/chapter/ch13_parent_hamiltonian_block_diagonal_chain_equality.tex and the /-! ... -/ / /- ... -/ docstrings in TNLean/MPS/ParentHamiltonian/BNTBlockDiagonalPGVWCComparison.lean (the docs/paper-gaps/ file is out of scope).
- No banned software-engineering terms introduced.
- No banned LLM writing patterns introduced.
- No Lean identifiers or namespace names appear in the blueprint prose.
- The boundary-crossing identity
$A^j_\beta C^j_{i,\rho} = \bigl((\mu_j^N X_j)A^j_\beta\bigr)A^j_\rho$ is displayed alongside every prose claim that refers to it; no word-only proof sketch without a corresponding formula. - Removing "formal" from "formal word variables" and "formal statement" improves mathematical directness without introducing any new issue.
0 prose issues.
There was a problem hiding this comment.
Review summary
Scope: Prose/terminology-only PR (17 insertions, 18 deletions). It replaces the "formal word"/"word-indexed"/"local coordinate" phrasing for the PGVWC (C^j,D^j) boundary comparison with "cut-adapted"/"blocked-word" terminology across one Lean module docstring (BNTBlockDiagonalPGVWCComparison.lean), one blueprint subsection (ch13_parent_hamiltonian_block_diagonal_chain_equality.tex), and one paper-gap note (cpgsv21_block_diagonal_parent_ground_space.tex). No Lean statements, proofs, \lean{}/\leanok tags, sorrys, or axioms are modified — confirmed against the diff.
What I checked and found clean:
- Proof integrity / correctness / type safety / performance: Not applicable — no proof or statement content changes, no new
sorry/axiom/native_decide. - Mathematical accuracy of the new wording: Faithful and more precise. The words (\beta) (length (a=i+L-N), before the cut) and (\rho) (outside word, length (N-L)) genuinely are the blocked site-words determined by where the periodic boundary cut is opened, so "cut-adapted coordinates"/"blocked words" is a sharper description than the previous "formal word variables." The change does not overclaim that (\beta,\rho) are source notation: the not-source-notation distinction is preserved (note line 286 "separates the cut-adapted coordinates from the paper's boundary indices"; line 502 "are not additional hypotheses or terminology from the paper"; Lean docstring line 446 "reindex the source end-site comparison by blocked words rather than replacing the source indices"). The
site-indexed → boundary-indexedswap for (C^j_{i_1}, D^j_{i_{m+1}}) is also accurate, since those matrices are indexed by the two boundary sites of the crossing interval. - Paper-gap note vs
policy.tex: The note stays self-contained, introduces its notation, states the cited (C^j,D^j,E^j) comparison from[Theorem 12]{PerezGarcia2007MPSReps}, isolates the remaining obstruction, and gives a verdict. The terminology swap does not degrade this.
🟡 Requires changes (1 issue):
- The terminology pass is incomplete. The paper-gap note still labels (\beta,\rho) as "local word coordinates" at line 500, while the immediately preceding line (498) was changed to "the cut-adapted (C^j,D^j) route" and the rest of the note now uses "cut-adapted coordinates." Two competing labels for the same objects in one paragraph undercut the internal consistency this PR is meant to establish. Fix flagged inline with a one-line suggestion.
This is a single trivial fix; once "local word coordinates" at line 500 is aligned to the new terminology, the PR is good to merge.
| The word-indexed \(C^j,D^j\) route is closer to the proof of | ||
| The cut-adapted \(C^j,D^j\) route is closer to the proof of | ||
| \cite[Theorem~12]{PerezGarcia2007MPSReps}. | ||
| The words \(\beta\) and \(\rho\) are local word coordinates introduced after |
There was a problem hiding this comment.
Incomplete terminology pass. This PR replaces the "formal word"/"word-indexed"/"local coordinate" phrasing for the PGVWC (C^j,D^j) boundary comparison with "cut-adapted coordinates" everywhere else in this note (lines 247, 258, 286) and in the Lean docstring and blueprint. But this line still calls (\beta,\rho) "local word coordinates," and the immediately preceding line (498) was just changed to "The cut-adapted (C^j,D^j) route." Using two different labels for the same (\beta,\rho) objects within one paragraph undercuts the internal consistency the PR is establishing, which the paper-gap policy (docs/paper-gaps/policy.tex, "Shared commands"/coherence) asks notes to maintain.
Suggested alignment:
| The words \(\beta\) and \(\rho\) are local word coordinates introduced after | |
| The words \(\beta\) and \(\rho\) are cut-adapted coordinates introduced after |
The rest of the sentence — "they reindex the source end-site comparison (i_1,i_{m+1}) by blocked words, and are not additional hypotheses or terminology from the paper" — already carries the not-source-notation disclaimer and can stay.
| The word-indexed \(C^j,D^j\) route is closer to the proof of | ||
| The cut-adapted \(C^j,D^j\) route is closer to the proof of | ||
| \cite[Theorem~12]{PerezGarcia2007MPSReps}. | ||
| The words \(\beta\) and \(\rho\) are local word coordinates introduced after |
There was a problem hiding this comment.
Incomplete terminology pass: line 498 was changed to "The cut-adapted (C^j,D^j) route," but this line still calls the same objects (\beta,\rho) "local word coordinates." Within a single paragraph (lines 498–503), the two adjacent sentences now use inconsistent labels for the identical mathematical objects. The paper-gap policy (docs/paper-gaps/policy.tex, §4 "Shared commands"/coherence) expects internal consistency within a note.
Suggested fix: change "local word coordinates" to "cut-adapted coordinates" to match line 498. The rest of the sentence already carries the not-source-notation disclaimer and can remain unchanged.
There was a problem hiding this comment.
Review Summary
Scope: Prose/terminology-only PR (17 additions, 18 deletions) replacing "formal word"/"word-indexed"/"local coordinate" phrasing with "cut-adapted"/"blocked-word" terminology across one Lean module docstring (BNTBlockDiagonalPGVWCComparison.lean), one blueprint subsection (ch13_parent_hamiltonian_block_diagonal_chain_equality.tex), and one paper-gap note (cpgsv21_block_diagonal_parent_ground_space.tex). No Lean theorems, proofs, sorry, axiom, \lean{} tags, or \leanok markers are modified.
Per-category findings
-
🔴 Proof integrity: No changes. No
sorry,axiom, or proof bypasses introduced or modified. -
🔴 Proof correctness: No proof terms modified. All theorem signatures preserved verbatim.
-
🟡 Mathlib style: The terminology substitutions are mathematically accurate and improve precision:
"word-indexed"→"cut-adapted"/"boundary-crossing"— replaces vague "word-indexed" with terminology describing what kind of word (cut-adapted coordinates)."formal word variables"→"cut-adapted words"/"blocked-word form"— removes the ambiguous "formal" and replaces it with precise descriptors."site-indexed matrices"→"boundary-indexed matrices"— more consistent with the paper's own notation (the source uses boundary indices (i_1, i_{m+1}))."local boundary-crossing coordinate form"→"cut-adapted boundary-crossing form"— drops the vague "local" and uses the specific "cut-adapted."
No banned software-engineering terms or LLM writing patterns appear in the new text. No style violations.
-
🔴 Type safety: No type changes. Not applicable.
-
🟡 Performance: No performance-affecting changes. Not applicable.
-
🟡 Modularity & duplication: No modularity concerns. Not applicable.
-
🟡 Documentation: The docstring changes are strictly clarifying. Coverage is maintained; the changes improve mathematical exposition by using more precise, source-faithful terminology. No missing documentation.
-
🟡 Paper-gap notes: One issue found. The terminology pass to
docs/paper-gaps/cpgsv21_block_diagonal_parent_ground_space.texis incomplete at line 500. Line 498 was changed to read "The cut-adapted (C^j,D^j) route," but line 500 still reads "The words (\beta) and (\rho) are local word coordinates introduced after..." Two competing labels for the same objects (\beta,\rho) in adjacent sentences (within the same paragraph) undercut the internal consistency the PR is meant to establish. The paper-gap policy (docs/paper-gaps/policy.tex, §4 "Shared commands"/coherence) expects internal consistency within a note. The fix is a one-line substitution ("local word coordinates" → "cut-adapted coordinates"). The rest of the note (lines 247, 258, 286) is correctly updated. Flagged inline.
Verification
- ✅
blueprint_lean_sync.py --cipassed (no\lean{}tags changed) - ✅
git diff --check— no whitespace errors - ✅ No Lean statement or proof changes
- ✅ All changes confined to docstrings and prose
Verdict
REQUEST_CHANGES. The incomplete terminology pass at line 500 of the paper-gap note must be fixed. Once "local word coordinates" at line 500 is aligned to "cut-adapted coordinates," all outstanding issues are resolved and the PR can be approved.
There was a problem hiding this comment.
Review — doc(MPS/ParentHamiltonian): align PGVWC boundary-word terminology
Prose/documentation-only PR: it edits module and definition docstrings in
BNTBlockDiagonalPGVWCComparison.lean, the corresponding ch13 blueprint subsection,
and the paper-gap note cpgsv21_block_diagonal_parent_ground_space.tex. No theorem
signature, \lean{} tag, proof term, or tactic block changes, so the proof-integrity,
proof-correctness, type-safety, and performance categories do not apply. I confirmed the
source framing against Papers/quant-ph_0608197/MPSarchive.tex:1424–1456 (Theorem
"Degeneracy of the ground space v2") and Papers/2011.12127/TN-Review-main.tex:2108–2128.
🟡 Requires changes — incomplete terminology pass in the paper-gap note
The PR's stated purpose is to retire the "formal word"/"word-indexed" framing for the
PGVWC
247, 257–258, 286–287, and 498, but line 500 still labels the same objects "local word
coordinates":
The cut-adapted
$C^j,D^j$ route is closer to the proof of [Theorem 12]. The words
$\beta$ and$\rho$ are local word coordinates introduced after opening and blocking
the cyclic boundary comparison …
Within one paragraph
yet are still called "local word coordinates" (line 500). docs/paper-gaps/policy.tex
(§Revision) asks that revisions "keep it as a coherent account"; leaving one residual label
for the objects the rest of the pass renamed is exactly the coherence gap the note should
avoid. This is already raised in an unresolved inline claude thread on line 500 with a
concrete suggestion (cut-adapted coordinates); I have left that thread open since it is
not yet addressed at the branch HEAD. The trailing clause — "they reindex the source
end-site comparison
terminology from the paper" — already carries the not-source-notation disclaimer and should
stay.
ℹ️ Advisory — PR-body claim slightly overstates the source
The PR motivation says the PGVWC07 source "describes them as cut-adapted coordinates after
opening the periodic cut." The source statement and proof
(MPSarchive.tex:1424–1456; TN-Review-main.tex:2108–2128) use end-site indices
or the phrase "cut-adapted." The note itself stays faithful — it explicitly disclaims that
this is only a note on the PR description's phrasing. Note also that the new note sentence
at line 257–258 ("These are the blocked words obtained by opening the source boundary-index
comparison") drops the point-of-introduction disclaimer that the old text carried ("not
names used in the source statement"); the disclaimer survives ~245 lines later at 500–503,
so the note remains correct, but restoring a short disclaimer at first use would read more
faithfully.
Verdict
REQUEST_CHANGES — one outstanding 🟡 (the already-flagged, unresolved
terminology-consistency gap at note line 500). The change is otherwise faithful and clean;
resolving line 500 to match the rest of the pass clears the only blocker.
2 participants
Motivation
BNTBlockDiagonalPGVWCComparison.lean, the corresponding blueprint subsection, and the paper-gap note described the PGVWC07 boundary matrices β and ρ as "formal word" labels; the PGVWC07 source (arXiv:quant-ph/0608197, Theorem 12; arXiv:2011.12127 §IV.C, lines 2126–2128) describes them as cut-adapted coordinates after opening the periodic cut, not word-indexed labels.BNTBlockDiagonalPGVWCComparison.leanmust cite correct prose before they can be narrowed or removed.Description
TNLean/MPS/ParentHamiltonian/BNTBlockDiagonalPGVWCComparison.lean: rewrites module docstrings to describe β and ρ as cut-adapted boundary-word coordinates rather than "formal word" labels (9 lines changed, 9 deleted).blueprint/src/chapter/ch13_parent_hamiltonian_block_diagonal_chain_equality.tex: aligns blueprint prose for the PGVWC Cʲ, Dʲ boundary-comparison subsection to match cut-adapted framing (4 additions, 5 deletions).docs/paper-gaps/cpgsv21_block_diagonal_parent_ground_space.tex: updates paper-gap note terminology to reflect cut-adapted boundary-word framing (4 additions, 4 deletions).\lean{}tags, or proof logic are changed.Testing
lake build TNLean.MPS.ParentHamiltonian.BNTBlockDiagonalPGVWCComparison -q --log-level=infopython3 scripts/check_reader_facing_prose.py --root . --diff-base origin/mainpython3 scripts/blueprint_lean_sync.py --root . --ci(passed; no\lean{}tags changed)git diff --checkleanblueprint webleanblueprint checkdeclsnot run:blueprint/lean_declsnot generated in this worktree; no\lean{}tags changed, andblueprint_lean_sync.py --cipassed.lean_action_ci.yml) to validate the Lean build.Refs #2971
Refs #190
Refs #460
Note
Low Risk
Comment and prose edits only; no Lean proofs or formal statements are modified.
Overview
Aligns reader-facing wording for the PGVWC (C^j,D^j) boundary comparison so β and ρ are described as cut-adapted coordinates after opening the periodic cut, not as "formal word" or "word-indexed" labels.
The same terminology pass touches Lean module docstrings in
BNTBlockDiagonalPGVWCComparison.lean, the blueprint subsectionch13_parent_hamiltonian_block_diagonal_chain_equality.tex, and the paper-gap notecpgsv21_block_diagonal_parent_ground_space.tex. Prose now stresses boundary-indexed matrices in the source paper versus cut-adapted / blocked-word forms in the formalization. No theorem statements,\lean{}tags, or proof logic change.Reviewed by Cursor Bugbot for commit 03efbfa. Bugbot is set up for automated code reviews on this repo. Configure here.