TNLean

TNLean is a Lean 4 library for finite-dimensional tensor-network mathematics. Its central thread is the Fundamental Theorem of Matrix Product States (MPS), with formal developments of finite-dimensional quantum channels, Perron--Frobenius and quantum Wielandt theory, parent Hamiltonians, matrix-product density operators (MPDOs), renormalization fixed points (RFPs), and the present PEPS frontier. The project is built on Mathlib and currently uses Lean 4 / Mathlib v4.31.0.

This is a research formalization. The maintained root import is

import TNLean

and it imports the public modules intended for downstream users. Some frontier files still contain explicit sorrys or sanctioned axioms; the badges above and the LeanBlueprint give the current accounting. The README below is therefore conservative: it separates proved infrastructure and theorem packages from the canonical-form, parent-Hamiltonian, MPDO/RFP, and PEPS arguments that remain active formalization fronts.

Mathematical scope

Matrix product states and the Fundamental Theorem

The MPS core introduces tensors MPSTensor d D, word evaluation, matrix product vector (MPV) coefficients, injectivity, blocking, transfer maps, overlap matrices, block-diagonal tensors, and gauge equivalence. The basic single-block theorem is proved by extending the map $A^i \mapsto B^i$ linearly, proving multiplicativity from MPV equality, and applying Skolem--Noether for full matrix algebras:

theorem MPSTensor.fundamentalTheorem_singleBlock {A B : MPSTensor d D}
    (hA : IsInjective A) (hAB : SameMPV A B) : GaugeEquiv A B

The library also contains chain-level variants, translation-invariance corollaries, finite-length SameMPV interfaces, and bridges between equality of periodic states and equality of MPV families under explicit hypotheses.

The multi-block and canonical-form development is substantially larger. It formalizes BNT-style block data, block permutations, normal and canonical-form predicates, overlap decay hypotheses, coefficient-convergence statements, and same-structure assembly theorems. Current top-level theorems include the canonical-form equal-MPV and proportional-MPV results under explicit structural and coefficient hypotheses, together with reduction theorems that decompose a general tensor, normalize nonzero irreducible blocks by a trace-preserving gauge, and remove periods by blocking or cyclic-sector decomposition. What is not yet advertised as a completed theorem is the fully automatic passage from arbitrary raw tensors to the final paper-level canonical form with all common-length, length-zero dimension, and sector-comparison hypotheses derived internally.

Quantum channels and Perron--Frobenius theory

The channel side works with finite-dimensional matrix algebras. It includes positive and completely positive maps, density-matrix retracts, partial traces, Choi--Jamiolkowski matrices, Kraus representations, Stinespring dilations, CP order and Radon--Nikodym infrastructure, POVMs, Schwarz inequalities and multiplicative domains, fixed-point algebras, irreducibility, stationary supports, peripheral spectra, and finite-dimensional quantum Markov semigroups in the style of Wolf's Quantum Channels & Operations.

One recurrent tool is the Perron--Frobenius existence theorem for positive maps, proved through a Brouwer fixed-point theorem on density matrices:

theorem exists_posSemidef_eigenvector [NeZero D]
    (E : Matrix (Fin D) (Fin D) ℂ →ₗ[ℂ] Matrix (Fin D) (Fin D) ℂ)
    (hpos : IsPositiveMap E)
    (hNZ : ∀ {ρ : Matrix (Fin D) (Fin D) ℂ}, ρ.PosSemidef → ρ ≠ 0 → E ρ ≠ 0) :
    ∃ (ρ : Matrix (Fin D) (Fin D) ℂ) (r : ℝ),
      ρ.PosSemidef ∧ ρ ≠ 0 ∧ 0 < r ∧ E ρ = (r : ℂ) • ρ

The formalized Wolf material is selective rather than a chapter-by-chapter completion. Chapters on Schwarz inequalities, spectral theory, fixed points, and semigroups are the most developed. Strong subadditivity and some operator-convexity facts are recorded as explicit axiomatized interfaces. Mutual-information monotonicity $I(A{:}B) \le I(A{:}BC)$ (Entropy.mutualInformation_monotone_tripartite, arXiv:1606.00608 Prop C.1) and the area-law bound $I(A{:}B) \le \log d_A + \log d_B$ (Entropy.mutualInformation_le_log_dim_add_log_dim, arXiv:1606.00608 line 1319) are proved as theorems from strong subadditivity, while further operator-convexity facts await upstream Mathlib coverage.

Quantum Wielandt theory

The Wielandt hierarchy supplies span-growth infrastructure, rank-one extraction, rectangular span arguments, primitive-map definitions, and paper-facing endpoint modules. A central current theorem is the cumulative $D^2$ bound for the project's normality predicate:

theorem cumulativeSpan_eq_top_of_isNormal_bound [NeZero D]
    (A : MPSTensor d D) (hN : IsNormal A) :
    cumulativeSpan A (D ^ 2) = ⊤

