feat(MPS/RFP): add unit pair-index structural form#3388
Conversation
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.
Blueprint & Prose Review — PR 3388
Category A (blueprint ↔ Lean equivalence): 0 issues.
Both new declarations check out:
rfp_nt_structural_full_unit_pair— blueprint and Lean hypotheses match (IsNormal,IsRFP, left-canonicalhLeft); conclusions agree: invertibleX, positiveΛ, the unit pair-index identity∑ᵢ star(Uᵢ_{pq}) · Uᵢ_{p'q'} = δ_{pp'}, and the conjugation form. The deliberate omission of∑ᵢ (Uᵢ)† Uᵢ = I(present in the parent) is correct for the rescaledUand is consistently absent from both blueprint and Lean.rfp_nt_structural_full_blocks_unit_pair— blockwise version; same analysis holds per block.- All
\leanoktags (statement and proof) are valid: both Lean proofs aresorry-free and the\lean{...}tags resolve.
Category B (prose quality): 4 issues — see inline comments.
| # | Location | Rule | Issue |
|---|---|---|---|
| B1 |
ch14_correlations.tex proof of thm:rfp_nt_structural_full_unit_pair
|
§"Source-faithful … formula-first" | "the pair-index equation loses the factor |
| B2 |
StructuralFull.lean line 446 |
§1 — prefer mathematical phrasing |
`rfp_nt_structural_full` used as a cross-reference rather than a mathematical description |
| B3 |
StructuralFull.lean lines 457–458 |
§1 — source-reference shorthand banned |
`eq:III_isometry` is a LaTeX source label, not a Lean identifier; backtick-wrapping it is the banned shorthand pattern |
| B4 |
StructuralFull.lean line 593 |
§1 — prefer mathematical phrasing |
`rfp_nt_structural_full_blocks` used as a cross-reference; same issue as B2 |
B3 is the clearest violation (a LaTeX internal label in backticks). B1 is required by the formula-first rule. B2 and B4 are the softer "use sparingly, prefer mathematical phrasing" guidance — easy to fix with a one-line edit each.
docs/paper-gaps/cpsv16_rfp_isometry_scope.tex was reviewed but is out of scope (developer-facing notes in docs/).
There was a problem hiding this comment.
Review: feat(MPS/RFP): add unit pair-index structural form
Thank you — the mathematics of the new theorems is correct. rfp_nt_structural_full_unit_pair rescales U₀ ↦ √D·U₀, Λ₀ ↦ Λ₀/√D, leaving the product Λ U (hence A^i = X Λ U^i X⁻¹) invariant while turning the pair-index sum from D⁻¹·δ into the unit δ. The (star s * s) = D cancellation, the positivity Λ₀ k / √D > 0, and the s • L/s • U₀ regrouping all check out. Crucially, the new theorem correctly drops the ∑ᵢ (Uⁱ)ᴴ Uⁱ = 1 conjunct, since in the rescaled convention that contracted identity is D·I, not I. Hypotheses match the parent rfp_nt_structural_full exactly — no smuggled assumptions — and the blueprint/Lean both honestly state that trace-normalization and cross-block orthogonality remain out of scope. Faithfulness rule satisfied.
One 🟡 issue blocks approval (paper-gap note precision), plus two smaller documentation/style points. Details inline.
🟡 Paper-gap note — verdict conflates two normalization conventions
In docs/paper-gaps/cpsv16_rfp_isometry_scope.tex §Conclusion, the sentence claiming the development "exposes both" the contracted identity ∑ᵢ (U_k^i)† U_k^i = I and the unit pair-index orthonormality reads as if both hold for one U_k. They hold for different tensors (the D_k^{-1/2}-normalized U_k of ..._blocks vs. the √D_k-rescaled U_k of ..._blocks_unit_pair, where the contracted identity is D_k·I). Per policy.tex §Classification ("a precise verdict") this should be made convention-explicit. See inline comment.
🟡 Documentation — scope-restriction marker omitted
The parent rfp_nt_structural_full_blocks carries an inline **Scope restriction (source isometry):** marker pointing at the paper-gap note (per CLAUDE.md §Locally-fixable deviations). The two new theorems are equally scope restrictions of Corollary III.cor3 / eq:III_isometry but use only free prose. For greppable consistency, add the marker. See inline comment.
ℹ️ Advisory — unused destructured hypothesis
hU₀_left is bound by the obtain but never used in the new proof; replacing it with _ avoids an unused-variable linter warning.
Note on verification
I verified the proof mathematically; a full lake env lean type-check was not possible here because the layer-5b dependency oleans for StructuralFull.lean are not prebuilt in this environment. The PR reports a successful lake build TNLean.MPS.RFP.StructuralFull; please ensure CI confirms it.
Verdict: REQUEST_CHANGES — resolve the paper-gap note precision and add the scope-restriction markers.
There was a problem hiding this comment.
Review: feat(MPS/RFP): add unit pair-index structural form
This is a third-party review confirming and extending findings from two prior bot reviews. The mathematics is correct — the rescaling U₀ ↦ √D·U₀, Λ₀ ↦ Λ₀/√D preserves the product Λ U (hence the decomposition A^i = X Λ U^i X⁻¹) while turning the pair-index sum from D⁻¹·δ into the unit δ. The (star s * s) = D cancellation, the positivity argument Λ₀ k / √D > 0, and the s • L/s • U₀ regrouping all check out. The new theorem correctly drops the ∑ᵢ (Uⁱ)ᴴ Uⁱ = 1 conjunct that is not preserved under the rescaling.
🔴 Proof Integrity — No issues.
No sorry, admit, axiom, native_decide, or unsafeCast present in the diff. Build passes (lake build TNLean.MPS.RFP.StructuralFull succeeds).
🔴 Proof Correctness — One advisory issue.
Lines 472–473 (StructuralFull.lean): The obtain block binds hU₀_left from rfp_nt_structural_full, but hU₀_left is never used in the proof. Replace with _ to avoid potential linter warnings. (Also flagged by a prior review.)
🔴 Type Safety — No issues.
No type mismatches, universe issues, or coercion problems. Complex/real conversions are handled correctly with Complex.ofReal_mul, Complex.ofReal_div, exact_mod_cast, etc.
🟡 Mathlib Style — No issues.
Naming follows conventions (camelCase, descriptive names). Tactic usage is appropriate (calc, simp with explicit lemma lists, rw, positivity). No unnecessary opens.
🟡 Performance — No issues.
The proofs use focused simp with explicit lemma sets, calc blocks of moderate depth, and a single positivity call. No risk of decide on large types or unbounded simp.
🟡 Modularity & Duplication — No issues.
The new theorems are genuinely new statements (different normalization convention). No duplication of existing Mathlib results.
🟡 Documentation — Two issues (blocking).
-
Lines 593–597 (
StructuralFull.lean) —rfp_nt_structural_full_blocks_unit_pairdocstring: The docstring is brief and neither references the paper-gap note (docs/paper-gaps/cpsv16_rfp_isometry_scope.tex) nor carries a formal**Scope restriction (**)**marker. The parent theoremrfp_nt_structural_full_blockshas a full scope-restriction marker at lines 568–576 linking to the paper-gap note. PerCLAUDE.md§Locally-fixable-deviations, this marker format is required for greppable consistency. Must be fixed before merge. -
Lines 445–459 (
StructuralFull.lean) —rfp_nt_structural_full_unit_pairdocstring: The docstring describes what is not proved in prose and references the paper-gap note, which is good. However, for consistency withrfp_nt_structural_full_blocks, it should also carry the formal**Scope restriction (source isometry):**marker format that explicitly names the missing conditions (tr(Λ)=1, cross-block orthogonality) and links to the paper-gap note. The content is already present; only the marker format needs to be added. (Also flagged by a prior review.) Must be fixed before merge. -
Lines 10–35 (
StructuralFull.lean) — Module docstring: The module docstring describes the main result (rfp_nt_structural_full) and proof strategy. It should be updated to mention that the file also provides the unit pair-index variantsrfp_nt_structural_full_unit_pairandrfp_nt_structural_full_blocks_unit_pair, since they are now first-class theorems in this file.
🟡 Paper-gap Notes — One issue (blocking).
Lines 141–143 of docs/paper-gaps/cpsv16_rfp_isometry_scope.tex §Conclusion:
"The formal development now exposes both the contracted per-block identity ∑_i (U_k^i)^† U_k^i = I and the diagonal pair-index orthonormality in the unit source convention."
Per policy.tex §Classification, the verdict should be "convention-explicit." The contracted identity ∑ (U_k^i)^† U_k^i = I holds for the D_k^{-1/2}-scaled U_k of rfp_nt_structural_full_blocks, while the unit pair-index orthonormality holds for the √D_k-rescaled U_k of rfp_nt_structural_full_blocks_unit_pair. These are different tensors related by rescaling. The current phrasing reads as if both properties hold simultaneously for one U_k. Clarify by adding a phrase like "across the two conventions" or distinguishing which property holds under which normalization choice. (Also flagged by a prior review.) Must be fixed before merge.
Out of Scope (per review instructions)
Blueprint ↔ Lean sync and prose quality are handled by the dedicated Blueprint & Prose Review workflow. Prior reviews flagged prose issues (B1–B4) that remain unaddressed.
Verdict: REQUEST_CHANGES — resolve the documentation scope-restriction markers and the paper-gap note precision before approval.
There was a problem hiding this comment.
Blueprint ↔ Lean Sync & Prose Review — synchronize pass
All 7 threads from the previous round were resolved above (marked outdated in the updated diff; confirmed fixed).
Category A — Blueprint ↔ Lean equivalence
thm:rfp_nt_structural_full_unit_pair
- Hypotheses match:
IsNormal A("normal"),IsRFP A("renormalization fixed point"),hLeft : ∑ i, (A i)ᴴ * A i = 1("canonical form II"). ✓ - Conclusion matches: decomposition
$A^i = X\Lambda U^i X^{-1}$ withX.det ≠ 0, all diagonal entries positive, pair-index equation$= \delta_{\alpha\alpha'}\delta_{\beta\beta'}$ encoded asif p = q then 1 else 0. ✓ -
\leanokon statement and proof: nosorryin the proof body. ✓ -
\uses{thm:rfp_nt_structural_full}correctly lists the one dependency. ✓
thm:rfp_nt_structural_full_blocks_unit_pair
- Blockwise lift of the above; blueprint's "under the hypotheses of Theorem~\ref{thm:rfp_nt_structural_full_blocks}" matches the Lean universal over
k. ✓ \leanokon statement and proof: proof isfun k => rfp_nt_structural_full_unit_pair (A k) ...; nosorry. ✓\uses{thm:rfp_nt_structural_full_unit_pair}correct. ✓
0 equivalence mismatches. 0 stale \leanok.
Category B — Prose quality
- Blueprint proof sketch now displays the rescaling calculation
$D \cdot D^{-1},\delta_{\alpha\alpha'}\delta_{\beta\beta'} = \delta_{\alpha\alpha'}\delta_{\beta\beta'}$ explicitly. ✓ - Docstrings use LaTeX cross-references
(Theorem~\ref{...})instead of bare Lean identifiers. ✓ - Source citations use
arXiv:1606.00608, lines 550--554rather than internal label shorthand. ✓ - Both docstrings carry the
**Scope restriction (source isometry):**marker with paper-gap reference. ✓ -
docs/paper-gaps/update separates the two normalization conventions clearly (each convention's contracted identity and pair-index equation stated for its own$U_k$ ). ✓ - No banned software-engineering terms, no LLM filler patterns, no bare Lean jargon in blueprint prose. ✓
0 prose issues.
Verdict: APPROVE. 0 equivalence mismatches, 0 stale status tags, 0 prose issues.
There was a problem hiding this comment.
Review: feat(MPS/RFP): add unit pair-index structural form (re-review after 6bb9949)
The second commit addressed all issues from the prior three review cycles. The mathematics is correct and the documentation is now precise.
Resolved prior issues
All 7 prior bot review threads have been addressed:
- Blueprint proof now displays the explicit D * D^{-1} * delta = delta calculation
- Lean identifier cross-references replaced with Theorem ref
- eq:III_isometry shorthand replaced with line-range citation
- Paper-gap note now clearly distinguishes D_k^{-1/2} vs sqrt(D_k) conventions
- Scope restriction markers added to both new theorems
- Unused hU0_left hypothesis replaced with underscore
Category-by-category assessment
- Proof integrity: No sorry, admit, axiom, native_decide, or unsafeCast.
- Proof correctness: The rescaling Lambda = Lambda0 / sqrt(D), U = sqrt(D) * U0 preserves Lambda * U = Lambda0 * U0 (hence A^i = X * Lambda * U^i * X^{-1}) while transforming the pair-index sum from D^{-1} * delta to the unit delta via star(sqrt(D)) * sqrt(D) = D cancellation. The new theorems correctly drop the sum (U^i)^H * U^i = 1 conjunct that would become D * I under rescaling. All real/complex conversions are correct.
- Mathlib style: Naming follows conventions (snake_case for theorems). Tactic usage is appropriate (calc, focused simp, positivity). No unnecessary opens.
- Type safety: No type mismatches or coercion issues. Real.sqrt, Complex.ofReal_*, and exact_mod_cast are used correctly.
- Performance: Proofs use focused simp with explicit lemma sets; no risk of timeouts.
- Modularity & duplication: The new theorems are genuinely new statements (different normalization convention). No duplication.
- Documentation: Both theorems have comprehensive docstrings with displayed equations, Scope restriction markers, and paper-gap note references. Hypotheses match the parent exactly.
- Paper-gap notes: The updated conclusion now gives a convention-explicit verdict per policy.tex: the contracted identity = I holds in the D_k^{-1/2} convention while the unit pair-index orthonormality holds in the rescaled convention where the contracted identity is instead D_k * I. Remaining gaps (tr(Lambda) = 1 and cross-block orthogonality) are clearly identified.
Verdict: APPROVE — no blocker or requires-changes issues remain.
There was a problem hiding this comment.
Review summary — APPROVE
This PR adds two unit-pair-index variants of the RFP structural isometry theorems plus matching blueprint and paper-gap documentation. All issues raised in the previous review cycle have been addressed by the new commits, and I find no new blocking or change-requiring issues.
Proof integrity 🔴 — clean
No sorry, admit, native_decide, unsafeCast, or axiom in TNLean/MPS/RFP/StructuralFull.lean (the rg hits are the English word "admits" in docstrings, not the admit tactic). Both new theorems, MPSTensor.rfp_nt_structural_full_unit_pair and MPSTensor.rfp_nt_structural_full_blocks_unit_pair, are fully proved.
Proof correctness 🔴 — sound
rfp_nt_structural_full_unit_pair is a clean rescaling of rfp_nt_structural_full: it sets Λ ↦ Λ₀/√D, U ↦ √D · U₀. The three obligations are each discharged with explicit calc blocks:
- Positivity of
Λfromdiv_pos (hΛ₀_pos k) hsR_pos. - Unit pair-index sum:
∑ᵢ star(U i p) · U i q = (star s · s) · ∑ᵢ star(U₀ i p) · U₀ i q = D · (if p=q then D⁻¹ else 0) = if p=q then 1 else 0, usinghs_star : star s · s = (D:ℂ)(sinces = (√D : ℝ)and√D·√D = D). Correct. - Decomposition preservation:
diag(Λ₀)·U₀ = (s • L)·U₀ = L·(s • U₀) = diag(Λ)·U, soAⁱ = X·diag(Λ)·Uⁱ·X⁻¹survives. Correct.
The blueprint proof body now shows the explicit D·D⁻¹ cancellation rather than a verbal summary, addressing the earlier comment.
Type safety 🔴 — clean
D : ℕ with [NeZero D]; hD_ne, hDpos, hsR_ne are all derived from it. The per-block variant correctly threads [∀ k, NeZero (dim k)]. No universe or coercion concerns.
Faithfulness / paper-gap note 🟡 — satisfied
Both theorems are scope restrictions of Corollary III.cor3, properly marked inline with **Scope restriction (source isometry):**, and recorded in docs/paper-gaps/cpsv16_rfp_isometry_scope.tex. Reviewed against docs/paper-gaps/policy.tex: the note is self-contained, introduces its notation, cites the source (arXiv:1606.00608, MPDO-22-12-17-2.tex:543–554 and :583–589), and now gives a precise verdict that cleanly separates the two conventions — the =I and unit orthonormality simultaneously. The note correctly continues to flag the two genuinely open items: source trace-normalization eq:III_isometry.
Documentation / style 🟡 — satisfied
Both new declarations carry docstrings with mathematical meaning and scope markers; theorem names are snake_case; line length within limits.
Prior review threads
All 7 previously-open claude threads (the unused hU₀_left now bound as _, the paper-gap conflation, the missing scope markers, and the prose threads) are addressed by the new commits and have been resolved.
Note on validation
Mathlib oleans are not cached in this environment, so I did not run a full lake build; the assessment rests on close reading plus the author's stated lake build TNLean.MPS.RFP.StructuralFull TNLean.MPS.RFP.CommutingBridge. The proofs are elementary rescaling arguments with no fragile automation.
No outstanding 🔴 or 🟡 issues.
2 participants
Motivation
rfp_nt_structural_full(arXiv:1606.00608, Appendix B, lines 543-555) carries a(D : ℂ)⁻¹-scaled pair-index orthonormality, whereas the source states the unit Kronecker-delta condition. This mismatch is documented indocs/paper-gaps/cpsv16_rfp_isometry_scope.texand blocks elimination of therfp_to_nncph_commuteaxiom via theAppendixBProductPairExtractionroute; see Prove Appendix B even-chain product-pair factorization #3372 as a sub-task of Pure-state equivalence RFP = ZCL = NNCPH ground state (arXiv:1606.00608, thm:main-MPS, line 534) #2633.Description
MPSTensor.rfp_nt_structural_full_unit_pair(TNLean/MPS/RFP/StructuralFull.lean): derives fromrfp_nt_structural_fullby rescaling Λ ↦ Λ / √D and U ↦ √D · U, preserving the decomposition A^i = XΛU^iX⁻¹ while expressing the pair-index sum as δ_{α,α'}δ_{β,β'}.rfp_nt_structural_full_blocks_unit_pair: per-block companion theorem.blueprint/src/chapter/ch14_correlations.texwith matching blueprint entries in Chapter 14.docs/paper-gaps/cpsv16_rfp_isometry_scope.texto record that the scalar normalization comparison is now explicit; trace normalization (tr Λ = 1) and cross-block orthogonality (arXiv:1606.00608, eq. III_isometry) remain open.hCore(N >= 2) is a follow-up.Testing
lake build TNLean.MPS.RFP.StructuralFull TNLean.MPS.RFP.CommutingBridgepython3 scripts/check_reader_facing_prose.py --root . --diff-base origin/main --cipython3 scripts/blueprint_lean_sync.py --root . --diff-base origin/main --cigit diff --check origin/main...HEADrg -n '\bsorry\b|\badmit\b|\bnative_decide\b|\bunsafeCast\b|\baxiom\b' TNLean/MPS/RFP/StructuralFull.lean TNLean/MPS/RFP/CommutingBridge.lean || trueRefs #3372
Note
Low Risk
Pure Mathlib rescaling proofs and doc/blueprint sync on top of an existing theorem; no runtime or security-sensitive code.
Overview
Adds unit pair-index variants of the RFP structural isometry theorems so the formal statements match the Cirac et al. convention where the pair-index sum equals Kronecker deltas (not scaled by (D^{-1})).
In Lean,
rfp_nt_structural_full_unit_pairis proved fromrfp_nt_structural_fullby rescaling (\Lambda \mapsto \Lambda/\sqrt{D}) and (U \mapsto \sqrt{D},U), keeping (A^i = X\Lambda U^i X^{-1}) while rewriting the pair-index orthonormality.rfp_nt_structural_full_blocks_unit_pairapplies the same per block. Chapter 14 blueprint entries anddocs/paper-gaps/cpsv16_rfp_isometry_scope.texnow document both normalization conventions explicitly; trace normalization and cross-block isometry remain out of scope.Reviewed by Cursor Bugbot for commit 6bb9949. Bugbot is set up for automated code reviews on this repo. Configure here.