Tracking: PEPS Fundamental Theorem for injective and normal tensors

[LionSR]

Purpose

Track the current cleanup of the PEPS Fundamental Theorem part so that both the Lean proof and the blueprint exposition follow arXiv:1804.04964 faithfully.

The original concerns were:

• the proof is not completed;
• the TikZ diagrams do not match the paper;
• some diagrams are not attached to precise mathematical steps.

Current structure

There are now three connected strands.

• Injective proof strand: Tracking: injective PEPS Fundamental Theorem #128 is the injective PEPS Theorem 2 tracker. The critical edge-local step is PEPS FT: formalize the edge-insertion comparison from arXiv:1804.04964 §3 #1255, whose remaining identity-insertion finite-sum reindexing substep is PEPS FT: prove the finite diagonal reindexing for identity edge insertion #1372. The blocked three-site injectivity bridge is PEPS FT: prove injectivity of the edge-blocked three-site MPS #1366. The edge-blocked insertion algebra isomorphism is PEPS FT: formalize the edge-blocked insertion algebra isomorphism #1367, whose two internal inj_isomorph substeps are PEPS FT: formalize virtual-to-physical realization in the three-site insertion argument #1369 and PEPS FT: formalize physical-to-virtual recovery in the three-site insertion argument #1370. Extraction of the conjugating edge gauge is PEPS FT: extract the edge gauge from the insertion algebra isomorphism #1368. Edge-gauge absorption into the modified tensor family is PEPS FT: formalize edge-gauge absorption into the modified tensor family #1363, and the post-absorption equality eq:inj_equal_edge is PEPS FT: formalize the post-absorption edge insertion equality #1364. The two-injective comparison is split into its scalar-reduction core PEPS FT: formalize scalar reduction in the two-injective-tensor comparison #1362 and the enclosing comparison PEPS FT: formalize the generalized two-injective-tensor comparison #1361; the final one-vertex-versus-complement step is PEPS FT: formalize the final one-vertex versus complement comparison #1360.
• Normal proof strand: Tracking: normal PEPS blocking route #1373 tracks the normal PEPS Section 3 route. Its subissues are PEPS FT: formalize the union of injective regions #1374 for Lemma injective_union, PEPS FT: formalize the normal PEPS edge-blocking hypotheses #1375 for the normal edge-blocking hypotheses and normal theorem statements, and Blueprint PEPS diagrams: attach the normal-section diagrams from the paper #1376 for the normal-section diagram attachments.
• Diagram strand: Tracking: semantic tensor-network diagrams for the blueprint #1019 is the tensor-network diagram tracker. The PEPS-specific audit and repair are separated into Blueprint PEPS diagrams: audit Chapter 13a against arXiv:1804.04964 #1256 and Blueprint PEPS diagrams: semantic TikZ primitives for edge blocking and insertions #1257.

Subissues and relevant open issues

• PEPS FT: formalize the edge-insertion comparison from arXiv:1804.04964 §3 #1255 — formalize the edge-insertion comparison from arXiv:1804.04964, Section 3.
• PEPS FT: prove the finite diagonal reindexing for identity edge insertion #1372 — prove the finite diagonal reindexing for the identity edge insertion.
• PEPS FT: prove injectivity of the edge-blocked three-site MPS #1366 — prove injectivity of the edge-blocked three-site MPS.
• PEPS FT: formalize the edge-blocked insertion algebra isomorphism #1367 — formalize the edge-blocked insertion algebra isomorphism from the three-site injective theorem.
• PEPS FT: formalize virtual-to-physical realization in the three-site insertion argument #1369 — formalize the virtual-to-physical realization X -> O_1,O_2 inside inj_isomorph.
• PEPS FT: formalize physical-to-virtual recovery in the three-site insertion argument #1370 — formalize the physical-to-virtual recovery O_1,O_2 -> W inside inj_isomorph.
• PEPS FT: extract the edge gauge from the insertion algebra isomorphism #1368 — extract the edge gauge and bond-dimension equality from the insertion algebra isomorphism.
• PEPS FT: formalize edge-gauge absorption into the modified tensor family #1363 — formalize absorption of edge gauges into the modified tensor family (\widetilde B).
• PEPS FT: formalize the post-absorption edge insertion equality #1364 — formalize the post-absorption edge insertion equality eq:inj_equal_edge.
• PEPS FT: formalize scalar reduction in the two-injective-tensor comparison #1362 — formalize the scalar-reduction substep inside Lemma inj_equal_tensors_2.
• PEPS FT: formalize the generalized two-injective-tensor comparison #1361 — formalize the generalized two-injective-tensor comparison, Lemma inj_equal_tensors_2.
• PEPS FT: formalize the final one-vertex versus complement comparison #1360 — formalize the final one-vertex versus complement comparison after edge-gauge absorption.
• Tracking: normal PEPS blocking route #1373 — track the normal PEPS blocking route of Section 3.
• PEPS FT: formalize the union of injective regions #1374 — formalize the union of injective regions.
• PEPS FT: formalize the normal PEPS edge-blocking hypotheses #1375 — formalize the normal PEPS edge-blocking hypotheses.
• Blueprint PEPS diagrams: attach the normal-section diagrams from the paper #1376 — attach the normal-section diagrams from the paper.
• PEPS: build virtual-insertion and blocking infrastructure for the remaining Fundamental Theorem theorems #763 — build the remaining virtual-insertion and blocking infrastructure.
• PEPS: HasLocalGaugeLift from SameState via blocked-middle three-site MPS reduction #820 — derive the local gauge lift from equality of states through the blocked-middle three-site MPS reduction.
• PEPS: bond-dimension equality from SameState and vertex injectivity #874 — prove bond-dimension equality from equality of states and vertex injectivity.
• PEPS: local gauge existence, consistency, and main theorem assembly #780 — assemble local gauge existence, consistency, and the main PEPS theorem.
• Discharge sorry in gauge_unique_mod_edge_scalars (PEPS uniqueness modulo balanced edge scalars) #842 — prove uniqueness modulo balanced edge scalars.
• Blueprint PEPS diagrams: audit Chapter 13a against arXiv:1804.04964 #1256 — audit Chapter 13a PEPS diagrams against the diagrams and proof steps of the paper.
• Blueprint PEPS diagrams: semantic TikZ primitives for edge blocking and insertions #1257 — add semantic TikZ primitives for PEPS edge blocking and matrix insertions.
• Blueprint tensor-network diagrams need a mathematical visual grammar #1009 — maintain a mathematical visual grammar for tensor-network diagrams.
• Tracking: semantic tensor-network diagrams for the blueprint #1019 — keep the blueprint diagram programme coherent across PDF and web output.

