# TNLean import structure

`TNLean.lean` is the stable import surface for the maintained library. It and
the directory aggregators are generated by
`scripts/generate_import_aggregators.py`; do not edit them by hand. The
completeness check requires every production module to occur in the generated
hierarchical frontier, rather than accepting an incidental import from another
handwritten module.

The generator creates one pure-import aggregator for each production directory
that does not already have a handwritten module of the same name. When a file
and directory share a module name, the handwritten file remains authoritative
and the nearest generated ancestor imports that file together with the
uncovered descendant frontier. This preserves existing public module names
without hiding descendants. A file is treated as generated only when it has
the stable marker, contains imports and comments only, and carries an embedded
module name matching its non-Archive path. This provenance lets the generator
remove stale aggregators after their source directory disappears, while copying
the marker into handwritten code does not make that file disposable.

## Conceptual layers

The generated files sort imports by module name; they do not encode dependency
order as comments. The library nevertheless follows the conceptual layers that
were formerly documented inline in `TNLean.lean`:

| Layer | Main areas | Responsibility |
| --- | --- | --- |
| 0 | `Algebra` | General matrix, representation, block, and finite-dimensional algebra. |
| 0b | `Analysis` | Ergodic, projection, functional-calculus, matrix-order, norm, and trace analysis. |
| 1 | `Topology` | Convex projection, Brouwer, compactness, and fixed-point infrastructure. |
| 2 | `Channel`, `Entropy` | Quantum channels; Choi, Kraus, and Stinespring theory; entropy and recovery. |
| 2a | `Axioms` | Explicit axiomatized inputs such as Brouwer, entropy inequalities, and operator convexity. |
| 2b | `Channel.Schwarz` and related analysis | Schwarz inequalities, operator convexity and monotonicity, and relative-entropy results. |
| 2c | `Channel.FixedPoint`, `Channel.Irreducible`, `Channel.Peripheral`, `Channel.Semigroup`, `Channel.KoashiImoto`, `QPF`, `Spectral` | Fixed points, quantum Perron--Frobenius theory, peripheral spectrum, spectral gaps, semigroups, and the common invariant algebra of jointly invariant states. |
| 3 | `MPS.Chain`, `MPS.Core`, `MPS.Overlap` | Matrix-product tensor definitions, words, blocking, transfer matrices, and overlaps. |
| 3b | `MPS.MPDO` | MPO, MPDO, and LPDO foundations. |
| 4 | `MPS.FundamentalTheorem`, `MPS.Symmetry` | The single-block fundamental theorem and symmetry consequences. |
| 5 | `MPS.BNT`, `MPS.CanonicalForm`, `MPS.Irreducible`, `MPS.Periodic`, `MPS.Structure` | Multi-block canonical forms, periodicity, and structural assembly. |
| 5b | `MPS.RFP` | Renormalization fixed-point theory. |
| 6 | `Wielandt` | Span growth, rank-one extraction, primitivity, and quantum Wielandt inequalities. |

`PiAlgebra` provides related algebraic formulations. `PEPS` contains the
two-dimensional injective and normal-tensor developments. Public chapter-index
and semigroup modules are part of the production tree and therefore enter the
generated import surface automatically.

## Archive exclusion

`TNLean/Archive/` is intentionally outside the production manifest and is not
imported by `TNLean.lean`. It contains retired, documentary, or alternate
routes retained for reference rather than active downstream use. In particular,
the old root documentation singled out the alternate CFII periodicity proof
`TNLean.Archive.BlockingPeriodicityCFII2` and the documentary separation
counterexample `TNLean.Archive.BlockSepCounterexample`; the archive now also
contains the documented Perron--Frobenius counterexamples. See
`TNLean/Archive/README.md` for the current archive policy and replacement paths.

## Size policy

The ordinary 1000-line limit still applies to hierarchical aggregators. The CI
size checker registers only the exact root path `TNLean.lean` as an import-only
exemption, and validates that it contains no declarations. No hierarchical
aggregator currently approaches the limit, so broadening that exemption is not
necessary. The import-completeness workflow independently verifies every
generated file byte-for-byte.