fix(MPS/RFP): omit empty chain from product-pair bridge#3403
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.
Review Summary
This PR tightens the product-pair bridge predicates in CommutingBridge.lean by adding a 0 < N hypothesis to HasProductPairMPV, ProductPairBridge, AppendixBProductPairExtraction, and the core-tensor factorization adapter. The change excludes the empty-chain (N = 0) case where the MPV coefficient equals the bond dimension D while productPairState ψ₂ 0 is constantly 1 — a genuine mathematical mismatch that makes the old unrestricted predicate incorrect for any nontrivial bond dimension.
Findings by category
🔴 Proof integrity: No sorry, axiom, native_decide, or other blockers introduced. This is a pure hypothesis tightening; no proof obligations are added or weakened. ✅
🔴 Proof correctness: The mathematical justification is solid. mpv_zero_length confirms mpv A σ = (D : ℂ) at N = 0, while productPairState_zero confirms productPairState ψ₂ 0 = 1. The 0 < N guard correctly excludes this boundary mismatch. The source statement in arXiv:1606.00608 Appendix B applies only for a positive number of pairs, so the restriction is source-faithful. The ofCoreTensorFactorization adapter correctly threads the new hN through the rewrite. All downstream consumers (commuting_twoSite_localTerms, toProductPairBridge, isNNCPH) are unaffected because they use only the localProjectors field or propagate the hypothesis correctly. ✅
🟡 Mathlib style: No issues. Naming follows conventions, binder syntax ∀ N, 0 < N → ∀ σ is standard. ✅
🔴 Type safety: No type mismatches, universe issues, or coercion problems. ✅
🟡 Performance: No performance-affecting changes. ✅
🟡 Modularity & duplication: No new lemmas or duplication. ✅
🟡 Documentation: Docstrings for all changed definitions have been updated to explain the 0 < N restriction and the scope boundary relative to Appendix B. The **Scope restriction:** marker in HasProductPairMPV correctly follows the paper-realignment conventions in CLAUDE.md. ✅
🟡 Paper-gap notes: The changes to cpsv16_rfp_isometry_scope.tex and cpsv16_nncph_ground_state_scope.tex are minimal and accurate — replacing "even-chain" with "positive-even-chain" in two factual statements. Both notes remain self-contained mathematical accounts compliant with docs/paper-gaps/policy.tex. ✅
Verdict: APPROVE
All categories pass. No blocking issues found. The PR is a minimal, well-documented scope restriction that makes the formal predicates faithful to arXiv:1606.00608 Appendix B.
There was a problem hiding this comment.
Review: fix(MPS/RFP): omit empty chain from product-pair bridge
Verdict: Approve. No 🔴 or 🟡 issues found. This is a correct, well-scoped, well-documented fix.
Mathematical correctness — confirmed
The fix removes a genuinely false instance of the bridge predicate. The N = 0 case of the factorization mpv A σ = productPairState ψ₂ N σ is contradicted by two existing @[simp] lemmas:
mpv_zero_length(TNLean/MPS/Defs.lean:80): at length 0,mpv A σ = (D : ℂ), the bond dimension.productPairState_zero(TNLean/MPS/RFP/CommutingBridge.lean:83):productPairState ψ₂ 0 = fun _ => (1 : ℂ).
Hence the N = 0 obligation asserts (D : ℂ) = 1, false whenever D ≠ 1. The previous HasProductPairMPV, ProductPairBridge.hmpv, AppendixBProductPairExtraction.hmpv, and the core-tensor factorization field all silently demanded D = 1, making the bridge unsatisfiable for any honest multi-dimensional bond. Adding 0 < N excises exactly this case.
This direction also improves faithfulness rather than harming it: arXiv:1606.00608 Appendix B / Theorem 3.10 concerns a positive number of adjacent pairs, so the 0 < N guard matches the source boundary. Because these are scope-marked bridge predicates (not a Lean statement claimed as the source theorem), the change does not smuggle a hypothesis into a claimed source result and is consistent with the CLAUDE.md faithfulness rule.
Internal consistency — confirmed
The hmpv field has exactly two consumers, both updated correctly:
AppendixBProductPairExtraction.toProductPairBridge(CommutingBridge.lean:351) passeshExtract.hmpvthrough to the now-matchingProductPairBridge.hmpv.AppendixBProductPairExtraction.ofCoreTensorFactorization(CommutingBridge.lean:338–341) threads the newhN : 0 < Nbinder throughintro N hN σ/exact hCore N hN σ.
AppendixBStructuralData.mpv_eq_productPairState_one (CommutingBridge.lean:308) is unaffected (uses N = 1 directly).
Downstream — confirmed unaffected
ProductPairBridge.isNNCPH and the consumers in TNLean/MPS/ParentHamiltonian/Commuting.lean and TNLean/Axioms/Beigi.lean reach the commutation conclusion through localProjectors, never through hmpv, so no new proof obligations arise from the tightened binder.
Proof integrity
No new sorry / admit / axiom / native_decide / kernel bypass introduced; the diff only narrows binders and updates docstrings/prose.
Documentation & paper-gap notes
Docstring updates accurately explain the empty-chain exclusion and carry the **Scope restriction:** markers per the realignment convention, with the source cited (arXiv:1606.00608 Appendix B). The one-word edits to docs/paper-gaps/cpsv16_rfp_isometry_scope.tex and cpsv16_nncph_ground_state_scope.tex (even-chain → positive-even-chain) and the audit note preserve the notes' self-contained mathematical character per docs/paper-gaps/policy.tex. The remaining open factorization theorem is correctly described as unchanged and tracked in #3372.
Note: I could not run a full lake build here (TNLean oleans are not pre-built in this environment); the assessment above is from static analysis of the diff and its consumers. The PR reports the build and prose/sync checks passing.
There was a problem hiding this comment.
Blueprint & Prose Review
Category A — Blueprint ↔ Lean equivalence: no issues.
The 0 < N guard added to HasProductPairMPV, ProductPairBridge.hmpv, and AppendixBProductPairExtraction.hmpv is correctly reflected in the blueprint remark (rem:product_pair_projectors), which now says "for a positive number \lean{...} tags in the remark still resolve, the remark \leanok remains valid (no new sorry, declarations still exist), and the proof \leanok on thm:appendixB_product_pair_has_nncph_ground_spaces is unaffected because that proof reaches the commutation conclusion through localProjectors, not through hmpv.
Category B — Prose: 4 issues (REQUEST_CHANGES).
| # | File | Location | Issue |
|---|---|---|---|
| B1 | ch13_…tex |
line 659 | "bridge" as banned connection noun (§2) |
| B2 | ch13_…tex |
line 670 | "bridge" second occurrence (§2) |
| B3 | ch13_…tex |
lines 659–668 |
\(n\), \(n=0\), \(1\) mixed with $…$ in same paragraph (§1/§4) |
| B4 | CommutingBridge.lean |
line 95 | backtick around non-Lean-identifier (0,1), (2,3), ... (§1) |
| B5 | CommutingBridge.lean |
line 153 | "bridge data" as banned connection noun in docstring (§2) |
(Counts: 0 equivalence mismatches, 0 stale \leanok, 5 prose issues.)
![chatgpt-codex-connector[bot]](https://avatars.githubusercontent.com/in/1144995?s=60&v=4){kind=small}
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: 437e068a23
ℹ️ 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".
| (hStruct : AppendixBStructuralData A) where | ||
| /-- Even-chain coefficient factorization through the structural two-site amplitude. -/ | ||
| hmpv : ∀ N (σ : Cfg d (2 * N)), | ||
| /-- Positive even-chain coefficient factorization through the structural two-site amplitude. -/ |
There was a problem hiding this comment.
In this paper-realignment change, the 0 < N boundary is being added to an Appendix B factorization hypothesis, but the new field docstring does not cite the source passage. AGENTS.md requires every restated hypothesis field in paper-realignment mode to carry a source reference by paper label or line range, so without an Appendix B label/line citation here a reviewer cannot verify that the positive-pair restriction is faithful rather than invented.
Useful? React with 👍 / 👎.
There was a problem hiding this comment.
Blueprint ↔ Lean review — APPROVE
0 equivalence mismatches · 0 stale \leanok · 0 prose issues
Category A — Blueprint ↔ Lean equivalence and status
All five \lean{...}-tagged declarations whose signatures changed in this PR were checked against the remark rem:product_pair_projectors.
| Declaration | Blueprint | Lean | Match? |
|---|---|---|---|
HasProductPairMPV |
"for a positive number |
∀ N, 0 < N → ∀ σ |
✓ |
ProductPairBridge.hmpv |
"positive even-chain MPVs factor through…" | ∀ N, 0 < N → ∀ σ |
✓ |
AppendixBProductPairExtraction.hmpv |
"positive even-chain coefficient factorization" | ∀ N, 0 < N → ∀ σ |
✓ |
The \leanok on rem:product_pair_projectors is valid: all 26 listed declarations exist in the PR branch, CommutingBridge.lean and Commuting.lean contain no sorry/admit, and no new axioms were introduced.
The \notready tags on thm:rfp_implies_nncph and thm:rfp_implies_nncph_ground_state remain appropriate — those theorems depend on Axioms.rfp_to_nncph_commute, which is unchanged.
Category B — Prose quality
The five issues raised in the previous round (two "bridge"-as-connection-noun occurrences in blueprint prose, mixed \(...\)/$...$ notation in the newly edited paragraph, a backtick around an index-pair expression in a Lean docstring, and "bridge data" in the ProductPairBridge docstring) are all addressed in the synchronize commit:
- Blueprint: "adjacent-pair formal input" replaces both "bridge" noun uses; all new inline math uses
$...$consistently. - Lean docstring (
HasProductPairMPV):\((0,1),(2,3),\ldots\)replaces the backtick span. - Lean docstring (
ProductPairBridge): "Product-of-entangled-pairs hypotheses" replaces "bridge data".
No new banned terms or jargon were introduced in the changed text.
There was a problem hiding this comment.
Review summary — APPROVE
This is a small, well-scoped soundness/faithfulness fix that adds a 0 < N hypothesis to the adjacent product-pair factorization predicates in TNLean/MPS/RFP/CommutingBridge.lean. I reviewed it against the proof-integrity, correctness, style, type-safety, performance, modularity, documentation, and paper-gap criteria.
Proof integrity 🔴 — clean
No sorry, admit, axiom, native_decide, or kernel-bypass is introduced. The only proof body touched is AppendixBProductPairExtraction.ofCoreTensorFactorization, correctly updated from intro N σ / exact hCore N σ to intro N hN σ / exact hCore N hN σ.
Proof correctness 🔴 — change is mathematically correct and faithful
The dropped N = 0 case was genuinely false, so removing it is the right call:
mpv A σforσ : Cfg d (2 * 0) = Cfg d 0unfolds tocoeff A (List.ofFn σ) = coeff A [] = Matrix.trace (evalWord A []) = Matrix.trace (1 : Matrix (Fin D) (Fin D) ℂ) = (D : ℂ), the bond dimension (TNLean/MPS/Defs.lean:31-73).productPairState ψ₂ 0 σ = 1(empty product;productPairState_zero,CommutingBridge.lean:83-86).
These disagree whenever D ≠ 1, so the old ∀ N, ∀ σ, mpv A σ = productPairState ψ₂ N σ asserted a generally false equation at N = 0. Restricting to 0 < N (i.e. a positive number of pairs, each pair = 2 sites; the N = 1 case is discharged by mpv_eq_productPairState_one) is faithful to the arXiv:1606.00608 Appendix B product-of-entangled-pairs form, which is stated for a positive number of pairs. Per the project faithfulness rule this removes a false instance rather than adding a hypothesis, so it strengthens faithfulness.
No downstream breakage: hmpv is a data-only field. The consumed proof paths — AppendixBProductPairExtraction.commuting_twoSite_localTerms, ProductPairBridge.isNNCPH, and ProductPairBridge.hasNNCPHGroundSpaces_of_groundSpaceSpanning (ParentHamiltonian/Commuting.lean:365-371) — rely on localProjectors/isNNCPH, never on hmpv at a concrete N, so the arity change propagates cleanly. The blueprint and paper-gap prose (ch13_…, cpsv16_nncph_ground_state_scope.tex, cpsv16_rfp_isometry_scope.tex, audit note) are consistently updated to "positive-even-chain".
Style / type safety / performance / modularity 🟡 — no issues
Mechanical signature edits only; naming and structure unchanged. No new instances, coercions, or timeout-prone tactics.
Documentation 🟡 — adequate
The scope-restriction marker added to HasProductPairMPV (Appendix B produces a cyclic virtual-pair network; this predicate is the later adjacent-pair input and "is not, by itself, the full Appendix B factorization theorem") is exactly the right disclosure and matches the lighter-weight marker convention in CLAUDE.md.
Note on the open chatgpt-codex-connector P1 thread (left unresolved)
That comment asks for a per-field source citation on hmpv under the paper-realignment source-citation rule. I assess this as advisory, not blocking: (a) the 0 < N change removes a provably-false case rather than aligning an invented hypothesis to a passage, and (b) the source passage is already cited in the immediate documentation context — the enclosing structure docstrings name arXiv:1606.00608 Theorem 3.10 and Appendix B, and the module docstring gives the precise source line ranges (543–555, 1307). Adding arXiv:1606.00608, Appendix B to the hmpv field docstring would be a nice completeness touch but is not required for merge.
All previously-raised claude[bot] prose threads (banned "bridge" usages, mixed $…$/\(…\) notation, backtick-around-non-identifier) are already addressed in the latest commit and resolved.
No 🔴 or 🟡 issues remain. Approving.
There was a problem hiding this comment.
Review Summary
What this PR does
Adds a 0 < N hypothesis to HasProductPairMPV, ProductPairBridge, AppendixBProductPairExtraction, and ofCoreTensorFactorization in CommutingBridge.lean, excluding the empty-chain case (N=0) where the MPV coefficient is the bond dimension D but productPairState evaluates to 1 — making the old universal quantifier mathematically false.
Findings by category
| Category | Status |
|---|---|
| 🔴 Proof integrity | ✅ Clean — no sorry, admit, axiom, native_decide, or unsafeCast in changed files |
| 🔴 Proof correctness | ✅ Correct — the 0 < N restriction is mathematically justified; productPairState at N=0 is constant 1, while the empty-chain MPV yields D |
| 🟡 Mathlib style | ✅ Naming conventions, tactic style, and structure follow project conventions |
| 🔴 Type safety | ✅ No type/universe/coercion issues |
| 🟡 Performance | ✅ Hypothesis-only change; no new complex proofs or decide/simp chains at risk |
| 🟡 Modularity & duplication | ✅ No duplication; clean minimal diff |
| 🟡 Documentation | ✅ Docstrings updated with explanations of the N=0 exclusion and scope restrictions |
| 🟡 Paper-gap notes | ✅ Both notes updated accurately: "even-chain" → "positive-even-chain" |
Previous bot review comments
All 5 previous claude[bot] review comments on commit 62b4492 (prose style violations) were addressed in commit 437e068 and have been resolved.
Build
lake build TNLean.MPS.RFP.CommutingBridge TNLean.MPS.ParentHamiltonian.Commuting passes cleanly (8669 jobs).
Verdict: APPROVE — the change is a correct and well-documented hypothesis tightening with no blockers.
2 participants
Motivation
N = 0), where the MPS coefficient equals the bond dimension while the empty adjacent-pair product evaluates to1. The two expressions disagree, making theN = 0case a false statement.0 < Nhypothesis makes the Lean predicate faithful to this boundary.N ≥ 1— is tracked in Prove Appendix B even-chain product-pair factorization #3372.Description
TNLean/MPS/RFP/CommutingBridge.lean: added0 < Nhypothesis toHasProductPairMPV,ProductPairBridge,AppendixBProductPairExtraction, and core-tensor factorization field; docstrings updated to explain the exclusion of the empty chain.blueprint/src/chapter/ch13_parent_hamiltonian_commuting_gap.tex: blueprint prose aligned to the tightened adjacent-pair bridge statement.docs/paper-gaps/cpsv16_rfp_isometry_scope.tex,docs/paper-gaps/cpsv16_nncph_ground_state_scope.tex: gap notes updated to record the remaining source boundary.docs/audits/2026-04-21_issue234_commuting_parent_hamiltonian_gap.md: audit note updated.Testing
lake build TNLean.MPS.RFP.CommutingBridge TNLean.MPS.ParentHamiltonian.Commutinglake env lean TNLean/MPS/RFP/CommutingBridge.leanpython3 scripts/check_reader_facing_prose.py --root . --diff-base origin/main --cipython3 scripts/blueprint_lean_sync.py --root . --diff-base origin/main --cirg -n '\bsorry\b|\badmit\b|\bnative_decide\b|\bunsafeCast\b|^\s*axiom\b' TNLean/MPS/RFP/CommutingBridge.lean TNLean/MPS/ParentHamiltonian/Commuting.lean || trueRefs #3372
Note
Low Risk
Predicate and documentation tightening only; no proof logic or axiom changes beyond excluding an incorrect
N = 0case.Overview
The adjacent product-pair bridge now requires a positive number of pairs (
0 < N) in every even-chain MPV factorization hypothesis (HasProductPairMPV,ProductPairBridge,AppendixBProductPairExtraction, and core-tensor factorization). That drops theN = 0case, where the empty-chain MPV is bond dimension butproductPairStateis constantly1.Docstrings and blueprint/audit/gap prose are aligned: wording shifts to adjacent product-pair input, explains why the empty chain is excluded, and notes that Appendix B's cyclic virtual-pair form still has to be identified with this bridge input—the open factorization theorem is unchanged.
Reviewed by Cursor Bugbot for commit 62b4492. Bugbot is set up for automated code reviews on this repo. Configure here.
Note
Low Risk
Predicate and documentation tightening only; no axiom or proof-path changes beyond dropping an unsound
N = 0case.Overview
The adjacent product-pair bridge predicates now require
0 < N(a positive number of adjacent pairs) in every even-chain MPV factorization hypothesis:HasProductPairMPV,ProductPairBridge,AppendixBProductPairExtraction, andofCoreTensorFactorization. That removesN = 0, where the empty-chain MPV is bond dimension butproductPairStateis constantly1, so the old universal quantifier was unsound.Lean docstrings and blueprint/audit/gap prose are aligned: wording emphasizes adjacent pairs, explains the empty-chain exclusion, and notes that matching Appendix B’s cyclic virtual-pair form to this bridge input remains the open factorization step (unchanged scope).
Reviewed by Cursor Bugbot for commit 437e068. Bugbot is set up for automated code reviews on this repo. Configure here.