feat: distinguish original-source identities

README.md

@@ -258,6 +258,8 @@ source := {
   spans := #[
     {
       page := "12"
+      anchor := "lem:addition-right-identity"
+      citation := "Lemma 2.1(1)"
       pdf := some { path := "source/pages/page-12.pdf" }
     }
   ]
@@ -269,7 +271,12 @@ For every natural number $`n`, $`n + 0 = n`.
 ````
 
 Current behavior: source provenance is exported in the Blueprint manifest as
-`sourceDocuments` and per-entry `sources`, and kept hidden in rendered pages.
+`sourceDocuments` and per-entry `sources`. A sourced node shows a compact chip;
+when an entry has exactly one source ref and that ref has one unique citation,
+the chip says, for example, `source: Lemma 2.1(1)` rather than presenting the
+citation as Blueprint's own generated number. Entries with multiple source refs
+retain the `sources N` summary so that the chip does not hide aggregated
+provenance.
 Browser clients can resolve source-document ids with `loadSourceDocument`, load
 the complete catalog with `loadSourceDocuments`, or join entry source refs with
 declared documents using `resolveSourceMetadata` from `api/data.mjs` or

doc/API.md

@@ -1239,7 +1239,14 @@ a `reason` and `diagnosticHtml` suitable for insertion into the page.
 `resolveSourceMetadata` is data-only: it returns source metadata and failure
 reasons, but no rendered HTML. It also does not load source PDFs, extracted
 text, or page images; callers use the returned paths and spans in the source UI
-they own.
+they own. Each span may carry a source-native `anchor` (for example a TeX
+`\label`) and a human-readable `citation` (for example `Lemma 2.1(1)`) in
+addition to its optional page, text range, and PDF location.
+
+Generated JSON includes every source-provenance field. Fields backed by Lean
+`Option` values are encoded as either their documented value or `null`, rather
+than being omitted. In particular, clients must handle page-less spans as
+`page: null` and use their anchor, text range, or PDF location instead.
 
 | Helper | Success shape | Failure shape |
 | --- | --- | --- |

doc/DESIGN_RATIONALE.md

@@ -1,6 +1,6 @@
 # Blueprint Design Rationale
 
-Last updated: 2026-06-20
+Last updated: 2026-07-17
 
 This document records the current architecture boundaries and the reasons the
 Blueprint implementation is shaped the way it is.
@@ -46,6 +46,23 @@ traversal/rendering pass answers "how do these objects sit inside this rendered
 site?" Rendering and UI layers are expected to project from those two stages
 rather than invent parallel sources of truth.
 
+### Blueprint Identity and Original-Source Identity
+
+Blueprint labels and traversal-generated heading numbers identify nodes inside
+the Blueprint site. They must remain independent of identities inherited from
+an original TeX, PDF, or text source. A source span may therefore record a
+stable source-native `anchor` and a human-facing `citation` either alongside
+physical page, text, or PDF locations or, for an anchor-only span, instead of
+them. For example, a node generated as `Lemma 2.2` can point to `itm:ib-first`
+and display `source: Lemma 2.1(1)` without changing its graph key,
+cross-references, or intrinsic numbering.
+
+The source anchor is machine identity; the citation is presentation. Neither is
+reconstructed from visible prose, and neither is used as a substitute for the
+Blueprint node label. This is particularly important for Blueprints generated
+from TeX, where definitions or split list items may consume different
+Blueprint counters than the source theorem environment.
+
 ### Command Split
 
 Command modules are split by concern:

doc/MANUAL.md

