feat(MPS/ParentHamiltonian): identify three-site parent lifts#3406
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 — APPROVE
A tightly-scoped, correct PR. It adds two lemmas identifying the translated length-two parent terms on a three-site chain with the AX/XB lifts of the canonical two-site parent interaction, plus a matching blueprint theorem.
Proof integrity 🔴 — clean
No sorry, admit, axiom, native_decide, or unsafeCast introduced. Both proofs are complete tactic proofs.
Proof correctness 🔴 — verified by hand
I checked the four index identities underlying localTerm_two_three_zero_eq_leftPairLift_parentInteraction and localTerm_two_three_one_eq_rightPairLift_parentInteraction against extractWindow/replaceWindow in TNLean/MPS/ParentHamiltonian/Defs.lean:87,101 and axPairCfg/xbPairCfg/replaceAXCfg/replaceXBCfg in LocalSupport.lean:30–49:
extractWindow 2 0 σ = σ⟨0⟩,σ⟨1⟩ = axPairCfg σ✓replaceWindow 2 _ 0 σ τ: offset(k+3)%3 = k, usesτiffk<2= replaceAXCfg σ τ✓extractWindow 2 1 σ = σ⟨1⟩,σ⟨2⟩ = xbPairCfg σ✓replaceWindow 2 _ 1 σ τ: offset(k+2)%3→k=0↦σ, k=1↦τ₀, k=2↦τ₁ = replaceXBCfg σ τ✓
Each is discharged by fin_cases <;> rfl, which is sound on these finite Fin 2/Fin 3 domains. The proof structure (ext on the Pi-basis Pi.single ω 1, then the hExtract/hPi reductions feeding simp [localTerm, …]) follows a clear logical strategy rather than a brute-force tactic chain.
Faithfulness — respected
The two Lean conclusions are reproduced verbatim by the new blueprint theorem thm:local_term_two_three_ax_xb_lifts, with no added hypotheses. The statement is correctly scoped: it identifies the translated parent terms with the AX/XB lifts of parentInteraction A 2 and explicitly does not assert Q_{AX}Q_{XB}=Q_{XB}Q_{AX} or the Definition D.2 kernel-intersection condition. The Appendix B remark update keeps the projector construction, their commutation, and the D.2 condition as explicit open work, so no source theorem is over-claimed.
Type safety / performance — no concerns
Small finite enumerations only; no large decide, unbounded simp sets, or symbolic norm_num.
Documentation — present
Both new theorems carry docstrings stating the mathematical meaning; the module docstring already frames the AX/XB support layer.
ℹ️ Advisory (non-blocking)
@[simp]on fully-concrete instances (LocalSupport.lean:163,191): both lemmas only fire on the literal patternlocalTerm A 2 3 0/localTerm A 2 3 1. Simp-normalizing a maximally-specialized literal instance is unusual — these read more like named rewrite lemmas for the downstream commutation argument. The direction is sound and non-looping (RHS contains nolocalTerm), so it is acceptable; consider dropping@[simp]unless a downstreamsimpcall relies on automatic firing.- Minor proof verbosity (the
hPi/hWindowblocks): the innerchange … ; rw [hWindow]restatesreplaceWindow 2 _ i σ τ = replaceAXCfg/replaceXBCfg σ τafter already proving it byfunext k; fin_cases k <;> rfl; the funext could close the goal directly. Purely cosmetic.
Blueprint \lean{}/\leanok/\uses{} sync and prose quality are out of scope here (handled by the dedicated Blueprint Sync & Prose Review workflow); no paper-gap notes were touched.
Only advisory items remain, so this is approvable.
There was a problem hiding this comment.
Review Summary
Verdict: REQUEST_CHANGES — one 🟡 style issue to fix before approval.
Changes reviewed
TNLean/MPS/ParentHamiltonian/LocalSupport.lean(+58 lines): Two new@[simp]lemmas proving three-site translated parent-term identities:localTerm_two_three_zero_eq_leftPairLift_parentInteraction: (h_0^{(3)}(A,2) = q(A)_{AX})localTerm_two_three_one_eq_rightPairLift_parentInteraction: (h_1^{(3)}(A,2) = q(A)_{XB})
blueprint/src/chapter/ch13_parent_hamiltonian_commuting_gap.tex(+34/−6 lines): New Theorem "Three-site translated parent terms" with\leanoktags; updated Appendix B product-pair remark.
Per-category findings
🔴 Proof integrity: ✅ PASS. No sorry, axiom, admit, native_decide, unsafeCast, or circular reasoning. The by decide for 2 ≤ 3 is proper.
🔴 Proof correctness: ✅ PASS. The extractWindow/replaceWindow ↔ axPairCfg/replaceAXCfg identifications are correct for the three-site chain (fin_cases exhausts all cases). The localTerm expansion interacts correctly with the leftPairLift/rightPairLift definitions.
🟡 Mathlib style: ❌ Two occurrences of fragile change tactic (lines 183, 211). Both LinearMap.pi_apply and LinearMap.coe_proj are @[simp] lemmas in Mathlib (LinearAlgebra/Pi.lean:61 and :92), so simp [hWindow] would close the goal without the brittle syntactic matching that change requires. This must be fixed before merge.
🔴 Type safety: ✅ PASS. Variables {d : ℕ} and {D : ℕ} are correctly scoped. The NSiteSpace abbreviation resolves to Cfg d N → ℂ.
🟡 Performance: ✅ PASS. fin_cases k <;> rfl for Fin 3 has 3 cases. No expensive computations.
🟡 Modularity & duplication: ℹ️ Advisory. The extractWindow/axPairCfg and replaceWindow/replaceAXCfg (and XB variants) equivalences are proved inline within the hExtract and hWindow blocks. Extracting them as reusable @[simp] lemmas (e.g., extractWindow_two_three_zero_eq_axPairCfg) would make future proofs shorter. Acceptable as-is since the PR is scoped to these two lemmas.
🟡 Documentation: ✅ PASS. Both lemmas have docstrings that state the mathematical meaning in (h_i^{(N)}) notation. The blueprint theorem is documented with prose proof sketch.
🟡 Paper-gap notes: N/A — no paper-gap notes were changed.
Mathematical faithfulness
The Lean statements faithfully match the cited source (arXiv:1606.00608 §3.3 and Appendix B). The blueprint theorem thm:local_term_two_three_ax_xb_lifts correctly states that these are the AX/XB lift identifications, and explicitly notes that commutation is not asserted yet — matching the PR scope documented in the description.
There was a problem hiding this comment.
Blueprint & Prose Review — PR 3406
Category A — Blueprint ↔ Lean equivalence: ✅ no issues
The single new blueprint theorem (thm:local_term_two_three_ax_xb_lifts) carries two \lean{...} tags, one per conjunct, covering both equalities stated in the display. Checked:
-
A.1 Mathematical equivalence.
localTerm A 2 3 (0 : Fin 3)= $h^{(3)}0(A,2)$,leftPairLift (parentInteraction A 2)= $q(A){AX}$ with$q(A)=1-P_{G_2(A)}$ (matchesDefs.leanlines 71–77). Likewise for the XB conjunct. Signatures match the blueprint on quantifiers, hypotheses, and conclusion. -
A.2
\leanokaccuracy. Statement\leanok: both Lean declarations resolve and match. Proof\leanok: neither proof body containssorryoradmit. Both tags are valid. -
A.3
\notready: not present; not applicable. -
A.4
\uses{}accuracy.\uses{def:overlapping_two_site_supports, def:local_term_parent}correctly names the two dependencies (leftPairLift/rightPairLiftlive indef:overlapping_two_site_supports;localTermindef:local_term_parent).
The updated "product-pair remark" prose accurately reflects that the AX/XB identification is now done while projector identification and
Category B — Prose quality: 🔴 2 issues
| # | Location | Rule | Finding |
|---|---|---|---|
| B1 | ch13…tex line 75 |
§1 source-reference shorthand | Definition~D.2 without \cite{} — line 54 of the same file already writes \cite[Definition~D.2]{Cirac2016MPDO_arXiv}; the new theorem text drops the citation wrapper |
| B2 | ch13…tex lines 78–83 |
§"Source-faithful terminology" — formula-driven proof sketches | Word-only proof sketch; the two pointwise equalities that carry the argument ($\sigma |
Verdict: REQUEST_CHANGES — 0 equivalence mismatches, 0 stale \leanok, 2 prose issues (1 missing citation, 1 formula-free proof sketch).
There was a problem hiding this comment.
Summary
Category A (blueprint ↔ Lean equivalence): no issues.
The new theorem thm:local_term_two_three_ax_xb_lifts is linked to two Lean declarations whose signatures exactly match the blueprint statement — localTerm A 2 3 (0 : Fin 3) = leftPairLift (parentInteraction A 2) and localTerm A 2 3 (1 : Fin 3) = rightPairLift (parentInteraction A 2). Quantifiers, site labelling (Fin 3 / {A,X,B}), and conclusions all match. Both Lean proofs are complete (no sorry), so both \leanok tags (statement and proof) are valid. The \uses{def:overlapping_two_site_supports, def:local_term_parent} entries are appropriate. The updated remark text is accurate about what the theorem does and does not prove.
Category B (prose quality): 2 issues.
Both are inline-math convention violations per docs/prose_style.md:
- New theorem block (lines 59–96): uses
\(...\)throughout — new blueprint prose must use$...$. - Edited remark paragraph (lines 711–716): inserts
\(...\)into a paragraph whose existing text uses$...$, creating a mixed paragraph.
0 equivalence mismatches · 0 stale \leanok · 2 inline-math convention violations.
| \lean{MPSTensor.localTerm_two_three_one_eq_rightPairLift_parentInteraction} | ||
| \leanok | ||
| \uses{def:overlapping_two_site_supports, def:local_term_parent} | ||
| Put \(q(A)=1-P_{G_2(A)}\) for the canonical two-site parent interaction. On |
There was a problem hiding this comment.
Category B — §"In blueprint files" inline-math convention: new theorem block uses \(...\) instead of $...$
docs/prose_style.md states: "In blueprint files, use $...$ for inline mathematics in new prose." The surrounding definitions and remarks in this file use $...$ (e.g. $i$ and $i+1$, $L$ on $N$ sites, $V^{(N)}(A)$). The entire new theorem and proof block (lines 59–96) uses \(...\) throughout.
Suggested fix — replace \(...\) with $...$ in the theorem statement and proof, for example:
- Put \(q(A)=1-P_{G_2(A)}\) for the canonical two-site parent interaction. On
- the three-site space
- \(\mathcal H_A\otimes\mathcal H_X\otimes\mathcal H_B\), with sites
- \(0,1,2\) labelled \(A,X,B\), the two adjacent translated length-two parent
+ Put $q(A)=1-P_{G_2(A)}$ for the canonical two-site parent interaction. On
+ the three-site space
+ $\mathcal H_A\otimes\mathcal H_X\otimes\mathcal H_B$, with sites
+ $0,1,2$ labelled $A,X,B$, the two adjacent translated length-two parentand similarly \(\sigma=(a,x,b)\) → $\sigma=(a,x,b)$ in the proof.
| The two-site parent projectors must also be identified with | ||
| idempotents $p_i$ satisfying | ||
| On a three-site chain, the two adjacent length-two parent terms are the | ||
| \(AX\) and \(XB\) actions of the canonical two-site parent interaction. |
There was a problem hiding this comment.
Category B — §"In blueprint files" inline-math convention: \(...\) inserted into a $...$ paragraph
docs/prose_style.md: "Do not mix $...$ and \(...\) in a newly edited paragraph; when touching an existing paragraph, prefer converting it to $...$ if the change is local."
The remark being edited (lines 705–731) uses $...$ throughout its existing text ($n=0$, $1$, $V^{(N)}(A)$). The new insertion uses \(AX\), \(XB\), \(Q_{AX}Q_{XB}=Q_{XB}Q_{AX}\), \(p_i\) — creating a mixed paragraph.
The old deleted sentence used $AX/XB$, confirming the paragraph's native convention. The fix is to write the new insertion in $...$:
- On a three-site chain, the two adjacent length-two parent terms are the
- \(AX\) and \(XB\) actions of the canonical two-site parent interaction.
- What remains from Appendix~B is to identify the projectors determined by the
- product-of-pairs form with these canonical parent interactions and to prove
- \(Q_{AX}Q_{XB}=Q_{XB}Q_{AX}\). For the all-chain statement, the resulting
- two-site parent projectors must be identified with idempotents \(p_i\)
+ On a three-site chain, the two adjacent length-two parent terms are the
+ $AX$ and $XB$ actions of the canonical two-site parent interaction.
+ What remains from Appendix~B is to identify the projectors determined by the
+ product-of-pairs form with these canonical parent interactions and to prove
+ $Q_{AX}Q_{XB}=Q_{XB}Q_{AX}$. For the all-chain statement, the resulting
+ two-site parent projectors must be identified with idempotents $p_i$
There was a problem hiding this comment.
Review summary — REQUEST_CHANGES
One 🟡 Mathlib style issue from the previous review cycle remains unfixed and blocks approval.
Changes since previous review (commit dcef502 → 6ce0da6)
The fixup commit addressed two of the four findings from the earlier reviews:
- ✅ Blueprint citation fix —
Definition~D.2→\cite[Definition~D.2]{Cirac2016MPDO_arXiv}(previously flagged as 🔴 prose issue B1). Resolved. - ✅ Blueprint proof sketch formulas — the word-only proof sketch was replaced with a formula-rich version displaying the four pointwise equalities that carry the argument (previously flagged as 🔴 prose issue B2). Resolved.
Still outstanding: 🟡 change tactic fragility (lines 183–186, 211–214)
The two change + rw [hWindow] blocks in hPi are still present (first flagged in the style review at dcef502). These are fragile — change requires exact syntactic matching that breaks silently if Mathlib redefines LinearMap.pi or LinearMap.proj.
Moreover, the change is entirely redundant here: LinearMap.pi and LinearMap.proj are defined with toFun forms that make (LinearMap.pi f) x i and (proj i) f definitionally equal to f i x and f i respectively. After funext τ, the goal is already definitionally:
(Pi.single ω 1) (replaceWindow 2 (by decide : 2 ≤ 3) i σ τ)
= (Pi.single ω 1) (replaceA*Cfg σ τ)
So the fix is simpler than previously suggested — just delete the change line and keep only rw [hWindow] (or equivalently simp [hWindow]):
-- line 183: replace the `change … + rw [hWindow]` block
simp [hWindow]Same for line 211.
This must be fixed before merge per Mathlib style conventions (§ Mathlib style in the review rubric).
Per-category status
| Category | Severity | Status |
|---|---|---|
| 🔴 Proof integrity | Blocker | ✅ Clean — no sorry/axiom/admit/unsafeCast |
| 🔴 Proof correctness | Blocker | ✅ Verified — extractWindow/replaceWindow identifications correct for the 3-site chain; fin_cases exhausts all cases |
| 🟡 Mathlib style | Requires changes | ❌ Two change + rw blocks (lines 183–186, 211–214) need replacing with rw [hWindow] or simp [hWindow] |
| 🔴 Type safety | Blocker | ✅ Clean |
| 🟡 Performance | Requires changes | ✅ No expensive computations |
| 🟡 Modularity | Requires changes | ℹ️ Advisory — hWindow and hExtract could be extracted as reusable lemmas (acceptable as-is) |
| 🟡 Documentation | Requires changes | ✅ Both lemmas have docstrings; blueprint theorem documented |
| 🟡 Paper-gap notes | Requires changes | N/A — no paper-gap files changed |
There was a problem hiding this comment.
Review Summary — REQUEST_CHANGES
A tightly-scoped, mathematically correct PR. It adds two @[simp] lemmas on
TNLean/MPS/ParentHamiltonian/LocalSupport.lean identifying the translated
length-two parent terms on a three-site chain with the AX/XB pair lifts of
the canonical two-site parent interaction parentInteraction A 2, plus a
matching blueprint theorem thm:local_term_two_three_ax_xb_lifts.
What I verified this cycle
- Build:
lake build TNLean.MPS.ParentHamiltonian.LocalSupportsucceeds
(only pre-existing header/style warnings in imported files). - Proof integrity 🔴 — clean: no
sorry,admit,axiom,
native_decide, orunsafeCast. - Proof correctness 🔴 — confirmed against the definitions in
TNLean/MPS/ParentHamiltonian/Defs.lean. For
localTerm_two_three_zero_eq_leftPairLift_parentInteraction:
extractWindow 2 0 σ = (σ⟨0⟩, σ⟨1⟩) = axPairCfg σ, and the offset
(k + 3 − 0) % 3 = kmakesreplaceWindow 2 _ 0 σ τuseτiffk < 2,
i.e.= replaceAXCfg σ τ. For the site-1 lemma, offset(k + 3 − 1) % 3
sendsk = 0 ↦ σ,k = 1 ↦ τ₀,k = 2 ↦ τ₁, i.e.
replaceWindow 2 _ 1 σ τ = replaceXBCfg σ τ, and
extractWindow 2 1 σ = (σ⟨1⟩, σ⟨2⟩) = xbPairCfg σ. All four discharged by
fin_cases <;> rfloverFin 2/Fin 3. ThelocalTerm/leftPairLift
expansion fed tosimpis sound. - Faithfulness — respected. The blueprint theorem reproduces the two Lean
conclusions verbatim with no added hypotheses, and explicitly states it does
not assertQ_{AX}Q_{XB} = Q_{XB}Q_{AX}or the
\cite[Definition~D.2]{Cirac2016MPDO_arXiv}kernel-intersection condition.
No source theorem is over-claimed.
🟡 Outstanding — must be fixed before approval
Fragile change tactic in both new lemmas
(localTerm_two_three_zero_eq_leftPairLift_parentInteraction, lines 183–186;
localTerm_two_three_one_eq_rightPairLift_parentInteraction, lines 211–214).
This was flagged in the two prior review cycles and remains unaddressed in the
pushed commits. The change … ; rw [hWindow] block depends on exact syntactic
matching of the LinearMap.pi / LinearMap.proj unfolding and silently
restates replaceWindow 2 _ i σ τ = replaceAXCfg/replaceXBCfg σ τ after it has
already been proved by funext k; fin_cases k <;> rfl.
I verified locally that replacing each change … ; rw [hWindow] block with a
single
simp [hWindow]still compiles (lake build TNLean.MPS.ParentHamiltonian.LocalSupport succeeds)
— LinearMap.pi_apply and LinearMap.coe_proj are @[simp] in Mathlib, so the
reduction is robust and shorter. This must be fixed before merge. (See the two
existing inline threads on lines 183 and 211.)
ℹ️ Advisory (non-blocking)
@[simp]on fully-concrete instances (lines 163, 191): both lemmas fire
only on the literal patternlocalTerm A 2 3 0/localTerm A 2 3 1. The
rewrite direction is non-looping (RHS has nolocalTerm), so it is harmless;
consider whether@[simp]is needed or these are better left as named
rewrite lemmas for the downstream commutation argument.
Out of scope here
Blueprint ↔ Lean \lean{}/\leanok/\uses{} sync and blueprint prose quality
(the citation-wrapper and formula-driven-proof-sketch items raised previously)
are handled by the dedicated Blueprint Sync & Prose Review workflow; I leave
those threads to that workflow. No paper-gap notes under docs/paper-gaps/
were changed.
Verdict: REQUEST_CHANGES — the 🟡 fragile-change style issue remains
unresolved.
There was a problem hiding this comment.
Review update (synchronize)
Fixed since last review — threads resolved:
- The
change …+rw [hWindow]fragility in both lemma proofs is gone; both now usesimp [hWindow]directly. ✓
Category A — blueprint ↔ Lean equivalence: no issues
The two new Lean theorems match the blueprint statement exactly:
localTerm A 2 3 (0 : Fin 3) = leftPairLift (parentInteraction A 2)↔h^{(3)}_0(A,2)=q(A)_{AX}localTerm A 2 3 (1 : Fin 3) = rightPairLift (parentInteraction A 2)↔h^{(3)}_1(A,2)=q(A)_{XB}
The description q(A)=1-P_{G_2(A)} agrees with the parentInteraction docstring ("Mathematically, h_L = 𝟙 - P_{G_L(A)}"). Both Lean proofs are sorry-free; the \leanok tags on statement and proof are valid.
Category B — 2 prose issues remain open
Threads PRRT_kwDORK8b986LaP19 and PRRT_kwDORK8b986LaP_7 are unresolved:
-
\(...\)vs$...$in the new theorem block (thm:local_term_two_three_ax_xb_lifts, lines 65–82): the entire theorem statement and proof still use\(...\).docs/prose_style.mdrequires$...$for inline mathematics in new blueprint prose. -
\(...\)vs$...$in the edited remark (lines 708–715): the four new inline expressions (\(AX\),\(XB\),\(Q_{AX}Q_{XB}=Q_{XB}Q_{AX}\),\(p_i\)) are inserted into a paragraph that uses$...$throughout its existing text, creating a mixed paragraph against the style guide's explicit instruction.
Summary: 0 equivalence mismatches, 0 stale \leanok, 2 open prose issues (inline-math convention). Requesting changes on the prose issues.
There was a problem hiding this comment.
Review Summary — ✅ APPROVE
All 🔴 and 🟡 issues from prior review cycles have been resolved. No new issues found.
Changes since previous review
The fixup commit addressed the two outstanding findings:
- ✅ 🟡
changetactic fragility (lines 183, 211) — replacedchange … + rw [hWindow]withsimp [hWindow]in both lemmas. TheLinearMap.pi_applyandLinearMap.coe_projlemmas are@[simp]in Mathlib, so this reduction is robust and idiomatic.
Per-category final status
| Category | Severity | Status |
|---|---|---|
| 🔴 Proof integrity | Blocker | ✅ No sorry, axiom, admit, native_decide, or unsafeCast. by decide on 2 ≤ 3 is proper. |
| 🔴 Proof correctness | Blocker | ✅ Verified — extractWindow/replaceWindow ↔ axPairCfg/replaceAXCfg (and XB variants) identifications are exhaustive via fin_cases over Fin 3 and Fin 2. The simp finales correctly unfold localTerm, leftPairLift, and rightPairLift. |
| 🟡 Mathlib style | Requires changes | ✅ simp [hWindow] fix applied. snake_case naming follows conventions. Docstrings present. |
| 🔴 Type safety | Blocker | ✅ Clean — {d : ℕ}, {D : ℕ} correctly scoped; no universe or coercion issues. |
| 🟡 Performance | Requires changes | ✅ fin_cases over small Fin types is negligible. simp sets are bounded. |
| 🟡 Modularity | Requires changes | ℹ️ Advisory — hExtract and hWindow could be extracted as reusable @[simp] lemmas (e.g., extractWindow_two_three_zero_eq_axPairCfg). Acceptable as-is for this scoped PR. |
| 🟡 Documentation | Requires changes | ✅ Both lemmas have docstrings stating the mathematical meaning in (h_i^{(N)}) notation. Blueprint theorem documented with formula-rich proof sketch. |
| 🟡 Paper-gap notes | Requires changes | N/A — no paper-gap files changed. |
Mathematical faithfulness
The Lean statements faithfully match the cited source (arXiv:1606.00608 §3.3 and Appendix B). The blueprint theorem thm:local_term_two_three_ax_xb_lifts correctly states the AX/XB lift identifications, explicitly notes that commutation is NOT asserted, and cites \cite[Definition~D.2]{Cirac2016MPDO_arXiv} correctly. No source theorem is over-claimed.
Resolved threads
Previously-resolved bot threads (citation fix, proof-sketch formulas) remain resolved. Two change-tactic threads (PRRT_kwDORK8b986LaJzM, PRRT_kwDORK8b986LaJ0w) resolved in this cycle — the code now uses simp [hWindow] as recommended.
There was a problem hiding this comment.
Review Summary — APPROVE
The single outstanding 🟡 issue from the prior review cycles — the fragile change + rw [hWindow] block in both new lemmas — has been resolved. Lines 183 and 208 of TNLean/MPS/ParentHamiltonian/LocalSupport.lean now use a single simp [hWindow], which reduces the LinearMap.pi / LinearMap.proj application robustly via the @[simp] Mathlib lemmas LinearMap.pi_apply / LinearMap.coe_proj rather than relying on exact syntactic matching.
Verified this cycle
- Build 🔴 —
lake build TNLean.MPS.ParentHamiltonian.LocalSupportsucceeds (only pre-existinglinter.style.header"Copyright too short" warnings in imported files). - Proof integrity 🔴 — clean: no
sorry,admit,axiom,native_decide, orunsafeCast. - Proof correctness 🔴 — re-confirmed against the definitions in
Defs.leanandLocalSupport.lean:localTerm_two_three_zero_eq_leftPairLift_parentInteraction:extractWindow 2 0 σ = (σ⟨0⟩, σ⟨1⟩) = axPairCfg σ; and the offset(k + 3 − 0) % 3 = kmakesreplaceWindow 2 _ 0 σ τpickτexactly whenk < 2, i.e.= replaceAXCfg σ τ.localTerm_two_three_one_eq_rightPairLift_parentInteraction:extractWindow 2 1 σ = (σ⟨1⟩, σ⟨2⟩) = xbPairCfg σ; and the offset(k + 3 − 1) % 3sendsk=0 ↦ σ,k=1 ↦ τ₀,k=2 ↦ τ₁, i.e.replaceWindow 2 _ 1 σ τ = replaceXBCfg σ τ.- All four pointwise identities discharged by
fin_cases <;> rfloverFin 2/Fin 3.
- Faithfulness — respected. The blueprint theorem
thm:local_term_two_three_ax_xb_liftsreproduces the two Lean conclusions with no added hypotheses and explicitly states it does not assertQ_{AX}Q_{XB} = Q_{XB}Q_{AX}or the\cite[Definition~D.2]{Cirac2016MPDO_arXiv}kernel-intersection condition. No source theorem is over-claimed. - Type safety / performance 🔴🟡 — clean;
fin_casesruns over tinyFin 2/Fin 3enumerations.
ℹ️ Advisory (non-blocking)
@[simp]on the fully-concrete instanceslocalTerm A 2 3 0/localTerm A 2 3 1(lines 163, 188): the rewrite is non-looping (RHS contains nolocalTerm), so it is harmless; consider whether plain named rewrite lemmas serve the downstream commutation argument better.
Out of scope here
The remaining unresolved inline threads concern blueprint prose only — \(...\) vs $...$ inline-math delimiters and proof-sketch formula support. These are handled by the dedicated Blueprint Sync & Prose Review workflow and are left to it.
Verdict: APPROVE — all previously-raised in-scope 🔴/🟡 issues are resolved.
2 participants
Motivation
(Q_{AX}) and (Q_{XB}) with translated length-two parent Hamiltonian terms before
their commutation can be established; see also Definition D.2 and gap notes
docs/paper-gaps/cpsv16_nncph_ground_state_scope.texanddocs/paper-gaps/cpsv16_parent_commuting_hamiltonian_scope.tex.local-support layer (PRs feat(MPS/ParentHamiltonian): add overlapping local support lifts #3384 and refactor(MPS/RFP): use unit Appendix B structural datum #3389) toward the all-chain
HasProductPairLocalProjectorswitness; see also Pure-state equivalence RFP = ZCL = NNCPH ground state (arXiv:1606.00608, thm:main-MPS, line 534) #2633 and Tracking: sanctioned axiom inventory and elimination #3375.Description
TNLean/MPS/ParentHamiltonian/LocalSupport.lean(+58 lines): adds two@[simp]lemmasproving that on a three-site chain the translated length-two parent terms at sites 0 and 1
equal the left and right pair lifts of the canonical two-site parent interaction
(q(A) = 1 - P_{G_2(A)}):
localTerm_two_three_zero_eq_leftPairLift_parentInteraction: (h_0^{(3)}(A,2) = q(A)_{AX})localTerm_two_three_one_eq_rightPairLift_parentInteraction: (h_1^{(3)}(A,2) = q(A)_{XB})blueprint/src/chapter/ch13_parent_hamiltonian_commuting_gap.tex(+34/−6 lines): records ablueprint theorem for the three-site translated parent term identities with Lean links;
updates the Appendix B product-pair remark so the AX/XB identification is marked done
while the Appendix B projector construction, their commutation
((Q_{AX}Q_{XB} = Q_{XB}Q_{AX})), and the Definition D.2 kernel-intersection condition remain
explicit future work.
Definition D.2 kernel-intersection condition, or supply the all-chain
HasProductPairLocalProjectorswitness.Testing
lake exe cache get && lake build TNLean.MPS.ParentHamiltonian.LocalSupport— succeeds;only pre-existing header/style warnings in imported files.
python3 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/ParentHamiltonian/LocalSupport.lean || true— no new sorry.lean_action_ci.yml) validates the full build.Addresses #3373
Note
Low Risk
Formal identification lemmas and blueprint sync only; no changes to axioms, runtime code, or commutation proofs.
Overview
Proves that on a three-site chain, translated length-two parent terms at sites 0 and 1 match the (AX) and (XB) lifts of the canonical two-site parent interaction (q(A)=1-P_{G_2(A)}).
In
LocalSupport.lean, two new@[simp]lemmas (localTerm_two_three_zero_eq_leftPairLift_parentInteractionandlocalTerm_two_three_one_eq_rightPairLift_parentInteraction) showlocalTerm A 2 3 0/1equalsleftPairLift/rightPairLiftofparentInteraction A 2, by aligningextractWindow/replaceWindowwithaxPairCfg/xbPairCfgand the pair-replacement maps.The blueprint adds Theorem “Three-site translated parent terms” with Lean links and a short proof sketch, and revises the Appendix B product-pair remark so this AX/XB identification is done while projector construction, (Q_{AX}Q_{XB}=Q_{XB}Q_{AX}), and the all-chain witness remain open.
Reviewed by Cursor Bugbot for commit dc55fb1. Bugbot is set up for automated code reviews on this repo. Configure here.