diff --git a/README.md b/README.md
index 09cd42be..e322d668 100644
--- a/README.md
+++ b/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
diff --git a/doc/API.md b/doc/API.md
index 829f9a82..22fb8b62 100644
--- a/doc/API.md
+++ b/doc/API.md
@@ -1215,7 +1215,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 |
 | --- | --- | --- |
diff --git a/doc/DESIGN_RATIONALE.md b/doc/DESIGN_RATIONALE.md
index 3411899e..3d3ba529 100644
--- a/doc/DESIGN_RATIONALE.md
+++ b/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:
diff --git a/doc/MANUAL.md b/doc/MANUAL.md
index f49585db..46b659d5 100644
--- a/doc/MANUAL.md
+++ b/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
diff --git a/src/VersoBlueprint/Informal/Block/Render.lean b/src/VersoBlueprint/Informal/Block/Render.lean
index 4d4ccc1d..286756e1 100644
--- a/src/VersoBlueprint/Informal/Block/Render.lean
+++ b/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
 
diff --git a/src/VersoBlueprint/PreviewManifest.lean b/src/VersoBlueprint/PreviewManifest.lean
index 13b9dcbd..f902e4c5 100644
--- a/src/VersoBlueprint/PreviewManifest.lean
+++ b/src/VersoBlueprint/PreviewManifest.lean
@@ -694,7 +694,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"
 
@@ -1697,18 +1697,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),
diff --git a/src/VersoBlueprint/Source/Data.lean b/src/VersoBlueprint/Source/Data.lean
index 69960207..6e43230b 100644
--- a/src/VersoBlueprint/Source/Data.lean
+++ b/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
 
