feat: complete attribute-first Blueprint rendering

README.md

@@ -143,7 +143,8 @@ theorem nat_add_zero_right (n : Nat) : n + 0 = n := by
 Blueprint supports three main ways to connect informal nodes to Lean:
 
 - inline code with a labeled Lean code block
-- compiled code tagged with `@[blueprint "addition_right_identity"]`
+- compiled code tagged with `@[blueprint]` or
+  `@[blueprint "addition_right_identity"]`
 - existing declarations referenced with `(lean := "Nat.add_assoc")`
 
 ```lean
@@ -152,6 +153,37 @@ theorem nat_add_zero_right (n : Nat) : n + 0 = n := by
   simp
 ```
 
+The string selects a short, explicit Blueprint label. Omitting it uses the
+declaration's qualified Lean name, so `@[blueprint] theorem
+MyProject.nat_add_zero_right ...` is referenced as
+`"MyProject.nat_add_zero_right"`. Attribute options remain available in the
+bare form, for example `@[blueprint (uses := ["addition_spec"])]`.
+
+After importing a Lean module containing tagged declarations, include one node
+per distinct directly owned label as a source-ordered Manual part with:
+
+```lean
+{includeBlueprintModule 0 MyProject.Formalization.Addition (title := "Compiled Addition Results")}
+```
+
+The `import MyProject.Formalization.Addition` statement still belongs in the
+Lean file header. When only one declaration should appear at a particular
+location in an existing Manual chapter, place that node with:
+
+```lean
+{blueprint_node "addition_right_identity"}
+```
+
+The declaration docstring supplies the informal statement when present; without
+one, Blueprint still renders a code-only node in either workflow. Docstrings are
+prose, not Blueprint dependency syntax: put `uses` and `proofUses` on the
+attribute. Standard `doc.verso` structure, including math, is preserved in both
+the statement and the attached “Lean code for…” declaration panel. For the
+precise dependency, prose, proof, metadata, and source-rendering boundaries, see
+the Manual's
+[“Attribute-first use-case matrix”](doc/MANUAL.md#attribute-first-use-case-matrix)
+section.
+
 Add `(autoDeps := true)` when a tagged declaration, labeled inline Lean block,
 or `(lean := "...")` statement should infer statement/proof dependency edges to
 directly referenced Lean declarations that are already associated with Blueprint

doc/API.md

@@ -129,7 +129,8 @@ Generated Blueprint sites write reusable data under `-verso-data/`:
 - `blueprint-manifest.json` contains semantic entries keyed by preview key,
   generated-page hrefs, graph records, labels, dependency data, Lean-code
   associations, a shared group catalog, ownership, tags, priority, effort,
-  status metadata, and display metadata.
+  status metadata, display metadata, and the folding policy needed by reusable
+  block renderers.
 - `blueprint-html-cache.json` contains rendered body fragments keyed by
   preview keys for entries that have generated preview bodies. Some semantic
   entries, such as source-backed external markup generated with
@@ -662,6 +663,19 @@ The useful data boundary is small:
 - Slide generators and other generated consumers should import and use the
   `Informal.Graft` node/config names directly.
 
+Manual documents expose two attribute-owned authoring paths before reaching
+this rendering boundary. `{includeBlueprintModule 0 Some.Module}` reads that
+imported module's persistent, source-ordered label catalog and creates one
+Manual part containing all directly owned nodes. `{blueprint_node "label"}`
+materializes one imported attribute node at the command's source position. In
+both cases a docstring supplies the statement body when present; otherwise a
+code-only preview entry is produced. Ordinary informal nodes must already be
+in the traversal, and Slides always use the manifest/cache supplied by their
+generator. The module command is deliberately Manual-only. Module selection and
+statement-facet materialization are document-elaboration concerns; persisted
+informal proof bodies are not yet materialized from imported modules. The
+config, manifest entry, and rendering APIs below remain shared.
+
 `VersoBlueprint.Graft.Render` packages that lookup-and-render path for custom
 interfaces. A consumer such as an audit view can provide its own wrapper
 classes and diagnostics while reusing the same manifest/cache content:

doc/DESIGN_RATIONALE.md

@@ -1,6 +1,6 @@
 # Blueprint Design Rationale
 
-Last updated: 2026-06-20
+Last updated: 2026-07-25
 
 This document records the current architecture boundaries and the reasons the
 Blueprint implementation is shaped the way it is.
@@ -212,13 +212,19 @@ flowchart TD
 The same flow can be read as four contracts:
 
 1. **Elaboration to environment.**
-   Source directives, inline Lean blocks, `@[blueprint "..."]` attributes,
+   Source directives, inline Lean blocks, `@[blueprint]` attributes with
+   declaration-name or explicit labels,
    external `(lean := "...")` references, group declarations, author
    declarations, citations, and metadata are elaborated into
    `Informal.Environment.State`. This is the canonical semantic store for
    Blueprint-owned facts. It is persisted through Lean environment extensions
    and imported through compiled oleans, so downstream modules see one merged
-   object database.
+   object database. Attribute registration also writes a small per-module
+   catalog of distinct labels that preserves first application order. The node
+   itself remains the single source of truth for associated Lean declarations.
+   This is the ownership and ordering source for `{includeBlueprintModule}`;
+   the include path does not infer chapters by sorting labels or reparsing Lean
+   source.
 
 2. **Environment to traversal.**
    During Verso traversal, Blueprint reads the semantic environment and writes
@@ -229,6 +235,23 @@ The same flow can be read as four contracts:
    public graph data records, and external declaration row anchors. These
    facts are intentionally not pushed back into `Environment.State`, because
    their values depend on the current rendered document and output mode.
+   An imported attribute-owned node has no source block of its own, so a Manual
+   `{blueprint_node}` placement expands to an invisible materialization block
+   followed by the ordinary graft. The materializer writes the same node,
+   statement-preview, Lean-code, anchor, numbering, and relation indexes as an
+   informal statement block; its only HTML is the empty destination anchor
+   immediately before the visible graft. This keeps placement phase-safe
+   without introducing a second renderer for attribute nodes. Persisted
+   provider-module proof bodies are not yet projected into proof-facet traversal
+   entries.
+   `{includeBlueprintModule}` builds a real Verso part by applying that same
+   materializer-plus-graft expansion to every entry in one imported module's
+   catalog. Catalog lookup is exact-module, so transitive imports appear only
+   when explicitly included as their own parts.
+   Statement payloads that already contain elaborated Manual blocks are
+   reconstructed through Manual's typed JSON instances. This is a localized
+   value-quotation bridge, not a second persisted body schema and not a
+   synthetic document elaboration pass.
 
 3. **Traversal to generated artifacts.**
    Page rendering and preview-data emission both consume the traversal state.
@@ -271,10 +294,11 @@ that owner.
 | Fact family | Owner | Stored as | Main consumers |
 | --- | --- | --- | --- |
 | Blueprint labels, node kind, declared dependencies, parent/group, owner, tags, priority, effort, PR URL | Elaboration | `Environment.State.data` and related environment maps | traversal, graph, summary, manifest construction |
+| Attribute-module ownership and first-application order | Attribute elaboration | `Environment.State.blueprintAttributeLabelsByModule`; node semantics remain in `Environment.State.data` | `{includeBlueprintModule}`, exact-module diagnostics |
 | Group and author declarations | Elaboration | `Environment.State.groups` and `Environment.State.authors` | block rendering, summary, graph/group panels |
 | Inline Lean and Rust attachments | Elaboration plus traversal | semantic code refs in environment; render-time code-panel indexes in `TraversalIndex.InlineCode` and `TraversalIndex.RustInlineCode` | block renderers, code panels, manifest entries |
 | External Lean declaration snapshots | Elaboration / declaration snapshot registration | `ExternalRef` records on semantic nodes, enriched with presence/status/source/render data | block renderers, code-summary badges, summary, graph, manifest |
-| Numbering, hrefs, anchors, preview keys | Traversal | `TraverseState` and `TraversalIndex` domains | page rendering, preview manifest, browser triggers |
+| Numbering, hrefs, anchors, preview keys, and placement folding policy | Traversal | `TraverseState` and `TraversalIndex` domains, projected into semantic preview entries where rendering needs them | page rendering, preview manifest, browser triggers |
 | Statement/proof preview source blocks | Traversal | `TraversalIndex.TraversalPreviews` | manifest/cache emission, same-document manual grafts |
 | Public graph data | Elaboration plus completed traversal | semantic `Informal.Graph.GraphModel` plus options cached in `TraversalIndex.Graphs`, then topology-finalized once through `Informal.GraphApi.finishData` into private-constructor `GraphData`; manifest emission subsequently resolves preview candidates against the artifact index without reopening topology | graph command rendering, browser runtime, custom graph consumers |
 | Lean code preview fragments | Traversal | `TraversalIndex.LeanCodePreviews` | Lean links, manifest/cache emission |
@@ -343,6 +367,9 @@ flowchart TD
   previewExtra["Preview-data extra step<br/>emitBlueprintPreviewData"]
   previewFiles["Manifest/cache files<br/>blueprint-manifest.json<br/>blueprint-html-cache.json"]
 
+  attributeEnv["Persistent attribute node/catalog<br/>Environment.State"]
+  moduleInclude["Attribute module part command<br/>includeBlueprintModule"]
+  attributeMaterializer["Attribute traversal materializer<br/>blueprintAttributeNodeSource"]
   manualGraft["Manual graft command<br/>Graft.renderManualGraftNode"]
   traversalPreview["Traversal preview lookup<br/>PreviewSource / TraversalPreviews"]
   manualPreviewHtml["Manual preview-body render<br/>renderManualBlocksHtmlWithStateAndHovers"]
@@ -362,6 +389,10 @@ flowchart TD
   manualMain --> previewExtra
   previewExtra --> previewFiles
 
+  attributeEnv --> moduleInclude
+  attributeEnv --> attributeMaterializer
+  moduleInclude --> attributeMaterializer
+  attributeMaterializer --> traversalPreview
   manualGraft --> traversalPreview
   traversalPreview --> manualPreviewHtml
   manualPreviewHtml --> graftContent
@@ -385,7 +416,8 @@ The current paths are:
 | --- | --- | --- | --- | --- |
 | Normal Manual site pages | `Informal.PreviewManifest.blueprintMainWithPreviewData` | `Environment.State` plus `TraverseState` | `Informal.Block.Render.renderInformalBlockModel` for informal blocks; command-specific renderers for graph, summary, and bibliography | generated Manual HTML pages and assets |
 | Preview manifest/cache emission | `Informal.PreviewManifest.emitBlueprintPreviewData` via `blueprintMainWithPreviewData` | completed Manual `TraverseState` and `TraversalIndex` domains | Manual preview render helpers plus manifest entry builders | `blueprint-manifest.json`, `blueprint-html-cache.json`, merged hover docs |
-| Manual same-document graft | `Informal.Graft.renderManualGraftNode` through `{blueprint_node}` in Manual | current page traversal preview entry and current `TraverseState` | `Informal.Graft.renderNodeWithContent` | grafted Manual HTML block |
+| Manual attribute materialization | `{blueprint_node}` for an untraversed attribute node, or `{includeBlueprintModule}` for a module catalog | persistent node/catalog data from `Environment.State` plus persisted statement blocks | `Block.blueprintAttributeNodeSource` registers through the ordinary block traversal path | current-document traversal entries followed by grafted Manual HTML |
+| Manual same-document graft | `Informal.Graft.renderManualGraftNode` through `{blueprint_node}` in Manual | current page traversal preview entry and current `TraverseState`, whether authored directly or attribute-materialized | `Informal.Graft.renderNodeWithContent` | grafted Manual HTML block |
 | Manual side-by-side graft wrapper | `Block.blueprintGraftSideBySide.toHtml` | already elaborated/rendered child blocks | wrapper only; child nodes follow the Manual graft path | side-by-side Manual HTML wrapper |
 | Slides graft node | `Informal.Slides.slidesMainWithBlueprintPreviews` plus `Informal.Slides.renderBlueprintSlideNode` | serialized manifest/cache files copied from the Blueprint site | `Informal.Graft.renderNodeFromManifestCache` then `renderNodeWithContent` | static slide-node HTML plus slide assets |
 | Slides side-by-side wrapper | `VersoSlides.BlockExt.wrap` emitted by `blueprint_side_by_side` in Slides | already rendered child slide blocks | upstream Slides wrapper; child nodes follow the Slides graft-node path | side-by-side slide HTML wrapper |
@@ -879,6 +911,10 @@ rather than page-local template bodies:
    then hydrates links, math, and related-entry preview panels; it does not
    reconstruct Blueprint block markup or relationship topology from ad hoc
    manifest scans.
+   `VersoBlueprint.ModuleInclude` owns the module-to-part authoring boundary:
+   it reads the persistent attribute catalog, creates the Verso part, and
+   delegates every contained node to the same Manual graft materialization
+   path.
 
 Inline Blueprint references, citation references, and the `used by`/group
 relationship panels are now preview-data callers: the rendered page carries the

doc/GETTING_STARTED.md

@@ -36,9 +36,17 @@ Those labels are the key to the whole system. They are used to:
 - attach inline Lean code with a labeled `lean` code block
 - attach external TeX or Markdown source for porting with `tex` or `md` code
   blocks
-- tag compiled declarations with `@[blueprint "label"]`, optionally using
-  `(autoDeps := true)` or `set_option verso.blueprint.autoDeps true` to infer
-  edges to directly referenced Lean declarations associated with Blueprint labels
+- tag compiled declarations with `@[blueprint]`, which defaults to the
+  qualified declaration name, or `@[blueprint "label"]` for an explicit short
+  label; either form can use `(autoDeps := true)` or
+  `set_option verso.blueprint.autoDeps true` to infer edges to directly
+  referenced Lean declarations associated with Blueprint labels
+- turn the distinct labels owned directly by one imported Lean module into a
+  source-ordered Manual chapter with `{includeBlueprintModule 0 Some.Module}`;
+  declarations that share a label become one node
+- place an imported attribute-owned declaration at a specific chapter location
+  with `{blueprint_node "label"}`; its docstring becomes the statement body and
+  an undocumented declaration renders as a code-only node
 
 If you pick stable labels early, the rest of the project structure becomes much
 easier to maintain.
@@ -93,6 +101,8 @@ Use [project_template/](../project_template/) as the starting point.
 Its key files are:
 
 - `ProjectTemplate/Chapters/Addition.lean`: the first chapter
+- `ProjectTemplate/Formalization/Addition.lean`: an ordinary Lean module whose
+  attribute-owned declarations become a generated chapter
 - `ProjectTemplate/Chapters/Multiplication.lean`: the second chapter
 - `ProjectTemplate/Chapters/Collatz.lean`: a third chapter with a deliberately
   unfinished open problem
@@ -104,16 +114,18 @@ Its key files are:
 The template is intentionally small. It is meant to teach the shape of a
 Blueprint project before you scale it up.
 
-## The three Verso forms to recognize first
+## The four Verso forms to recognize first
 
-If you are new to Verso, there are only three forms you need to understand at
+If you are new to Verso, there are only four forms you need to understand at
 the start:
 
 - `#doc (Manual) "Title" =>` starts a document module
 - `{include 0 Some.Module}` includes a chapter into the top-level file
