This directory contains the mathematical blueprint for TNLean. The blueprint is the reader-facing account of the formalization: it states the definitions, lemmas, and theorems in mathematical language and links them to the corresponding Lean declarations with \lean{...} and \leanok tags.

• src/ contains the LaTeX source.
• src/chapter/ contains one file per chapter.
• src/content.tex is the chapter router for the full Tensor Network Theory blueprint.
• src/content_ft_mps.tex contains the separate Fundamental Theorem of Matrix Product States volume, comprising the tensor-network chapters through Symmetries and String Order.
• src/print_ft_mps.tex is the PDF entry point for that FT--MPS volume.
• src/macros/ contains blueprint-specific macros and diagram commands.
• src/references.bib is the blueprint bibliography.
• print/ and web/ are generated outputs.

Run these commands from the repository root:

lake build
python3 scripts/fetch_tenkz.py
cd blueprint
leanblueprint checkdecls
leanblueprint pdf
leanblueprint web

leanblueprint checkdecls should be run after adding or changing \lean{...} tags. The PDF and web builds regenerate blueprint/print/ and blueprint/web/.

Build the separate FT--MPS volume from the repository root:

./scripts/build_blueprint_ch01_12.sh

This writes blueprint/print/print12.pdf, containing the focused FT--MPS volume. The full build remains at blueprint/print/print.pdf.

Blueprint prose should be mathematical prose. Avoid Lean-specific explanations in visible text; the \lean{...} tag supplies the link to the formal declaration. Maintainer notes about proof status, local formalization choices, or paper-gap documents should be written as LaTeX comments unless they are part of the mathematical statement being presented to readers.

When a result is claimed to formalize a source theorem, the blueprint statement must match the source hypotheses. If the current Lean theorem has extra hypotheses, the source theorem should not be marked as fully formalized until a source-faithful statement exists.

The detailed style rules are in:

• docs/blueprint_style_guide.md
• the lean-conventions skill (prose_style, MATHLIB_doc references)