Skip to content

feat(MPS/ParentHamiltonian): identify three-site parent lifts #3406

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
LionSR merged 3 commits into from
Jun 22, 2026
Merged

feat(MPS/ParentHamiltonian): identify three-site parent lifts #3406

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
3 commits
Select commit Hold shift + click to select a range
dcef502
feat(MPS/ParentHamiltonian): identify three-site parent lifts
texra-ai Jun 22, 2026
6ce0da6
doc(parent): expand three-site lift blueprint proof
texra-ai Jun 22, 2026
dc55fb1
style(ParentHamiltonian): simplify local term lift proofs
texra-ai Jun 22, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
52 changes: 52 additions & 0 deletions TNLean/MPS/ParentHamiltonian/LocalSupport.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -150,12 +150,64 @@
ext ψ σ
simp [Module.End.mul_apply]

@[simp] theorem rightPairLift_mul

Check warning on line 153 in TNLean/MPS/ParentHamiltonian/LocalSupport.lean

View workflow job for this annotation

GitHub Actions / Check blueprint compiles without errors

Blueprint update suggested 

MPSTensor.rightPairLift_mul is changed in this PR but has no corresponding \lean{} tag in blueprint/src/chapter.
(Q R : NSiteSpace d 2 →ₗ[ℂ] NSiteSpace d 2) :
rightPairLift (Q * R) = rightPairLift Q * rightPairLift R := by
ext ψ σ
simp [Module.End.mul_apply]

variable {D : ℕ}

/-- On a three-site window, the translated length-two parent interaction at
the first site is the \(AX\) lift of the two-site parent interaction. -/
@[simp]
theorem localTerm_two_three_zero_eq_leftPairLift_parentInteraction
(A : MPSTensor d D) :
localTerm A 2 3 (0 : Fin 3) = leftPairLift (parentInteraction A 2) := by
ext ω σ
have hExtract : extractWindow 2 (0 : Fin 3) σ = axPairCfg σ := by
funext j
fin_cases j <;> rfl
have hPi :
((LinearMap.pi fun τ : Cfg d 2 =>
(LinearMap.proj (replaceWindow 2 (by decide : 2 ≤ 3) (0 : Fin 3) σ τ) :
NSiteSpace d 3 →ₗ[ℂ] ℂ)) (Pi.single ω (1 : ℂ))) =
(fun α : Cfg d 2 =>
((Pi.single ω (1 : ℂ) : NSiteSpace d 3) (replaceAXCfg σ α))) := by
funext τ
have hWindow :
replaceWindow 2 (by decide : 2 ≤ 3) (0 : Fin 3) σ τ =
replaceAXCfg σ τ := by
funext k
fin_cases k <;> rfl
simp [hWindow]
simp [localTerm, leftPairLift, hExtract, hPi]

/-- On a three-site window, the translated length-two parent interaction at
the second site is the \(XB\) lift of the two-site parent interaction. -/
@[simp]
theorem localTerm_two_three_one_eq_rightPairLift_parentInteraction
(A : MPSTensor d D) :
localTerm A 2 3 (1 : Fin 3) = rightPairLift (parentInteraction A 2) := by
ext ω σ
have hExtract : extractWindow 2 (1 : Fin 3) σ = xbPairCfg σ := by
funext j
fin_cases j <;> rfl
have hPi :
((LinearMap.pi fun τ : Cfg d 2 =>
(LinearMap.proj (replaceWindow 2 (by decide : 2 ≤ 3) (1 : Fin 3) σ τ) :
NSiteSpace d 3 →ₗ[ℂ] ℂ)) (Pi.single ω (1 : ℂ))) =
(fun β : Cfg d 2 =>
((Pi.single ω (1 : ℂ) : NSiteSpace d 3) (replaceXBCfg σ β))) := by
funext τ
have hWindow :
replaceWindow 2 (by decide : 2 ≤ 3) (1 : Fin 3) σ τ =
replaceXBCfg σ τ := by
funext k
fin_cases k <;> rfl
simp [hWindow]
simp [localTerm, rightPairLift, hExtract, hPi]

/-- The algebraic part of the source nearest-neighbor parent-commuting condition
on one tripartite window.

Expand Down
53 changes: 47 additions & 6 deletions blueprint/src/chapter/ch13_parent_hamiltonian_commuting_gap.tex
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -56,6 +56,45 @@ \section{Translated parent-term commutation}\label{sec:commuting_parent_ham}
the middle site.
\end{definition}

\begin{theorem}[Three-site translated parent terms]
\label{thm:local_term_two_three_ax_xb_lifts}
\lean{MPSTensor.localTerm_two_three_zero_eq_leftPairLift_parentInteraction}
\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

@claude claude Bot Jun 22, 2026

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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 parent

and similarly \(\sigma=(a,x,b)\) → $\sigma=(a,x,b)$ in the proof.

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
interactions are the two local actions
\[
h^{(3)}_0(A,2)=q(A)_{AX},\qquad
h^{(3)}_1(A,2)=q(A)_{XB}.
\]
This identifies the two translated parent interactions with the two
supports appearing in \cite[Definition~D.2]{Cirac2016MPDO_arXiv}; it does
not assert that they commute.
\end{theorem}

\begin{proof}\leanok
Let \(\sigma=(a,x,b)\) be a three-site configuration. For the first
translated term, the length-two window and the corresponding replacement
satisfy
\[
\sigma_{\{0,1\}}=(a,x)=\sigma_{AX},\qquad
\sigma^{\{0,1\}\leftarrow(\alpha,\xi)}
=(\alpha,\xi,b)=\sigma^{AX\leftarrow(\alpha,\xi)}.
\]
For the second translated term,
\[
\sigma_{\{1,2\}}=(x,b)=\sigma_{XB},\qquad
\sigma^{\{1,2\}\leftarrow(\xi,\beta)}
=(a,\xi,\beta)=\sigma^{XB\leftarrow(\xi,\beta)}.
\]
Substituting these two pairs of identities into the definition of the
translated parent term gives the two displayed equations.
\end{proof}
Comment thread
claude[bot] marked this conversation as resolved.

\begin{definition}[Translated parent-term commutation]\label{def:is_commuting_parent_ham}
\lean{MPSTensor.IsCommutingParentHam}
\leanok
Expand Down Expand Up @@ -669,8 +708,13 @@ \section{Translated parent-term commutation}\label{sec:commuting_parent_ham}
Appendix~B first gives a cyclic virtual-pair expression; identifying that
expression with this adjacent-pair formal input is part of the remaining
factorization theorem.
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.

@claude claude Bot Jun 22, 2026

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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$

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\)
satisfying
\[
h_i(A,2)=p_i,\qquad p_i^2=p_i,\qquad p_ip_j=p_jp_i.
\]
Expand All @@ -681,10 +725,7 @@ \section{Translated parent-term commutation}\label{sec:commuting_parent_ham}
which is the nearest-neighbor commuting conclusion for every finite chain.
The even-chain factorization and the two-site projector identification are
the inputs supplied by Appendix~B of \cite{Cirac2016MPDO_arXiv}; given them,
the local terms commute. The three-site $AX/XB$ support maps of
Definition~\ref{def:overlapping_two_site_supports} record the local action
of the adjacent projectors, but the theorem identifying those projectors with
the translated parent terms remains open. Together with
the local terms commute. Together with
Lemma~\ref{lem:parent_hamiltonian_ff}, the product-pair input also gives the
zero-energy equation for $V^{(N)}(A)$, still without asserting the source
ground-space spanning condition.
Expand Down
Loading