+- `{includeBlueprintModule 0 Some.Formalization}` turns that imported Lean
+  module's tagged declarations into a generated Manual chapter
 - `:::definition "label_1"` starts a Blueprint block
 
-You can get a long way just by following those three patterns in the template.
+You can get a long way just by following those four patterns in the template.
 
 ## Read the first chapters
 
@@ -141,15 +153,18 @@ small enough to copy and adapt.
 
 The top-level file in
 [project_template/ProjectTemplate/Blueprint.lean](../project_template/ProjectTemplate/Blueprint.lean)
-does two jobs:
+does three jobs:
 
 1. it includes the chapter modules into the document
-2. it chooses which rendered overview pages to include
+2. it projects the tagged formalization module into a generated chapter
+3. it chooses which rendered overview pages to include
 
 The starter template includes:
 
 - the chapter pages with `{include 0 ProjectTemplate.Chapters.Addition}` and
   the other chapter includes
+- the compiled-results page with
+  `{includeBlueprintModule 0 ProjectTemplate.Formalization.Addition ...}`
 - a dependency graph with `{blueprint_graph}`
 - a progress summary with `{blueprint_summary}`
 

doc/MAINTAINER_GUIDE.md

@@ -1,6 +1,6 @@
 # Blueprint Maintainer Guide
 
