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

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

* doc(parent): expand three-site lift blueprint proof

* style(ParentHamiltonian): simplify local term lift proofs

---------

Co-authored-by: Sirui Lu <texra-ai@outlook.com>

Author: LionSR

TNLean/MPS/ParentHamiltonian/LocalSupport.lean

@@ -156,6 +156,58 @@ def rightPairLift (Q : NSiteSpace d 2 →ₗ[ℂ] NSiteSpace d 2) :
   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.
 

blueprint/src/chapter/ch13_parent_hamiltonian_commuting_gap.tex

@@ -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
+    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}
+
 \begin{definition}[Translated parent-term commutation]\label{def:is_commuting_parent_ham}
     \lean{MPSTensor.IsCommutingParentHam}
     \leanok
@@ -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.
+    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.
     \]
@@ -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.