refactor(MPS/RFP): use unit Appendix B structural datum

Author: texra-ai

TNLean/MPS/RFP/CommutingBridge.lean

@@ -31,13 +31,14 @@ The declarations below separate three mathematical statements:
   idempotents on each finite chain;
 * the already formalized Appendix B structural form.
 
-**Scope restriction (overlapping two-site terms):** The current \(N\)-site state
-space is a function space indexed by configurations. It does not yet expose the
-tensor-product support maps needed to state directly the source relation
-\([\tau_1(P_2),P_2]=0\) for the two overlapping nearest-neighbor terms. For this
-reason commutativity of the translated idempotents is an explicit hypothesis in
-`HasProductPairLocalProjectors`. Eliminating this hypothesis is the
-overlapping product-of-entangled-pairs locality step recorded in
+**Scope restriction (overlapping two-site terms):** The three-site support maps
+for the source \(AX\) and \(XB\) windows are now available in
+`TNLean.MPS.ParentHamiltonian.LocalSupport`. What is still missing is the
+Appendix-B theorem identifying the product-of-entangled-pairs parent projectors
+with the translated length-two parent terms and proving their overlapping
+commutation. For this reason commutativity of the translated idempotents is
+still an explicit hypothesis in `HasProductPairLocalProjectors`. Eliminating
+this hypothesis is the product-of-entangled-pairs locality step recorded in
 `docs/paper-gaps/cpsv16_nncph_ground_state_scope.tex`.
 -/
 
@@ -111,10 +112,12 @@ theorem HasProductPairMPV.exists_twoSiteAmplitude {A : MPSTensor d D}
 \(p_i\) associated to the adjacent two-site factors on an \(N\)-site chain, with
 \(p_i p_j=p_j p_i\).
 
-**Scope restriction (tensor-product locality):** The current formal state space
-does not yet carry the tensor-product support maps used in the source
-product-of-entangled-pairs argument, so the projectors are stated directly as
-endomorphisms of the full \(N\)-site space. -/
+**Scope restriction (local projectors):** The formal development now has the
+three-site \(AX/XB\) support maps for adjacent windows. This structure still does
+not construct, from the Appendix-B product-of-entangled-pairs form, the
+chain-level projectors that equal the translated length-two parent terms. The
+projectors are therefore still stated directly as endomorphisms of the full
+\(N\)-site space. -/
 structure HasProductPairLocalProjectors (A : MPSTensor d D) (N : ℕ) where
   proj : Fin N → NSiteSpace d N →ₗ[ℂ] NSiteSpace d N
   hidem : ∀ i, proj i * proj i = proj i
@@ -183,12 +186,12 @@ theorem ProductPairBridge.localTerm_idempotent
 /-! ### Appendix B structural form as the preceding input -/
 
 /-- Structure recording the Appendix B normal-tensor decomposition
-\(A^i=X\Lambda U^iX^{-1}\).
+\(A^i=X\Lambda U^iX^{-1}\) in the source unit pair-index convention.
 
-The theorem `rfp_nt_structural_full` proves existence of this structural form
-from the RFP, normality, and left-canonical hypotheses. The remaining
-product-of-entangled-pairs factorization and parent-term identities must use
-the same \(X,\Lambda,U\). -/
+The theorem `rfp_nt_structural_full_unit_pair` proves existence of this
+structural form from the RFP, normality, and left-canonical hypotheses. The
+remaining product-of-entangled-pairs factorization and parent-term identities
+must use the same \(X,\Lambda,U\). -/
 structure AppendixBStructuralData (A : MPSTensor d D) where
   /-- The virtual-bond change of basis. -/
   X : Matrix (Fin D) (Fin D) ℂ
@@ -200,15 +203,11 @@ structure AppendixBStructuralData (A : MPSTensor d D) where
   hX_det : X.det ≠ 0
   /-- The diagonal weights are strictly positive. -/
   hΛ_pos : ∀ k, 0 < Λ k
-  /-- The residual tensor is left-canonical. -/
-  hU_left : ∑ i : Fin d, (U i)ᴴ * U i = 1
-  /-- The residual tensor satisfies the normalized per-block pair-index
-  orthonormality condition. The normalization differs from the source's unit
-  pair-index convention as recorded in
-  `docs/paper-gaps/cpsv16_rfp_isometry_scope.tex`. -/
+  /-- The residual tensor satisfies the source unit pair-index orthonormality
+  condition from arXiv:1606.00608, lines 550--554, restricted to one block. -/
   hU_pair : ∀ p q : Fin D × Fin D,
     ∑ i : Fin d, star (U i p.1 p.2) * U i q.1 q.2 =
