RFP/MPDO 2/5 Commuting parent Hamiltonians and decorrelation theorem

[LionSR]

What

Define commuting and nearest-neighbor commuting parent Hamiltonians (NNCPH). Prove the dimension-independent decorrelation ⟺ commuting Hamiltonian equivalence from Appendix D. Connect to the RFP theory (Thm 3.10(iii) ⟺ (i), gated on [Beigi]).

Files

• TNLean/MPS/ParentHamiltonian/Commuting.lean — IsCommutingParentHam, IsNNCPH, RFP connection
• TNLean/MPS/ParentHamiltonian/Decorrelation.lean — IsDecorrelated, decorrelation ⟺ commuting Ham
• Blueprint: extend ch14 (§14.6 commuting PH, §14.7 decorrelation)

Key definitions

/-- Commuting parent Hamiltonian: local terms mutually commute. -/
def IsCommutingParentHam (A : MPSTensor d D) (L N : ℕ) : Prop :=
  ∀ i j : Fin N, localTerm A L N i * localTerm A L N j = localTerm A L N j * localTerm A L N i

/-- Nearest-neighbor commuting parent Hamiltonian (L = 2). -/
def IsNNCPH (A : MPSTensor d D) (N : ℕ) : Prop :=
  IsCommutingParentHam A 2 N

/-- Regions A and B are decorrelated w.r.t. subspace K if
    P_K O_A P_K^⊥ O_B P_K = 0 for all observables O_A, O_B. -/
def IsDecorrelated (P_K : ...) (H_A H_B : ...) : Prop := ...

Key statements

1. Def 3.9 IsCommutingParentHam, IsNNCPH
2. Thm 3.10(iii)⟹(i) nncph_implies_rfp: NNCPH ⟹ RFP — gated on [Beigi]
3. Thm 3.10(i)⟹(iii) rfp_implies_nncph: RFP ⟹ NNCPH — follows from Thm 3.11 structural form
4. Prop D.1 decorrelated_iff_commutingHam: K_{AXB} has commuting parent Ham ⟺ A, B decorrelated

Approach

Commuting.lean: IsCommutingParentHam is a predicate on the PH definitions from #191 (PR#201). The direction RFP ⟹ NNCPH is straightforward from the structural form (Thm 3.11, issue 1/5): RFP tensors generate product-of-entangled-pair states, whose parent Hamiltonians obviously commute. The reverse direction (NNCPH ⟹ RFP) uses [Beigi]'s result that ground spaces of commuting NN Hamiltonians in 1D with finite degeneracy are spanned by states of the form U^⊗N |φ⟩^⊗N that are locally orthogonal — hence RFP by Thm 3.11.

Decorrelation.lean: Self-contained, dimension-independent. The proof uses:

• Support projectors P_{AX}, P_{XB} of partial traces of K_{AXB}
• The decorrelation condition forces P_{AX} P_{XB} = P_{XB} P_{AX} = P_{AXB}
• Commutativity of projectors ⟹ commuting Hamiltonian (set Q = 1 - P)
• Converse: commuting projectors ⟹ P_{AX} P_{XB} = P_{AXB} ⟹ decorrelation

Reading

• [CPGSV17] Papers/1606.00608/MPDO-22-12-17-2.tex §3.3 (lines 507–528), Appendix B last paragraph (lines 1305–1307), Appendix D.2 (lines 2181–2290)
• [Beigi] Beigi, Shor, Whalen, Commun. Math. Phys. 2012 — ground space characterization for commuting Hamiltonians

Dependencies