-Last updated: 2026-05-04
+Last updated: 2026-07-25
 
 This document is the repository-level workflow guide for maintaining Blueprint
 support in `verso-blueprint`, its in-repo validation projects, and its
@@ -147,6 +147,26 @@ interaction behavior:
 uv run --project tests/browser --extra test python -m pytest tests/browser -q --browser chromium
 ```
 
+### Cover Feature Intersections
+
+User-facing authoring behavior should be tested through its final rendered
+surface, not only at the parser or environment-extension boundary. For a feature
+that crosses phases, cover the applicable rows of this matrix:
+
+| Boundary | What to assert | Current attribute-first fixtures |
+| --- | --- | --- |
+| Declaration and import | persisted label, declaration association, dependencies, module ownership/order | `BlueprintAttribute.lean` with `BlueprintAttribute/Provider.lean`, `HybridProvider.lean`, and `DefaultLabelProvider.lean` |
+| Consumer traversal | numbering, folding/options, relation data, preview keys | `BlueprintAttributeRendering.lean` |
+| Final Manual HTML | statement body, code-only fallback, structural docstrings/math, code-panel disclosure state | `BlueprintAttributeRendering.lean` |
+| Generated site | embedded assets and the reusable external-declaration renderer | `preview_runtime_showcase` and `check_blueprint_code_panels.py` |
+| Browser runtime | transformations or hydration that cannot be proved from static HTML | `test_preview_runtime_regressions.py` |
+
+When a new option or source form applies to more than one placement path, add
+one compact cross-feature regression that exercises those paths together. A
+unit test for each isolated component is not sufficient when data is projected
+through the environment, traversal store, preview manifest, HTML cache, and
+browser runtime.
+
 Browser tests that need the public Blueprint render API should use
 `blueprint_render_api_script` or `wait_for_blueprint_render_api` from
 `tests/browser/support.py`. Those helpers import