-      if p = q then (D : ℂ)⁻¹ else 0
+      if p = q then 1 else 0
   /-- The original tensor has the Appendix B structural form. -/
   hA_eq : ∀ i, A i = X * Matrix.diagonal (fun k => (Λ k : ℂ)) * U i * X⁻¹
 
@@ -218,15 +217,14 @@ theorem AppendixBStructuralData.exists_ofRFP (A : MPSTensor d D) [NeZero D]
     (hLeft : ∑ i : Fin d, (A i)ᴴ * A i = 1) :
     Nonempty (AppendixBStructuralData A) := by
   classical
-  obtain ⟨X, Λ, U, hX_det, hΛ_pos, hU_left, hU_pair, hA_eq⟩ :=
-    rfp_nt_structural_full A hNT hRFP hLeft
+  obtain ⟨X, Λ, U, hX_det, hΛ_pos, hU_pair, hA_eq⟩ :=
+    rfp_nt_structural_full_unit_pair A hNT hRFP hLeft
   exact ⟨
     { X := X
       Λ := Λ
       U := U
       hX_det := hX_det
       hΛ_pos := hΛ_pos
-      hU_left := hU_left
       hU_pair := hU_pair
       hA_eq := hA_eq }⟩
 
@@ -309,7 +307,7 @@ theorem AppendixBStructuralData.mpv_eq_productPairState_one {A : MPSTensor d D}
 /-- The remaining product-of-entangled-pairs input needed after Appendix B.
 
 For a fixed structural form, this captures the two facts that are still not
-produced internally by `rfp_nt_structural_full`: the even-chain MPV must be a
+produced by the Appendix-B structural datum: the even-chain MPV must be a
 repeated copy of the two-site amplitude determined by that same witness, and the
 nearest-neighbor parent projectors on each finite chain must be identified with a
 commuting family attached to these adjacent two-site factors. -/

blueprint/src/chapter/ch13_parent_hamiltonian_commuting_gap.tex

@@ -597,7 +597,8 @@ \section{Translated parent-term commutation}\label{sec:commuting_parent_ham}
 
 \begin{proof}
     \notready
-    \uses{thm:rfp_implies_nncph, lem:parent_hamiltonian_ff}
+    \uses{thm:rfp_implies_nncph, lem:parent_hamiltonian_ff,
+        def:overlapping_two_site_supports}
     Conditional on Theorem~\ref{thm:rfp_implies_nncph}, the first equation is
     immediate. The second is Lemma~\ref{lem:parent_hamiltonian_ff} with $L=2$.
 \end{proof}
@@ -638,6 +639,14 @@ \section{Translated parent-term commutation}\label{sec:commuting_parent_ham}
     \[
         A^i=X\Lambda U^iX^{-1}.
     \]
