From dcef502df1473f76316880c148d846aa654f7bd1 Mon Sep 17 00:00:00 2001 From: Sirui Lu Date: Mon, 22 Jun 2026 23:55:43 +0200 Subject: [PATCH 1/3] feat(MPS/ParentHamiltonian): identify three-site parent lifts --- .../MPS/ParentHamiltonian/LocalSupport.lean | 58 +++++++++++++++++++ .../ch13_parent_hamiltonian_commuting_gap.tex | 40 +++++++++++-- 2 files changed, 92 insertions(+), 6 deletions(-) diff --git a/TNLean/MPS/ParentHamiltonian/LocalSupport.lean b/TNLean/MPS/ParentHamiltonian/LocalSupport.lean index 0303911d8..a732f8aa5 100644 --- a/TNLean/MPS/ParentHamiltonian/LocalSupport.lean +++ b/TNLean/MPS/ParentHamiltonian/LocalSupport.lean @@ -156,6 +156,64 @@ 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 + change (Pi.single ω (1 : ℂ) : NSiteSpace d 3) + (replaceWindow 2 (by decide : 2 ≤ 3) (0 : Fin 3) σ τ) = + (Pi.single ω (1 : ℂ) : NSiteSpace d 3) (replaceAXCfg σ τ) + rw [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 + change (Pi.single ω (1 : ℂ) : NSiteSpace d 3) + (replaceWindow 2 (by decide : 2 ≤ 3) (1 : Fin 3) σ τ) = + (Pi.single ω (1 : ℂ) : NSiteSpace d 3) (replaceXBCfg σ τ) + rw [hWindow] + simp [localTerm, rightPairLift, hExtract, hPi] + /-- The algebraic part of the source nearest-neighbor parent-commuting condition on one tripartite window. diff --git a/blueprint/src/chapter/ch13_parent_hamiltonian_commuting_gap.tex b/blueprint/src/chapter/ch13_parent_hamiltonian_commuting_gap.tex index 6f24bc107..8ba706db1 100644 --- a/blueprint/src/chapter/ch13_parent_hamiltonian_commuting_gap.tex +++ b/blueprint/src/chapter/ch13_parent_hamiltonian_commuting_gap.tex @@ -56,6 +56,32 @@ \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 Definition~D.2; it does not assert that they commute. +\end{theorem} + +\begin{proof}\leanok + For the first translated term, the length-two window extracts the + \(AX\)-coordinates and replacing that window is the same as replacing the + \(AX\)-face while leaving \(B\) fixed. For the second translated term, the + window extracts the \(XB\)-coordinates and replacement leaves \(A\) fixed. +\end{proof} + \begin{definition}[Translated parent-term commutation]\label{def:is_commuting_parent_ham} \lean{MPSTensor.IsCommutingParentHam} \leanok @@ -669,8 +695,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 +712,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. From 6ce0da6beeac4fc5eb4400b1ee196dc5ab500af0 Mon Sep 17 00:00:00 2001 From: Sirui Lu Date: Tue, 23 Jun 2026 00:03:13 +0200 Subject: [PATCH 2/3] doc(parent): expand three-site lift blueprint proof --- .../ch13_parent_hamiltonian_commuting_gap.tex | 23 +++++++++++++++---- 1 file changed, 18 insertions(+), 5 deletions(-) diff --git a/blueprint/src/chapter/ch13_parent_hamiltonian_commuting_gap.tex b/blueprint/src/chapter/ch13_parent_hamiltonian_commuting_gap.tex index 8ba706db1..1a397121e 100644 --- a/blueprint/src/chapter/ch13_parent_hamiltonian_commuting_gap.tex +++ b/blueprint/src/chapter/ch13_parent_hamiltonian_commuting_gap.tex @@ -72,14 +72,27 @@ \section{Translated parent-term commutation}\label{sec:commuting_parent_ham} h^{(3)}_1(A,2)=q(A)_{XB}. \] This identifies the two translated parent interactions with the two - supports appearing in Definition~D.2; it does not assert that they commute. + supports appearing in \cite[Definition~D.2]{Cirac2016MPDO_arXiv}; it does + not assert that they commute. \end{theorem} \begin{proof}\leanok - For the first translated term, the length-two window extracts the - \(AX\)-coordinates and replacing that window is the same as replacing the - \(AX\)-face while leaving \(B\) fixed. For the second translated term, the - window extracts the \(XB\)-coordinates and replacement leaves \(A\) fixed. + 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} From dc55fb1bb08b7aec70342b839a7ac57ba06634a7 Mon Sep 17 00:00:00 2001 From: Sirui Lu Date: Tue, 23 Jun 2026 00:16:55 +0200 Subject: [PATCH 3/3] style(ParentHamiltonian): simplify local term lift proofs --- TNLean/MPS/ParentHamiltonian/LocalSupport.lean | 10 ++-------- 1 file changed, 2 insertions(+), 8 deletions(-) diff --git a/TNLean/MPS/ParentHamiltonian/LocalSupport.lean b/TNLean/MPS/ParentHamiltonian/LocalSupport.lean index a732f8aa5..8a7fcbfdb 100644 --- a/TNLean/MPS/ParentHamiltonian/LocalSupport.lean +++ b/TNLean/MPS/ParentHamiltonian/LocalSupport.lean @@ -180,10 +180,7 @@ theorem localTerm_two_three_zero_eq_leftPairLift_parentInteraction replaceAXCfg σ τ := by funext k fin_cases k <;> rfl - change (Pi.single ω (1 : ℂ) : NSiteSpace d 3) - (replaceWindow 2 (by decide : 2 ≤ 3) (0 : Fin 3) σ τ) = - (Pi.single ω (1 : ℂ) : NSiteSpace d 3) (replaceAXCfg σ τ) - rw [hWindow] + simp [hWindow] simp [localTerm, leftPairLift, hExtract, hPi] /-- On a three-site window, the translated length-two parent interaction at @@ -208,10 +205,7 @@ theorem localTerm_two_three_one_eq_rightPairLift_parentInteraction replaceXBCfg σ τ := by funext k fin_cases k <;> rfl - change (Pi.single ω (1 : ℂ) : NSiteSpace d 3) - (replaceWindow 2 (by decide : 2 ≤ 3) (1 : Fin 3) σ τ) = - (Pi.single ω (1 : ℂ) : NSiteSpace d 3) (replaceXBCfg σ τ) - rw [hWindow] + simp [hWindow] simp [localTerm, rightPairLift, hExtract, hPi] /-- The algebraic part of the source nearest-neighbor parent-commuting condition