The active frontier here is to align sharpened quantum Wielandt bounds with the subspace elements and constants used in the source literature. The repository keeps mathematical notes under docs/paper-gaps/ when a paper argument and the formal statement are not identical.

Parent Hamiltonians, MPDO/RFP, PEPS, and examples

The parent-Hamiltonian modules define local terms and finite-chain ground spaces, prove basic frustration-free and annihilation statements, develop intersection and wrapping-window infrastructure, and contain unique-ground-state theorems for injective or normal MPS under the hypotheses stated in the Lean declarations. The martingale and overlapping-window estimates needed for spectral-gap proofs remain an active frontier.

The MPDO and RFP modules contain foundations for matrix-product density operators, locally purified density operators, vertical and bi-canonical form, zero-correlation-length and RFP predicates, pure-recovery and structural-form interfaces, fusion-isometry and commuting-form constructions, and related bridges. These files should be read as a growing formal infrastructure for the MPDO/RFP parts of the tensor-network story, not as a completed classification proof.

The PEPS directory gives finite-graph tensor definitions including square-lattice graph structure, state coefficients, virtual insertion, identity-edge insertion, normal-edge blocking and complement-cover infrastructure, edge gauge extraction, local gauge operations, and the current scaffold for the injective PEPS Fundamental Theorem. The PEPS theorem statements are intentionally present near the definitions they require, but the complete proof of the two-dimensional theorem is still future work.

The repository also contains small MPS examples such as AKLT, GHZ, even parity, and $\mathbb{Z}/2\mathbb{Z}$ examples, together with the TNLean/PiAlgebra/ directory of algebraic Fundamental-Theorem variants.

Module structure

TNLean.lean is the public import surface. It imports maintained modules and intentionally leaves archival material in TNLean/Archive/ outside the root import. The main source tree is organized as follows.

Path	Role
TNLean/Algebra, TNLean/Analysis, TNLean/Topology	Matrix algebra, trace pairings, Gram matrices, Frobenius norms, Skolem--Noether, convergence helpers, and finite-dimensional fixed-point infrastructure.
TNLean/Axioms, TNLean/Entropy	Explicit interfaces for Brouwer, strong subadditivity, Beigi recovery, operator convexity, and entropy corollaries.
TNLean/Channel	Quantum-channel representations, Schwarz theory, fixed points, irreducibility, peripheral spectra, semigroups, determinants, POVMs, and Wolf chapter index modules.
TNLean/QPF, TNLean/Spectral	Perron--Frobenius, positivity, mixed transfers, overlap decay, spectral gaps, and quantitative correlation estimates.
TNLean/MPS/Core, TNLean/MPS/Chain, TNLean/MPS/Overlap	MPS tensors, words, blocking, chains, transfer maps, and overlap matrices.
TNLean/MPS/Tactic	Custom simp attribute sets (mps_block_words, mps_transfer) and tactic macros (mpv_ext, block_words, transfer_simp) for recurring MPS proof patterns.
TNLean/MPS/FundamentalTheorem, TNLean/MPS/BNT, TNLean/MPS/CanonicalForm, TNLean/MPS/Periodic, TNLean/MPS/Structure	Single-block, same-structure, BNT, periodic, and canonical-form Fundamental-Theorem material.
TNLean/MPS/Symmetry	Gauge uniqueness, on-site symmetries, virtual representations, cocycle coboundaries, symmetric MPS, and string-order infrastructure.
TNLean/MPS/Irreducible	Fixed-point projections, Form II reductions, scalar fixed points, adjoint irreducibility, and periodic-blocking infrastructure for irreducible blocks.
TNLean/MPS/SharedInfra	Cross-cutting helpers reused across the canonical-form, irreducible, and Wielandt developments: block assembly and gauge data, gauge-phase normalization, Kraus-adjoint setup, scaling, and sector decomposition.
TNLean/MPS/ParentHamiltonian	Parent Hamiltonians, local projectors, ground spaces, intersection and wrapping-window arguments, commuting cases, and martingale estimates.
TNLean/MPS/MPDO, TNLean/MPS/RFP	MPDO/LPDO foundations, canonical-form and zero-correlation-length predicates, pure RFP structures, and structural bridges.
TNLean/MPS/Examples	Example tensors and state families, including AKLT, even-parity, GHZ, and $\mathbb{Z}/2$ examples.
TNLean/Wielandt	Quantum Wielandt span growth, rank-one constructions, rectangular span, primitivity equivalences, and paper-facing endpoints.
TNLean/PEPS	PEPS definitions, square-lattice graph structure, virtual insertions, identity-edge insertions, normal-edge blocking and complement-cover infrastructure, edge gauge extraction, local gauge transformations, and the injective PEPS theorem frontier.
TNLean/PiAlgebra	Algebraic Fundamental-Theorem variants and product-algebra/canonical-form auxiliary predicates.
blueprint/, docs/	The LeanBlueprint, style and contribution guides, CI documentation, and paper-gap notes.