+    The residual tensor is now recorded in the source unit pair-index convention:
+    \[
+        \sum_i
+        \overline{(U^i)_{\alpha,\beta}}\,
+        (U^i)_{\alpha',\beta'}
+        =
+        \delta_{\alpha,\alpha'}\delta_{\beta,\beta'}.
+    \]
     The change of basis does not alter periodic MPS coefficients, so the
     corresponding two-site amplitude is
     \[
@@ -666,9 +675,13 @@ \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. Together with Lemma~\ref{lem:parent_hamiltonian_ff},
-    they also give the zero-energy equation for \(V^{(N)}(A)\), still without
-    asserting the source ground-space spanning condition.
+    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
+    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.
 \end{remark}
 
 \begin{theorem}[Product-pair data and ground-space spanning give all-chain NNCPH]%

docs/audits/2026-04-21_issue234_commuting_parent_hamiltonian_gap.md

@@ -111,10 +111,10 @@ into
 - a family of chain-level projectors whose values are exactly the nearest-neighbor `localTerm`s.
 
 This is a genuine chain-space construction problem on `NSiteSpace d N`; it is **not** a remaining
-issue about the NNCPH definition itself. The present `AppendixBStructuralData` record still exposes
-only the left-canonical identity for `U`; a proof of the all-even-length factorization may need the
-stronger matrix-entry isometry produced inside `rfp_nt_structural_full` to be exported, or an
-alternative local-support description of the product-pair state.
+issue about the NNCPH definition itself. The present `AppendixBStructuralData` record now exposes
+the unit pair-index isometry for `U` in the source convention. A proof of the all-even-length
+factorization still has to turn that matrix-entry isometry into the repeated two-site amplitude on
+the cyclic chain, or give an equivalent local-support description of the product-pair state.
 
 ## Gap 2 — the forward decorrelation theorem is blocked on tensor locality
 

docs/paper-gaps/cpsv16_nncph_ground_state_scope.tex

@@ -111,6 +111,11 @@ \section{Formal boundary}
 not yet prove the named ground-space spanning condition, the three-way
 equivalence with ZCL, the complete canonical-form hypotheses from the source
 statement, or the Beigi ground-space characterization as an internal theorem.
+For the forward RFP-to-NNCPH direction, the three-site \(AX/XB\) support maps
+are now represented in \leanid{MPSTensor.HasOverlappingTwoSiteCommutation};
+the remaining local step is to identify the Appendix~B product-of-entangled-pairs
+projectors with the translated two-site parent terms and prove the overlapping
+commutation relation for them.
 The reverse theorem now consumes both the explicit BNT relation
 \leanid{MPSTensor.IsBNT} and the named all-chain condition
 \leanid{MPSTensor.HasNNCPHGroundSpaces}, but the implication still depends on
@@ -138,9 +143,11 @@ \section{Elimination plan}
 
 The present formal boundary is therefore: the reverse implication has the
 source ground-space hypothesis, but its proof is still the Beigi axiom; the
-forward implication proves only the commutation and zero-energy equations from
-the already axiomatized commutation direction together with frustration-freeness
-of the MPS vector for the canonical parent interaction.
+forward implication has the source-unit Appendix~B structural datum and the
+three-site \(AX/XB\) support maps, but still lacks the even-chain
+product-of-pairs factorization and the local-projector commutation theorem.
+The axiom-backed theorem still supplies the commutation direction used by the
+unconditional statements.
 
 \bibliographystyle{alpha}
 \bibliography{references}

docs/paper-gaps/cpsv16_parent_commuting_hamiltonian_scope.tex

@@ -61,17 +61,25 @@ \section{Current boundary}
 idempotent-product consequence of Definition~D.2 that is sufficient for the
 backward decorrelation implication already proved in the file.
 
+The nearest-neighbor parent-Hamiltonian development now also has a separate
+three-site support layer for the \(AX\) and \(XB\) faces:
+\leanid{MPSTensor.leftPairLift}, \leanid{MPSTensor.rightPairLift}, and
+\leanid{MPSTensor.HasOverlappingTwoSiteCommutation}.  This records the local
+action and commutation equation on the common three-site space, but it still
+does not include the kernel-intersection condition or the orthogonal-projector
+identification required by Definition~D.2.
+
 \section{Elimination plan}
 
-A source-faithful version should introduce the tensor-product setting
-\(\mathcal H_A\otimes\mathcal H_X\otimes\mathcal H_B\), the local subspaces
-\(K_{AX}\) and \(K_{XB}\), and the corresponding orthogonal projectors
-\(Q_{AX}\) and \(Q_{XB}\).  From the source hypotheses it should derive the
+A source-faithful version should build on the existing \(AX/XB\) support layer
+by adding the local subspaces \(K_{AX}\) and \(K_{XB}\), the corresponding
+orthogonal projectors \(Q_{AX}\) and \(Q_{XB}\), and the source
+kernel-intersection equation.  From those hypotheses it should derive the
 idempotent-product declaration above as a lemma, with \(P_K=P_{AXB}\).
 
-After that tensor-product version is available, the blueprint entry for the
-source parent commuting Hamiltonian condition should point to that source-level
-statement.  The current idempotent-product declaration can remain as the
+After that source-level version is available, the blueprint entry for the source
+parent commuting Hamiltonian condition should point to that statement.  The
+current idempotent-product declaration can remain as the
 algebraic lemma used in the backward direction of Proposition~D.3.  The work is
 tracked by \ghissue{2633} and \ghissue{190}.
 

docs/paper-gaps/cpsv16_rfp_isometry_scope.tex

@@ -102,6 +102,9 @@ \section{Formal boundary}
 \end{align}
 Thus the scalar normalization mismatch is no longer hidden in the formal
 statement: both conventions are available, and their comparison is explicit.
+The Appendix~B structural datum used in the parent-Hamiltonian bridge now
+chooses the unit pair-index convention, so the remaining even-chain
+factorization problem starts from the source normalization.
 
 There is still no conclusion relating $U_k$ and $U_\ell$ for $k\ne \ell$.  Thus
 the formal theorems record only a separate isometry condition for each block;