@@ -646,6 +646,8 @@ source := {
   spans := #[
     {
       page := "12"
+      anchor := "lem:addition-right-identity"
+      citation := "Lemma 2.1(1)"
       text := some {
         path := "source/pages/page-12.md"
         startLine := 41
@@ -667,8 +669,53 @@ For every natural number $`n`, $`n + 0 = n`.
 The generated manifest exports declared documents in `sourceDocuments` and each
 manifest entry's original-source refs in `entry.sources`. Normal generated node
 shells also show a compact source chip when source provenance is present; open
-it to inspect the source document id, page summary, and recorded text/PDF span
-details.
+it to inspect the source document id, source-native anchor and citation, page
+summary, and recorded text/PDF span details.
+
+When an entry has exactly one source ref with one unique citation, the chip
+displays that citation as `source: ...`. A single ref without a unique citation
+uses `source 1`; entries that aggregate several refs use `sources N` so the
+compact label does not hide additional provenance.
+
+`anchor` is a stable identifier in the original source, such as a TeX
+`\label`; `citation` is the corresponding human-readable source identity, such
+as `Lemma 2.1(1)` or `Equation (2.4)`. These fields do not replace the
+Blueprint node's label or generated heading number. A node may therefore remain
+`Lemma 2.2` in the Blueprint while its source chip explicitly reads
+`source: Lemma 2.1(1)`. Keeping the identities separate avoids silently
+changing graph keys, Blueprint references, or site-local numbering to imitate
+the source document.
+
+For a text source such as the TeX input itself, omit `page` and use a source
+anchor, a text line range, or both:
+
+````md
+:::source_document "paper-tex"
+%%%
+title := "Representation Theory (TeX source)"
+kind := .text
+%%%
+:::
+
+:::lemma_ "addition_right_identity"
+%%%
+source := {
+  document := "paper-tex"
+  spans := #[{
+    anchor := "itm:addition-right-identity"
+    citation := "Lemma 2.1(1)"
+    text := some {
+      path := "paper.tex"
+      startLine := 439
+      endLine := 440
+    }
+  }]
+}
+%%%
+
+For every natural number $`n`, $`n + 0 = n`.
+:::
+````
 
 Manifest clients should read `entry.sources`; there is no singular
 `entry.source` field. Lean code preview entries may contain multiple refs when
@@ -684,8 +731,8 @@ read the complete catalog with `loadSourceDocuments`.
 
 Browser clients can call `resolveSourceMetadata` from `api/data.mjs` or
 `api/preview.mjs` to resolve source refs for a preview key, manifest entry, or
-render result. The API returns structured source-document metadata and recorded
-text/PDF spans.
+render result. The API returns structured source-document metadata, source
+identities, and text/PDF spans.
 Manifest entries also include `sourceLocation`, a lookup result for the authored
 Blueprint label/facet location or Lean declaration source. Browser clients that
 start from semantic names can call `resolveLabel`, or `resolveDeclaration` for

src/VersoBlueprint/Informal/Block/Render.lean

@@ -270,6 +270,20 @@ private def externalMarkupBadgeText : Data.ExternalMarkupLanguage → String
 private def pushUniqueString (values : Array String) (value : String) : Array String :=
   if values.contains value then values else values.push value
 
+private def trimmedOptionalString (value? : Option String) : Option String := do
+  let rawValue ← value?
+  let value := rawValue.trimAscii.toString
+  if value.isEmpty then none else some value
+
+private def collectTrimmedUniqueBy {α : Type} (values : Array α)
+    (value? : α → Option String) : Array String :=
+  values.foldl
+    (init := #[])
+    fun collected item =>
+      match trimmedOptionalString (value? item) with
+      | some value => pushUniqueString collected value
+      | none => collected
+
 private def externalMarkupLanguages (markup : Array Data.ExternalMarkup) :
     Array Data.ExternalMarkupLanguage :=
   markup.foldl
@@ -369,11 +383,7 @@ private def renderMetadataCodeLinkValue (href : String) (value : Data.AuthorId)
   {{<a class="bp_metadata_link bp_metadata_value" href={{href}}><code>s!"{value}"</code></a>}}
 
 private def sourceSpanPages (spans : Array Source.Span) : Array String :=
-  spans.foldl
-    (init := #[])
-    fun pages span =>
-      let page := span.page.trimAscii.toString
-      if page.isEmpty then pages else pushUniqueString pages page
+  collectTrimmedUniqueBy spans (·.page)
 
 private def sourcePagesSummary (pages : Array String) : String :=
   match pages.toList with
@@ -394,10 +404,16 @@ private def sourcePdfSpanSummary (span : Source.PdfSpan) : String :=
   | Option.some image => s!"pdf {span.path}; image {image}"
   | Option.none => s!"pdf {span.path}"
 
+private def pushOptionalSourceSummary (parts : Array String) (key : String)
+    (value? : Option String) : Array String :=
+  match trimmedOptionalString value? with
+  | some value => parts.push s!"{key} {value}"
+  | none => parts
+
 private def sourceSpanSummary (span : Source.Span) : String :=
-  let page := span.page.trimAscii.toString
-  let parts : Array String :=
-    if page.isEmpty then #[] else #[s!"page {page}"]
+  let parts := pushOptionalSourceSummary #[] "citation" span.citation
+  let parts := pushOptionalSourceSummary parts "anchor" span.anchor
+  let parts := pushOptionalSourceSummary parts "page" span.page
   let parts :=
     match span.text with
     | Option.some textRange => parts.push (sourceTextRangeSummary textRange)
@@ -408,6 +424,9 @@ private def sourceSpanSummary (span : Source.Span) : String :=
     | Option.none => parts
   String.intercalate "; " parts.toList
 
+private def sourceSpanCitations (spans : Array Source.Span) : Array String :=
+  collectTrimmedUniqueBy spans (·.citation)
+
 private def sourceRefSummary (sourceRef : Source.Ref) : String :=
   let pages := sourceSpanPages sourceRef.spans
   let pageSummary := sourcePagesSummary pages
@@ -425,10 +444,12 @@ private def sourceRefTitle (sourceRef : Source.Ref) : String :=
     s!"Original source document {sourceRef.document}: {String.intercalate " | " spanSummary}"
 
 private def sourceRefsChipText (sourceRefs : Array Source.Ref) : String :=
-  if sourceRefs.size == 1 then
-    "source 1"
-  else
-    s!"sources {sourceRefs.size}"
+  match sourceRefs.toList with
+  | [sourceRef] =>
+      match sourceSpanCitations sourceRef.spans |>.toList with
+      | [citation] => s!"source: {citation}"
+      | _ => "source 1"
+  | _ => s!"sources {sourceRefs.size}"
 
 private def sourceRefsPanelTitle (sourceRefs : Array Source.Ref) : String :=
   if sourceRefs.size == 1 then
@@ -452,7 +473,7 @@ private def sourceRefsChipTitle (sourceRefs : Array Source.Ref) : String :=
 private def sourceSpanPreviewText (span : Source.Span) : String :=
   let summary := sourceSpanSummary span
   if summary.isEmpty then
-    "Source span recorded without page, text, or PDF location"
+    "Source span recorded without page, anchor, text, or PDF location"
   else
     summary
 

src/VersoBlueprint/PreviewManifest.lean

@@ -686,7 +686,7 @@ This is a VBP stale-artifact diagnostic marker, not a public interchange
 version. It may change whenever the generated-data reader needs a clean
 validation boundary.
 -/
-def manifestInternalSchemaVersion : Nat := 3
+def manifestInternalSchemaVersion : Nat := 4
 
 def manifestInternalSchemaVersionField : String := "vbpInternalSchemaVersion"
 
@@ -1791,18 +1791,31 @@ private partial def schemaForType (ty : Expr) : StateT SchemaState MetaM Json :=
       modify fun st => { st with seen := st.seen.insert name }
       let env ← getEnv
       if let some info := getStructureInfo? env name then
-        let mut properties : List (String × Json) := []
-        let mut required : Array Json := #[]
-        for fieldInfo in info.fieldInfo do
-          let schema ← schemaForType (← fieldType fieldInfo.projFn)
-          let docs? ← findDocString? env fieldInfo.projFn
-          let schema :=
-            match docs? with
-            | some docs => schemaWithDescription schema docs
-            | none => schema
-          let key := fieldKey fieldInfo.fieldName
-          properties := properties.concat (key, schema)
-          required := required.push (Json.str key)
+        let rec collectFields (info : StructureInfo) :
+            StateT SchemaState MetaM (List (String × Json) × Array Json) := do
+          let mut properties : List (String × Json) := []
+          let mut required : Array Json := #[]
+          for fieldInfo in info.fieldInfo do
+            match fieldInfo.subobject? with
+            | some parentName =>
+                -- Derived JSON flattens embedded parent structures into the child object.
+                let some parentInfo := getStructureInfo? env parentName
+                  | throwError "Unsupported schema parent structure: {parentName}"
+                let (parentProperties, parentRequired) ← collectFields parentInfo
+                properties := properties ++ parentProperties
+                required := required ++ parentRequired
+            | none =>
+                let schema ← schemaForType (← fieldType fieldInfo.projFn)
+                let docs? ← findDocString? env fieldInfo.projFn
+                let schema :=
+                  match docs? with
+                  | some docs => schemaWithDescription schema docs
+                  | none => schema
+                let key := fieldKey fieldInfo.fieldName
+                properties := properties.concat (key, schema)
+                required := required.push (Json.str key)
+          pure (properties, required)
+        let (properties, required) ← collectFields info
         let schema := Json.mkObj [
           ("type", Json.str "object"),
           ("properties", Json.mkObj properties),

src/VersoBlueprint/Source/Data.lean

@@ -70,7 +70,8 @@ def ValidationError.message : ValidationError → String
   | .pdfBoxInvalidYRange => "source PDF box yMin must be less than yMax"
   | .pdfBoxXMaxBeyondPageWidth => "source PDF box xMax must be within pageWidth"
   | .pdfBoxYMaxBeyondPageHeight => "source PDF box yMax must be within pageHeight"
-  | .spanMissingLocation => "source spans require text or PDF location data"
+  | .spanMissingLocation =>
+      "source spans require a page, source anchor, text range, or PDF location"
   | .refMissingSpan => "source metadata must include at least one source span"
 
 instance : ToString ValidationError where
@@ -160,14 +161,26 @@ def PdfSpan.validationErrors (span : PdfSpan) : Array ValidationError :=
 
 /-- One source span attached to a Blueprint node. -/
 structure Span where
-  page : String
+  /-- Optional source-local page identifier. Text sources do not need one. -/
+  page : Option String := none
+  /-- Stable source-native identifier, such as a TeX `\label`. -/
+  anchor : Option String := none
+  /-- Human-readable source-native reference, such as `Lemma 2.1(1)`. -/
+  citation : Option String := none
   text : Option TextRange := none
   pdf : Option PdfSpan := none
 deriving Inhabited, Repr, BEq, DecidableEq, FromJson, ToJson, Quote
 
 def Span.validationErrors (span : Span) : Array ValidationError :=
-  let errors := nonEmptyField "source span page" span.page
-  let errors := addIf errors (span.text.isNone && span.pdf.isNone) .spanMissingLocation
+  let errors : Array ValidationError := #[]
+  let errors := addOptional errors span.page (nonEmptyField "source span page")
+  let errors := addOptional errors span.anchor (nonEmptyField "source span anchor")
+  let errors := addOptional errors span.citation (nonEmptyField "source span citation")
+  let hasPage := span.page.any fun page => !page.trimAscii.isEmpty
+  let hasAnchor := span.anchor.any fun anchor => !anchor.trimAscii.isEmpty
+  let errors := addIf errors
+    (!hasPage && !hasAnchor && span.text.isNone && span.pdf.isNone)
+    .spanMissingLocation
   let errors := addOptional errors span.text TextRange.validationErrors
   addOptional errors span.pdf PdfSpan.validationErrors
 

src/VersoBlueprint/blueprint-api-types.mjs

@@ -175,9 +175,9 @@
  * @property {string} id Canonical source-document id.
  * @property {string} title Human-readable source title.
  * @property {"pdf" | "text" | string} kind Broad source-document kind.
- * @property {string} [pdf] Source PDF path, when the document is PDF-backed.
- * @property {string} [pageRoot] Optional root for extracted source pages.
- * @property {string} [imageRoot] Optional root for extracted page images.
+ * @property {string | null} pdf Source PDF path, or `null` when the document is not PDF-backed.
+ * @property {string | null} pageRoot Root for extracted source pages, or `null` when unavailable.
+ * @property {string | null} imageRoot Root for extracted page images, or `null` when unavailable.
  */
 
 /**
@@ -187,8 +187,8 @@
  * @property {string} path Source text path.
  * @property {number} startLine One-based inclusive start line.
  * @property {number} endLine One-based inclusive end line.
- * @property {number} [startCharacter] Optional start character.
- * @property {number} [endCharacter] Optional end character.
+ * @property {number | null} startCharacter Start character, or `null` when the span covers whole lines.
+ * @property {number | null} endCharacter End character, or `null` when the span covers whole lines.
  */
 
 /**
@@ -209,17 +209,19 @@
  *
  * @typedef {Object} BlueprintSourcePdfSpan
  * @property {string} path Source PDF page path.
- * @property {string} [image] Optional rendered page image path.
- * @property {BlueprintSourcePdfBox} [box] Optional crop box.
+ * @property {string | null} image Rendered page image path, or `null` when unavailable.
+ * @property {BlueprintSourcePdfBox | null} box Crop box, or `null` when the span covers the page.
  */
 
 /**
  * One original source span attached to a Blueprint node.
  *
  * @typedef {Object} BlueprintSourceSpan
- * @property {string} page Source-local page identifier.
- * @property {BlueprintSourceTextRange} [text] Text location for this span.
- * @property {BlueprintSourcePdfSpan} [pdf] PDF/page-image location for this span.
+ * @property {string | null} page Source-local page identifier, or `null` for a page-less span.
+ * @property {string | null} anchor Stable source-native identifier, such as a TeX `\\label`, or `null` when unavailable.
+ * @property {string | null} citation Human-readable source-native reference, such as `Lemma 2.1(1)`, or `null` when unavailable.
+ * @property {BlueprintSourceTextRange | null} text Text location, or `null` when unavailable.
+ * @property {BlueprintSourcePdfSpan | null} pdf PDF/page-image location, or `null` when unavailable.
  */
 
 /**

tests/VersoBlueprintTests/BlueprintExternalMarkup.lean

@@ -52,7 +52,7 @@ private def entryHasSourcePage
     (entry : Informal.PreviewManifest.Entry) (document page : String) : Bool :=
   entry.sources.any fun sourceRef =>
     sourceRef.document == document &&
-      sourceRef.spans.any (fun span => span.page == page)
+      sourceRef.spans.any (fun span => span.page == some page)
 
 private def htmlHasSourcePreview (html document pageText : String) : Bool :=
   hasSubstr html "bp_extra_slot_source" &&
@@ -963,7 +963,7 @@ external markup.
       sourcedWitnessEntry.sources.any (fun sourceRef =>
         sourceRef.document == "external-paper" &&
           sourceRef.spans.size == 1 &&
-          sourceRef.spans[0]!.page == "7") &&
+          sourceRef.spans[0]!.page == some "7") &&
       htmlHasSourcePreview sourcedWitnessHtml "external-paper" "p. 7" &&
       hasSubstr externalOut "bp_extra_slot_markup" &&
       hasSubstr externalOut "bp_external_markup_badge_markdown" &&