Previous issues folded in

• Discharge 6 sorrys in PEPS/FundamentalTheorem.lean #503 was the original six-sorry tracker. It is now superseded by the finer PEPS issues under Tracking: injective PEPS Fundamental Theorem #128 and Tracking: normal PEPS blocking route #1373.
• Add TikZ diagrams to PEPS blueprint section #504 added the first PEPS TikZ diagrams. The present problem is that those diagrams now require a mathematical audit against the paper, tracked by Blueprint PEPS diagrams: audit Chapter 13a against arXiv:1804.04964 #1256 and Blueprint PEPS diagrams: semantic TikZ primitives for edge blocking and insertions #1257. The injective diagrams are tracked through PEPS FT: prove injectivity of the edge-blocked three-site MPS #1366, PEPS FT: formalize the edge-blocked insertion algebra isomorphism #1367, PEPS FT: formalize virtual-to-physical realization in the three-site insertion argument #1369, PEPS FT: formalize physical-to-virtual recovery in the three-site insertion argument #1370, PEPS FT: extract the edge gauge from the insertion algebra isomorphism #1368, PEPS FT: formalize edge-gauge absorption into the modified tensor family #1363, PEPS FT: formalize the post-absorption edge insertion equality #1364, PEPS FT: formalize scalar reduction in the two-injective-tensor comparison #1362, PEPS FT: formalize the generalized two-injective-tensor comparison #1361, and PEPS FT: formalize the final one-vertex versus complement comparison #1360. The normal-section diagrams are tracked through Blueprint PEPS diagrams: attach the normal-section diagrams from the paper #1376.
• PEPS/Defs: strengthen IsVertexInjective to LinearIndependent #594 and PEPS: replace function-level vertex injectivity with linear independence #633 repaired the paper mismatch in vertex injectivity by replacing function-level injectivity with linear independence.
• PEPS/FundamentalTheorem: repair gauge_unique_up_to_scalar after the triangle counterexample #762 repaired the false global-scalar uniqueness statement; the remaining proof of the corrected statement is Discharge sorry in gauge_unique_mod_edge_scalars (PEPS uniqueness modulo balanced edge scalars) #842.

Standard for the next work

The injective proof should follow the paper's Section 3 route:

1. block a neighbourhood of a chosen edge into a three-site injective MPS;
2. prove that vertex injectivity passes to the edge-blocked three-site MPS;
3. define the edge-insertion coefficient and prove its identity specialization, with the finite diagonal reindexing tracked by PEPS FT: prove the finite diagonal reindexing for identity edge insertion #1372;
4. realize arbitrary virtual insertions by physical operations on either neighboring endpoint, and recover a virtual insertion from two equal neighboring physical actions;
5. compare arbitrary matrix insertions on the chosen virtual bond and obtain the edge-blocked insertion algebra isomorphism;
6. obtain the bond-dimension equality and the edge gauge from the algebra isomorphism;
7. absorb the edge gauges into the second tensor family, producing (\widetilde B), and prove the post-absorption insertion equality eq:inj_equal_edge;
8. prove the scalar-reduction substep and the generalized two-injective-tensor comparison, then apply that comparison by blocking one vertex against its complement, obtaining local proportionality of the tensors;
9. absorb the remaining scalar freedom into the local gauges, with uniqueness understood modulo balanced edge scalars.

The normal proof should add the paper's extra blocking layer: prove the union of injective regions, build the square-lattice regions R, S, and T, block around each edge into three injective regions, then reuse the same injective-chain insertion route. The diagrams should depict these same mathematical objects and should be attached to the named theorem or definition that uses them.

[LionSR]

somebody take it up

[LionSR]

Please use the native subissues for tracking

[LionSR]

Current PEPS Section 3 status update:

• Proof route: PEPS FT: formalize the edge-insertion comparison from arXiv:1804.04964 §3 #1255 now has the first formal edge-insertion layer in TNLean/PEPS/Blocking.lean and a companion note, docs/paper-gaps/peps_injective_ft_section3_route.tex, mapping arXiv:1804.04964, Section 3 to the remaining formal obligations.
• Diagrams: Blueprint PEPS diagrams: audit Chapter 13a against arXiv:1804.04964 #1256 and Blueprint PEPS diagrams: semantic TikZ primitives for edge blocking and insertions #1257 now track the corrected Section 3 diagrams. The current worktree adds semantic macros for edge blocking, three-site insertion comparison, and physical realization of a virtual insertion, and attaches them in Chapter 13a.
• Local checks completed: paper-gap note compiles cleanly with BibTeX; diagram macro registry and Python compilation pass; standalone LaTeX/TikZ rendering of the three new macros succeeds.
• Local blockers remain: Lean checking is blocked by stale or missing .olean files until the cache is refreshed; leanblueprint checkdecls is blocked by missing blueprint/lean_decls.