For exact imports, read TNLean.lean; it is the most reliable snapshot of the maintained library surface.

Current frontiers

The issue tracker contains fine-grained formalization tasks. The main fronts at the present release state are:

• completing the arbitrary-tensor-to-final-canonical-form path, especially common blocking lengths, cyclic-sector comparison, length-zero dimension bookkeeping, and the finite-length span equalities used by the block permutation theorem;
• strengthening the parent-Hamiltonian story from intersection and uniqueness results toward martingale and overlapping-window spectral-gap estimates;
• extending the quantum Wielandt endpoint to the sharpened bounds and subspace elements used in the current paper notes;
• turning the MPDO/RFP structural interfaces into complete classification arguments; and
• replacing the PEPS Fundamental-Theorem scaffold by a full proof of local gauge existence, consistency, and uniqueness.

Known mathematical deviations, missing hypotheses, or places where the formal route differs from a cited source are recorded in docs/paper-gaps/ as stand-alone mathematical notes.

Building

The Lean version is pinned by lean-toolchain; Mathlib is pinned in lakefile.toml and lake-manifest.json.

# Optional but recommended: download pre-built Mathlib artifacts.
lake exe cache get

# Build the default target, which is TNLean.
lake build

# Equivalently, build the public Lean library target.
lake build TNLean

# Check a single file during development.
lake env lean TNLean/MPS/FundamentalTheorem/Basic.lean

Repository-specific notes from past Lean/Mathlib upgrades are collected in docs/upgrade_4_29.md.

Blueprint and documentation

The LeanBlueprint in blueprint/ is the mathematical companion to the Lean library. Its chapters cover the MPS core, the single-block theorem, quantum channels, Perron--Frobenius theory, Schwarz inequalities, spectral theory, quantum Wielandt, canonical form, BNT and block-permutation arguments, periodic Fundamental-Theorem material, semigroups, PEPS, symmetry, parent Hamiltonians, correlations, and examples.

Typical blueprint commands are:

lake build TNLean
cd blueprint
leanblueprint checkdecls
leanblueprint web   # or: leanblueprint pdf / leanblueprint all

The command leanblueprint checkdecls assumes that the Lean declarations named in the blueprint are available from a successful Lean build. General repository guidance for contributors is in AGENTS.md and CLAUDE.md; style and review conventions are in docs/.

References

The formalization draws principally on the following sources.

• D. Pérez-García, F. Verstraete, M. M. Wolf, J. I. Cirac, Matrix Product State Representations, arXiv:quant-ph/0608197, Quantum Inf. Comput. 7 (2007).
• M. Sanz, D. Pérez-García, M. M. Wolf, J. I. Cirac, A quantum version of Wielandt's inequality, arXiv:0909.5347, IEEE Trans. Inf. Theory 56(9), 4668--4673 (2010).
• J. I. Cirac, D. Pérez-García, N. Schuch, F. Verstraete, Matrix Product Density Operators: Renormalization Fixed Points and Boundary Theories, arXiv:1606.00608, Ann. Phys. 378, 100--149 (2017).
• G. De las Cuevas, J. I. Cirac, N. Schuch, D. Pérez-García, Irreducible forms of Matrix Product States: Theory and Applications, arXiv:1708.00029, J. Math. Phys. 58, 121901 (2017).
• J. I. Cirac, D. Pérez-García, N. Schuch, F. Verstraete, Matrix Product States and Projected Entangled Pair States, arXiv:2011.12127, Rev. Mod. Phys. 93, 045003 (2021).
• A. Molnár, J. Garre-Rubio, D. Pérez-García, N. Schuch, J. I. Cirac, Normal projected entangled pair states generating the same state, arXiv:1804.04964, New J. Phys. 20, 113017 (2018).
• D. Pérez-García, M. M. Wolf, M. Sanz, F. Verstraete, J. I. Cirac, String Order and Symmetries in Quantum Spin Lattices, arXiv:0802.0447, Phys. Rev. Lett. 100, 167202 (2008).
• C. Fernández-González, N. Schuch, M. M. Wolf, J. I. Cirac, D. Pérez-García, Frustration free gapless Hamiltonians for Matrix Product States, arXiv:1210.6613, Commun. Math. Phys. 333, 299--333 (2015).
• N. Schuch, I. Cirac, D. Pérez-García, PEPS as ground states: Degeneracy and topology, arXiv:1001.3807, Ann. Phys. 325, 2153--2192 (2010).
• J. I. Cirac, J. Garre-Rubio, D. Pérez-García, Mathematical open problems in projected entangled pair states, arXiv:1903.09439, Rev. Mat. Complut. 32, 579--599 (2019).
• M. M. Wolf, Quantum Channels & Operations: Guided Tour (2012).
• Mathlib4, the Lean 4 mathematics library.