• Issue 1/5 (RFP/MPDO 1/5 Pure-state RFP: definitions, ZCL ⟺ E²=E, structural form #233): MPS/RFP/Assembly.lean (RFP ⟺ ZCL), MPS/RFP/StructuralForm.lean
• Parent Hamiltonian 1/5 Ground space, definitions, and basic properties #191 / PR#201: MPS/ParentHamiltonian/Defs.lean (parentHamiltonian, localTerm, IsFrustrationFree)
• External: [Beigi] result (not in Mathlib or codebase — needed for NNCPH ⟹ RFP)

Estimated ~470 LOC. Decorrelation theorem (~350) is independent of everything else.

Part of #232.

[LionSR]

Auto fix: Define commuting parent Hamiltonians and prove decorrelation theorem

Read Papers/1606.00608/MPDO-22-12-17-2.tex — specifically §3.3 (Def 3.9, Thm 3.10), Appendix D.2 (Prop D.1).

The decorrelation theorem (Prop D.1) is independent of the RFP chain and can be done now:

Create TNLean/MPS/ParentHamiltonian/Decorrelation.lean:

1. Define IsDecorrelated — regions A, B decorrelated w.r.t. subspace K
2. Prove decorrelated_iff_commutingHam — decorrelation ⟺ commuting Hamiltonian

Also create TNLean/MPS/ParentHamiltonian/Commuting.lean:

1. Define IsCommutingParentHam — local terms mutually commute
2. Define IsNNCPH — nearest-neighbor commuting (L=2)
3. State rfp_implies_nncph (RFP ⟹ NNCPH) — can be sorry pending RFP/MPDO 1/5 Pure-state RFP: definitions, ZCL ⟺ E²=E, structural form #233

Read existing TNLean/MPS/ParentHamiltonian/Defs.lean for parentHamiltonian, localTerm, IsFrustrationFree.

Commit: feat(ParentHamiltonian): define commuting PH and prove decorrelation theorem

@claude

---

Generated by Claude Code

[claude]

Claude finished @LionSR's task in 9m 27s —— View job • claude/issue-234-rfpmpdo-25-commuting-parent-hamiltonians • Create PR ➔

---

Implementing commuting parent Hamiltonians and decorrelation theorem

• Read CLAUDE.md and gather repo context
• Read existing ParentHamiltonian/Defs.lean for definitions
• Read paper §3.3 and Appendix D.2 for mathematical content
• Create Commuting.lean — IsCommutingParentHam, IsNNCPH, RFP connection
• Create Decorrelation.lean — IsDecorrelated, decorrelation ⟺ commuting Ham
• Update module imports in TNLean.lean
• Build and verify with lake build
• Commit and push

Summary

Created two new files (328 LOC total):

TNLean/MPS/ParentHamiltonian/Commuting.lean (~110 LOC):

• IsCommutingParentHam A L N — local terms of parent Hamiltonian mutually commute (Def 3.9)
• IsNNCPH A N — nearest-neighbor commuting parent Hamiltonian (L = 2)
• IsCommutingParentHam.symm, .ham_comm_localTerm — basic API
• rfp_implies_nncph / nncph_implies_rfp / rfp_iff_nncph — Thm 3.10 equivalence (sorry, pending RFP/MPDO 1/5 Pure-state RFP: definitions, ZCL ⟺ E²=E, structural form #233 structural form and [Beigi])

TNLean/MPS/ParentHamiltonian/Decorrelation.lean (~210 LOC):

• IsDecorrelated P_K ObsA ObsB — regions A, B decorrelated w.r.t. subspace K
• HasCommutingParentHam P_K — subspace corresponds to commuting parent Hamiltonian
• decorrelated_iff_commutingHam — Prop D.1 (sorry, pending tensor-product Hilbert space infrastructure)
• Fully proved auxiliary lemmas: comp_idempotent_of_comm_of_idempotent, left_absorb_of_comm_idempotent, right_absorb_of_comm_idempotent, comp_complement_comm_zero

All sorrys are documented and gated on specific dependencies (#233, [Beigi], tensor product infrastructure).

[claude]

🤖 PR #372 has been opened to address this issue.

Branch: claude/issue-234-rfpmpdo-25-commuting-parent-hamiltonians
Title: feat(MPS/ParentHamiltonian): add commuting parent Hamiltonians and decorrelation theorem

Defines IsCommutingParentHam, IsNNCPH, and IsDecorrelated with the decorrelation ⟺ commuting Hamiltonian equivalence (Prop D.1); RFP connection statements are gated on #233 and [Beigi].

[claude]

📦 PR #372 (feat(MPS/ParentHamiltonian): add commuting parent Hamiltonians and decorrelation theorem) has been merged. Accomplished:

• Def 3.9: IsCommutingParentHam, IsNNCPH with basic API (symm, ham_comm_localTerm)
• Thm 3.10 (i)⟹(iii): isNNCPH_of_isRFP — compiles without sorry but is vacuously true (placeholder localTerm = 0)
• Def D.1/D.2: IsDecorrelated, HasCommutingParentHam (abstract, non-tensor-product setting)
• Prop D.3 backward: commutingHam_isDecorrelated — fully proved via comp_complement_comm_zero
• Blueprint: Updated ch14_parent_hamiltonian.tex with all 6 new declarations

Remaining:

1. Rewrite isNNCPH_of_isRFP and ham_comm_localTerm once localTerm gets its real definition (gated on parentInteraction fix, depends on RFP/MPDO 1/5 Pure-state RFP: definitions, ZCL ⟺ E²=E, structural form #233)
2. Add nncph_implies_rfp with 2 ≤ N hypothesis (gated on Beigi's result)
3. Add tensor-product locality constraints to HasCommutingParentHam (needs tensor-product Hilbert space infrastructure)
4. Prove forward direction of Prop D.3 (decorrelated → commuting parent Hamiltonian, tensor-product setting)

Suggested next step: Items 1–2 are gated on #233 (structural form of RFP tensors) — once IsCID and Thm 3.11 are complete there, the vacuous proofs here can be replaced. Item 3 (tensor-product locality) is independent and could be started as soon as Mathlib's tensor-product Hilbert space API is available.