diff --git a/src/VersoBlueprint/blueprint-api-types.mjs b/src/VersoBlueprint/blueprint-api-types.mjs
index a296450c..c688a25c 100644
--- a/src/VersoBlueprint/blueprint-api-types.mjs
+++ b/src/VersoBlueprint/blueprint-api-types.mjs
@@ -173,9 +173,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.
  */
 
 /**
@@ -185,8 +185,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.
  */
 
 /**
@@ -207,17 +207,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.
  */
 
 /**
diff --git a/tests/VersoBlueprintTests/BlueprintExternalMarkup.lean b/tests/VersoBlueprintTests/BlueprintExternalMarkup.lean
index 0c692f37..edcaa498 100644
--- a/tests/VersoBlueprintTests/BlueprintExternalMarkup.lean
+++ b/tests/VersoBlueprintTests/BlueprintExternalMarkup.lean
@@ -48,7 +48,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" &&
@@ -951,7 +951,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" &&
diff --git a/tests/VersoBlueprintTests/BlueprintPreviewSchema.lean b/tests/VersoBlueprintTests/BlueprintPreviewSchema.lean
index ef2e9efb..0ef73dee 100644
--- a/tests/VersoBlueprintTests/BlueprintPreviewSchema.lean
+++ b/tests/VersoBlueprintTests/BlueprintPreviewSchema.lean
@@ -31,10 +31,61 @@ open Informal.PreviewManifest
         fromJson? (α := Array String) requiredJson |>.toOption
       let some relatedEntrySchema := defs.get? "Informal.PreviewManifest.RelatedEntry" | return false
       let some graphNodeSchema := defs.get? "Informal.Graph.NodeData" | return false
+      let some sourceDocumentSchema := defs.get? "Informal.Source.Document" | return false
+      let Except.ok sourceDocumentPropsJson :=
+        Json.getObjVal? sourceDocumentSchema "properties" | return false
+      let Except.ok sourceDocumentProps := sourceDocumentPropsJson.getObj? | return false
+      let sourceDocumentRequired? := do
+        let requiredJson ← sourceDocumentSchema.getObjVal? "required" |>.toOption
+        fromJson? (α := Array String) requiredJson |>.toOption
+      let some sourceSpanSchema := defs.get? "Informal.Source.Span" | return false
+      let Except.ok sourceSpanPropsJson := Json.getObjVal? sourceSpanSchema "properties" | return false
+      let Except.ok sourceSpanProps := sourceSpanPropsJson.getObj? | return false
+      let sourceSpanRequired? := do
+        let requiredJson ← sourceSpanSchema.getObjVal? "required" |>.toOption
+        fromJson? (α := Array String) requiredJson |>.toOption
+      let some sourceTextRangeSchema := defs.get? "Informal.Source.TextRange" | return false
+      let Except.ok sourceTextRangePropsJson :=
+        Json.getObjVal? sourceTextRangeSchema "properties" | return false
+      let Except.ok sourceTextRangeProps := sourceTextRangePropsJson.getObj? | return false
+      let sourceTextRangeRequired? := do
+        let requiredJson ← sourceTextRangeSchema.getObjVal? "required" |>.toOption
+        fromJson? (α := Array String) requiredJson |>.toOption
+      let some sourcePdfSpanSchema := defs.get? "Informal.Source.PdfSpan" | return false
+      let Except.ok sourcePdfSpanPropsJson :=
+        Json.getObjVal? sourcePdfSpanSchema "properties" | return false
+      let Except.ok sourcePdfSpanProps := sourcePdfSpanPropsJson.getObj? | return false
+      let sourcePdfSpanRequired? := do
+        let requiredJson ← sourcePdfSpanSchema.getObjVal? "required" |>.toOption
+        fromJson? (α := Array String) requiredJson |>.toOption
       let schemaText := schema.compress
       let stringSchemaHasMinLengthOne (schema : Json) : Bool :=
         (schema.getObjValAs? String "type" |>.toOption) == some "string" &&
           (schema.getObjValAs? Nat "minLength" |>.toOption) == some 1
+      let stringSchema (schema : Json) : Bool :=
+        (schema.getObjValAs? String "type" |>.toOption) == some "string"
+      let integerSchema (schema : Json) : Bool :=
+        (schema.getObjValAs? String "type" |>.toOption) == some "integer"
+      let refSchema (expected : String) (schema : Json) : Bool :=
+        (schema.getObjValAs? String "$ref" |>.toOption) == some expected
+      let schemaHasValueNull (valueSchema : Json → Bool) (schema : Json) : Bool :=
+        match Json.getObjVal? schema "anyOf" with
+        | Except.error _ => false
+        | Except.ok anyOfJson =>
+            match anyOfJson.getArr? with
+            | Except.error _ => false
+            | Except.ok schemas =>
+                schemas.any valueSchema &&
+                schemas.any (fun (schema : Json) =>
+                  (schema.getObjValAs? String "type" |>.toOption) == some "null")
+      let schemaHasStringNull (schema : Json) : Bool :=
+        schemaHasValueNull stringSchema schema
+      let schemaHasNonEmptyStringNull (schema : Json) : Bool :=
+        schemaHasValueNull stringSchemaHasMinLengthOne schema
+      let schemaHasIntegerNull (schema : Json) : Bool :=
+        schemaHasValueNull integerSchema schema
+      let schemaHasRefNull (expected : String) (schema : Json) : Bool :=
+        schemaHasValueNull (refSchema expected) schema
       let previewKeySchemaHasNonEmptyStringNull (schema : Json) : Bool :=
         match Json.getObjVal? schema "properties" with
         | Except.error _ => false
@@ -44,16 +95,7 @@ open Informal.PreviewManifest
             | Except.ok props =>
                 match props.get? "previewKey" with
                 | none => false
-                | some previewKeyJson =>
-                    match Json.getObjVal? previewKeyJson "anyOf" with
-                    | Except.error _ => false
-                    | Except.ok anyOfJson =>
-                        match anyOfJson.getArr? with
-                        | Except.error _ => false
-                        | Except.ok schemas =>
-                            schemas.any stringSchemaHasMinLengthOne &&
-                            schemas.any (fun (schema : Json) =>
-                              (schema.getObjValAs? String "type" |>.toOption) == some "null")
+                | some previewKeyJson => schemaHasNonEmptyStringNull previewKeyJson
       let internalSchemaDesc? := do
         let internalSchemaJson ← fileProps.get? "vbpInternalSchemaVersion"
         internalSchemaJson.getObjValAs? String "description" |>.toOption
@@ -81,6 +123,10 @@ open Informal.PreviewManifest
         authoredLabelJson.getObjValAs? String "description" |>.toOption
       let some fileRequired := fileRequired? | return false
       let some entryRequired := entryRequired? | return false
+      let some sourceDocumentRequired := sourceDocumentRequired? | return false
+      let some sourceSpanRequired := sourceSpanRequired? | return false
+      let some sourceTextRangeRequired := sourceTextRangeRequired? | return false
+      let some sourcePdfSpanRequired := sourcePdfSpanRequired? | return false
       let some useRefProps := useRefProps? | return false
       let displayCaptionDesc? := do
         let displayCaptionJson ← entryProps.get? "displayCaption"
@@ -157,10 +203,46 @@ open Informal.PreviewManifest
         defs.contains "Informal.Data.ExternalMarkupLocation" &&
         defs.contains "Informal.Source.Document" &&
         defs.contains "Informal.Source.DocumentKind" &&
+        !sourceDocumentProps.contains "toDocumentMetadata" &&
+        sourceDocumentRequired.contains "id" &&
+        sourceDocumentRequired.contains "title" &&
+        sourceDocumentRequired.contains "kind" &&
+        sourceDocumentRequired.contains "pdf" &&
+        sourceDocumentRequired.contains "pageRoot" &&
+        sourceDocumentRequired.contains "imageRoot" &&
+        (sourceDocumentProps.get? "pdf").any schemaHasStringNull &&
+        (sourceDocumentProps.get? "pageRoot").any schemaHasStringNull &&
+        (sourceDocumentProps.get? "imageRoot").any schemaHasStringNull &&
         defs.contains "Informal.Source.Ref" &&
         defs.contains "Informal.Source.Span" &&
+        sourceSpanProps.contains "page" &&
+        sourceSpanProps.contains "anchor" &&
+        sourceSpanProps.contains "citation" &&
+        sourceSpanProps.contains "text" &&
+        sourceSpanProps.contains "pdf" &&
+        sourceSpanRequired.contains "page" &&
+        sourceSpanRequired.contains "anchor" &&
+        sourceSpanRequired.contains "citation" &&
+        sourceSpanRequired.contains "text" &&
+        sourceSpanRequired.contains "pdf" &&
+        (sourceSpanProps.get? "page").any schemaHasStringNull &&
+        (sourceSpanProps.get? "anchor").any schemaHasStringNull &&
+        (sourceSpanProps.get? "citation").any schemaHasStringNull &&
+        (sourceSpanProps.get? "text").any
+          (schemaHasRefNull "#/$defs/Informal.Source.TextRange") &&
+        (sourceSpanProps.get? "pdf").any
+          (schemaHasRefNull "#/$defs/Informal.Source.PdfSpan") &&
         defs.contains "Informal.Source.TextRange" &&
+        sourceTextRangeRequired.contains "startCharacter" &&
+        sourceTextRangeRequired.contains "endCharacter" &&
+        (sourceTextRangeProps.get? "startCharacter").any schemaHasIntegerNull &&
+        (sourceTextRangeProps.get? "endCharacter").any schemaHasIntegerNull &&
         defs.contains "Informal.Source.PdfSpan" &&
+        sourcePdfSpanRequired.contains "image" &&
+        sourcePdfSpanRequired.contains "box" &&
+        (sourcePdfSpanProps.get? "image").any schemaHasStringNull &&
+        (sourcePdfSpanProps.get? "box").any
+          (schemaHasRefNull "#/$defs/Informal.Source.PdfBox") &&
         defs.contains "Informal.Source.PdfBox" &&
         defs.contains "Informal.Data.SourceLocation" &&
         defs.contains "Informal.Data.SourceLocationResult" &&
diff --git a/tests/VersoBlueprintTests/BlueprintSource.lean b/tests/VersoBlueprintTests/BlueprintSource.lean
index be1516f9..df17cf27 100644
--- a/tests/VersoBlueprintTests/BlueprintSource.lean
+++ b/tests/VersoBlueprintTests/BlueprintSource.lean
@@ -20,7 +20,10 @@ private def sourcedLabel : Name := Name.mkSimple "source.lemma"
 private def secondSourcedLabel : Name := Name.mkSimple "source.second"
 
 private def sourceRefHasPage (document page : String) (sourceRef : Informal.Source.Ref) : Bool :=
-  sourceRef.document == document && sourceRef.spans.any (fun span => span.page == page)
+  sourceRef.document == document && sourceRef.spans.any (fun span => span.page == some page)
+
+private def sourceRefHasAnchor (document anchor : String) (sourceRef : Informal.Source.Ref) : Bool :=
+  sourceRef.document == document && sourceRef.spans.any (fun span => span.anchor == some anchor)
 
 private def entryHasSourcePage
     (document page : String) (entry : Informal.PreviewManifest.Entry) : Bool :=
@@ -30,11 +33,21 @@ private def entryOptionHasSourcePage
     (document page : String) (entry? : Option Informal.PreviewManifest.Entry) : Bool :=
   entry?.any fun entry => entryHasSourcePage document page entry
 
+private def entryHasSourceAnchor
+    (document anchor : String) (entry : Informal.PreviewManifest.Entry) : Bool :=
+  entry.hasSourceDocument document && entry.sources.any (sourceRefHasAnchor document anchor)
+
+private def entryOptionHasSourceAnchor
+    (document anchor : String) (entry? : Option Informal.PreviewManifest.Entry) : Bool :=
+  entry?.any fun entry => entryHasSourceAnchor document anchor entry
+
 private def sourceRefHasRepresentationTheorySpan (sourceRef : Informal.Source.Ref) : Bool :=
   sourceRef.document == "paper" &&
     sourceRef.spans.any fun span =>
       let boxXMax := (span.pdf.bind (·.box)).map (·.xMax)
-      span.page == "12" &&
+      span.page == some "12" &&
+        span.anchor == some "lem:representation" &&
+        span.citation == some "Lemma 4.2" &&
         span.text.map (·.path) == some "source/pages/page-12.md" &&
         span.text.map (·.startLine) == some 41 &&
         span.text.map (·.endLine) == some 45 &&
@@ -69,6 +82,8 @@ source := {
   spans := #[
     {
       page := "12"
+      anchor := "lem:representation"
+      citation := "Lemma 4.2"
       text := some {
         path := "source/pages/page-12.md"
         startLine := 41
@@ -101,9 +116,10 @@ source := {
   document := "notes"
   spans := #[
     {
-      page := "A"
+      anchor := "itm:addition-right-identity"
+      citation := "Lemma 2.1(1)"
       text := some {
-        path := "source/notes/addition.md"
+        path := "source/notes/addition.tex"
         startLine := 1
         endLine := 3
       }
@@ -250,13 +266,69 @@ Invalid source metadata.
     let refErrors :=
       Informal.Source.Ref.validationErrors
         ({ document := "paper" } : Informal.Source.Ref)
+    let citationOnlySpanErrors :=
+      Informal.Source.Span.validationErrors
+        ({ citation := "Lemma 2.1(1)" } : Informal.Source.Span)
+    let anchorOnlySpanErrors :=
+      Informal.Source.Span.validationErrors
+        ({ anchor := "itm:addition-right-identity" } : Informal.Source.Span)
+    let anchoredTextSpanErrors :=
+      Informal.Source.Span.validationErrors
+        ({
+          anchor := "itm:addition-right-identity"
+          citation := "Lemma 2.1(1)"
+          text := some { path := "source.tex", startLine := 1, endLine := 3 }
+        } : Informal.Source.Span)
     let expectedDocumentErrors : Array Informal.Source.ValidationError := #[
       .emptyField "source document id",
       .pdfDocumentMissingPath
     ]
     let expectedRefErrors : Array Informal.Source.ValidationError := #[.refMissingSpan]
     documentErrors == expectedDocumentErrors &&
-      refErrors == expectedRefErrors
+      refErrors == expectedRefErrors &&
+      citationOnlySpanErrors == #[.spanMissingLocation] &&
+      anchorOnlySpanErrors.isEmpty &&
+      anchoredTextSpanErrors.isEmpty
+
+/-- info: true -/
+#guard_msgs in
+#eval
+  show Bool from
+    let sharedCitation := "Lemma 2.1(1)"
+    let paperSource : Informal.Source.Ref := {
+      document := "paper"
+      spans := #[{ page := "12", citation := sharedCitation }]
+    }
+    let notesSource : Informal.Source.Ref := {
+      document := "notes"
+      spans := #[{ anchor := "itm:addition-right-identity", citation := sharedCitation }]
+    }
+    let uncitedSource : Informal.Source.Ref := {
+      document := "paper"
+      spans := #[{ page := "12" }]
+    }
+    let ambiguousSource : Informal.Source.Ref := {
+      document := "paper"
+      spans := #[
+        { page := "12", citation := sharedCitation },
+        { page := "13", citation := "Lemma 2.1(2)" }
+      ]
+    }
+    let singleHtml? :=
+      (Informal.renderSourceHeaderExtra? #[paperSource]).map (·.html.asString)
+    let multipleHtml? :=
+      (Informal.renderSourceHeaderExtra? #[paperSource, notesSource]).map (·.html.asString)
+    let uncitedHtml? :=
+      (Informal.renderSourceHeaderExtra? #[uncitedSource]).map (·.html.asString)
+    let ambiguousHtml? :=
+      (Informal.renderSourceHeaderExtra? #[ambiguousSource]).map (·.html.asString)
+    singleHtml?.any (hasSubstr · s!"source: {sharedCitation}") &&
+      multipleHtml?.any (hasSubstr · "sources 2") &&
+      !multipleHtml?.any (hasSubstr · s!"source: {sharedCitation}") &&
+      uncitedHtml?.any (hasSubstr · "source 1") &&
+      !uncitedHtml?.any (hasSubstr · "source:") &&
+      ambiguousHtml?.any (hasSubstr · "source 1") &&
+      !ambiguousHtml?.any (hasSubstr · "source:")
 
 /-- info: true -/
 #guard_msgs in
@@ -265,17 +337,21 @@ Invalid source metadata.
     let (html, st) ← renderManualDocHtmlStringAndState extension_impls% sourceProvenanceDoc
     let sourceDocument? := Informal.TraversalIndex.SourceDocuments.data? st "paper"
     let sourceRef? := Informal.TraversalIndex.SourceRefs.data? st sourcedLabel
+    let secondSourceRef? := Informal.TraversalIndex.SourceRefs.data? st secondSourcedLabel
     let storageOk :=
-      match sourceDocument?, sourceRef? with
-      | some sourceDocument, some sourceRef =>
+      match sourceDocument?, sourceRef?, secondSourceRef? with
+      | some sourceDocument, some sourceRef, some secondSourceRef =>
           sourceDocument.id == "paper" &&
             sourceDocument.title == "Representation Theory" &&
             sourceDocument.kind == .pdf &&
             sourceDocument.pdf == some "source/paper.pdf" &&
             sourceDocument.pageRoot == some "source/pages" &&
             sourceDocument.imageRoot == some "source/pages/images" &&
-            sourceRefHasRepresentationTheorySpan sourceRef
-      | _, _ => false
+            sourceRefHasRepresentationTheorySpan sourceRef &&
+            sourceRefHasAnchor "notes" "itm:addition-right-identity" secondSourceRef &&
+            secondSourceRef.spans.any (fun span =>
+              span.page.isNone && span.citation == some "Lemma 2.1(1)")
+      | _, _, _ => false
     pure <|
       hasSubstr html "A sourced statement." &&
       !hasSubstr html "source/paper.pdf" &&
@@ -312,9 +388,9 @@ Invalid source metadata.
         entry.targetKind == .leanDecl &&
           entry.sources.size == 2 &&
           entryHasSourcePage "paper" "12" entry &&
-          entryHasSourcePage "notes" "A" entry) &&
+          entryHasSourceAnchor "notes" "itm:addition-right-identity" entry) &&
       entryOptionHasSourcePage "paper" "12" entry? &&
-      entryOptionHasSourcePage "notes" "A" secondEntry?
+      entryOptionHasSourceAnchor "notes" "itm:addition-right-identity" secondEntry?
 
 /-- info: true -/
 #guard_msgs in
diff --git a/tests/VersoBlueprintTests/Vbp.lean b/tests/VersoBlueprintTests/Vbp.lean
index e73d04a2..0d0aa8e0 100644
--- a/tests/VersoBlueprintTests/Vbp.lean
+++ b/tests/VersoBlueprintTests/Vbp.lean
@@ -1032,6 +1032,30 @@ private def writeRawManifestOnlySite (site : System.FilePath) (manifestJson : Js
         message.contains Informal.PreviewManifest.manifestInternalSchemaVersionField &&
         message.contains "lake exe vbp build"
 
+/-- info: true -/
+#guard_msgs in
+#eval do
+  let site ← freshVbpFixtureRoot
+  let staleManifestJson := Json.mkObj [
+    (Informal.PreviewManifest.manifestInternalSchemaVersionField,
+      toJson (Informal.PreviewManifest.manifestInternalSchemaVersion - 1)),
+    ("previews", Json.arr #[]),
+    ("groups", Json.arr #[]),
+    ("graphs", Json.arr #[]),
+    ("sourceDocuments", Json.arr #[])
+  ]
+  writeRawManifestOnlySite site staleManifestJson
+  try
+    let _ ← VersoBlueprint.Vbp.readManifestForSite site
+    pure false
+  catch err =>
+    let message := IO.Error.toString err
+    pure <|
+      message.contains "unsupported internal Blueprint manifest schema" &&
+        message.contains "found" &&
+        message.contains "expected" &&
+        message.contains "lake exe vbp build"
+
 /-- info: true -/
 #guard_msgs in
 #eval
diff --git a/tests/browser/test_preview_runtime_regressions.py b/tests/browser/test_preview_runtime_regressions.py
index 83d5694a..11f7e3ad 100644
--- a/tests/browser/test_preview_runtime_regressions.py
+++ b/tests/browser/test_preview_runtime_regressions.py
@@ -1500,6 +1500,7 @@ def test_generated_manifest_carries_source_metadata_for_external_markup(self, se
         )
         source_ref = entry["sources"][0]
         span = source_ref["spans"][0]
+        page_less_span = source_ref["spans"][1]
 
         assert source_document == {
             "id": "custom-client-paper",
@@ -1513,6 +1514,8 @@ def test_generated_manifest_carries_source_metadata_for_external_markup(self, se
         assert entry["label"] == "custom_client_external_markdown_metadata"
         assert source_ref["document"] == "custom-client-paper"
         assert span["page"] == "42"
+        assert span["anchor"] == "thm:custom-client"
+        assert span["citation"] == "Theorem 4.2"
         assert span["text"]["path"] == "source/pages/page-42.md"
         assert span["text"]["startLine"] == 10
         assert span["text"]["endLine"] == 12
@@ -1527,6 +1530,19 @@ def test_generated_manifest_carries_source_metadata_for_external_markup(self, se
             "yMax": 520,
             "yMin": 240,
         }
+        assert page_less_span == {
+            "anchor": "itm:custom-client",
+            "citation": "Theorem 4.2",
+            "page": None,
+            "pdf": None,
+            "text": {
+                "endCharacter": None,
+                "endLine": 82,
+                "path": "source/custom-client.tex",
+                "startCharacter": None,
+                "startLine": 80,
+            },
+        }
 
     def test_public_apis_resolve_source_documents_from_manifest(self, server: str, page: Page):
         errors = record_runtime_errors(page)
@@ -2168,7 +2184,7 @@ def test_source_header_chip_opens_source_preview(self, server: str, page: Page):
         ).first
         source_slot = statement.locator(".bp_extra_slot_source").first
         chip = source_slot.locator(".bp_source_ref_chip").first
-        expect(chip).to_have_text("source 1")
+        expect(chip).to_have_text("source: Theorem 4.2")
 
         uses_chip = statement.locator(".bp_extra_slot_uses .bp_relation_chip").first
         source_box = require_box(chip)
@@ -2190,8 +2206,12 @@ def test_source_header_chip_opens_source_preview(self, server: str, page: Page):
         body = preview.locator(".bp_source_ref_preview_body").first
         expect(body).to_contain_text("custom-client-paper")
         expect(body).to_contain_text("custom-client-paper p. 42")
+        expect(body).to_contain_text("citation Theorem 4.2")
+        expect(body).to_contain_text("anchor thm:custom-client")
         expect(body).to_contain_text("source/pages/page-42.md:10-12")
         expect(body).to_contain_text("source/pages/page-42.pdf")
+        expect(body).to_contain_text("anchor itm:custom-client")
+        expect(body).to_contain_text("source/custom-client.tex:80-82")
 
         assert_no_runtime_errors(errors)
 
diff --git a/tests/test_blueprints/preview_runtime_showcase/PreviewRuntimeShowcase/Chapters/CustomRenderClient.lean b/tests/test_blueprints/preview_runtime_showcase/PreviewRuntimeShowcase/Chapters/CustomRenderClient.lean
index e91c8caa..78defc04 100644
--- a/tests/test_blueprints/preview_runtime_showcase/PreviewRuntimeShowcase/Chapters/CustomRenderClient.lean
+++ b/tests/test_blueprints/preview_runtime_showcase/PreviewRuntimeShowcase/Chapters/CustomRenderClient.lean
@@ -498,6 +498,8 @@ source := {
   spans := #[
     {
       page := "42"
+      anchor := "thm:custom-client"
+      citation := "Theorem 4.2"
       text := some {
         path := "source/pages/page-42.md"
         startLine := 10
@@ -516,6 +518,15 @@ source := {
           yMax := 520
         }
       }
+    },
+    {
+      anchor := "itm:custom-client"
+      citation := "Theorem 4.2"
+      text := some {
+        path := "source/custom-client.tex"
+        startLine := 80
+        endLine := 82
+      }
     }
   ]
 }