diff --git a/6-Documentation/docs/GLOSSARY.md b/6-Documentation/docs/GLOSSARY.md
index f456a353..add3bb53 100644
--- a/6-Documentation/docs/GLOSSARY.md
+++ b/6-Documentation/docs/GLOSSARY.md
@@ -109,6 +109,10 @@ surface.
 | **VM** | Virtual machine. | AVM / substrate state |
 | **XNA** | Xenonucleic acid. | Biology references |
 | **ZK** | Zero knowledge. | STARK / Warden validation |
+| **CM** | Concept Map — JSONL artifact mapping files to extracted concepts. | `shared-data/data/concept_map/` |
+| **JM** | Jaccard Matcher — arxiv paper discovery via keyword overlap. | `extraction/jaccard_matcher.py` |
+| **PTC** | PIST Trace Classifier — Lean-first proof trace spectral classifier. | `PistClassifyTrace.lean` |
+| **SS** | SilverSight — standalone Lean repo for schema/layout/wireformat/codec. | `/tmp/SilverSight` |
 
 ## Core Formalism
 
@@ -237,6 +241,43 @@ surface.
 | **Sigma** | Statistical surprise measure (5σ / 6σ / 6.5σ). Applies ONLY to statistical claims, not formal proofs. |
 | **FNWH** | Formal Non-Wave Harmonic — the underlying harmonic framework for Burgers/Braiding proofs. |
 
+## Concept Mapping & Citations
+
+| Term | Definition |
+|---|---|
+| **Concept Map** | JSONL artifact (`shared-data/data/concept_map/markdown_concept_map.jsonl`) mapping 822 local files to 3,152 extracted concepts with types, tags, dependencies, and summaries. Parallel extraction from 7 agents covering root docs, specs, wiki modules, infra, and artifacts. |
+| **Drive Concept Map** | JSONL artifact (`shared-data/data/concept_map/drive_concept_map.jsonl`) classifying 752 Google Drive files by relevance to Research Stack. 19 directly related, 13 Google Docs (FAMM, RRC, ENE). |
+| **Cornfield Concepts** | 48 formally grounded concepts in `extraction/cornfield_concepts.json`. Each carries academic citations (DOI/arxiv), novelty classification, and novelty_statement. 19 novel claims, 29 grounded in prior work. |
+| **concept_citations** | Postgres table on neon-64gb linking `math_objects.id` to papers via `paper_id`, `doi`, `title`, `authors`, `year`, `journal`, `arxiv_category`, `relation_type` (grounds/extends/applies/cites). 118 records. |
+| **paper_refs** | JSONB column on `math_objects` storing structured citation array. Each entry: `{paper_id, doi, title, authors, year, journal, arxiv_category, relation_type, notes}`. |
+| **is_novel_claim** | Boolean column on `math_objects`. True = original work with no prior paper covering exactly this. Requires `novelty_statement` explaining the precise delta. |
+| **novelty_statement** | Text column on `math_objects`. One-sentence description of what is new vs. cited prior art. Hostile reviewer must be able to verify the delta independently. |
+| **Jaccard Matcher** | Script (`jaccard_matcher.py`) that finds arxiv papers for cornfield concepts via keyword overlap against 700k arxiv_papers. Computes coverage = |matched_keywords| / |concept_keywords|. |
+| **relation_type** | Citation edge type in `concept_citations`: `grounds` (foundational paper), `extends` (builds on), `applies` (application), `cites` (general reference). |
+
+## SilverSight
+
+| Term | Definition |
+|---|---|
+| **SilverSight** | Standalone Lean repo at `/tmp/SilverSight` for schema/layout/wireformat/codec work. Separated from Research Stack to isolate the Core Semantics surface. 8-phase microstep pipeline designed in `6-Documentation/docs/plans/SilverSight_completion_pipeline.md`. |
+| **Product Schema** | Schema instance for `α × β` with `byteSize = byteSize α + byteSize β` and `wellFormed = wellFormed a && wellFormed b`. Phase 1.1 of SilverSight pipeline. |
+| **Product Wire Format** | Row-major encode/decode for pairs: `encode (a,b) = encode a ++ encode b`. Roundtrip theorem proven. Phase 1.2. |
+| **Product Layout Bridge** | Identity and rowMajor↔columnar bridges for product types. Phase 1.3. |
+| **Product View** | Zero-copy `View.fst` / `View.snd` for pair fields without copying. Phase 1.4. |
+| **ReceiptHeader** | Fixed-size 48-byte header for Receipt serialization: `receiptIDHash`, `expressionHash`, `finalState`, `ticCount`, `fuelUsed`, `pathCostRaw`, `verified`, `libraryRefCount`, `libraryRefsHash`. Phase 1.9. |
+| **Gate** | Proof-carrying partial function: `run : α → Option β`, `inv : α → β → Bool`, `preserves : ∀ a b, run a = some b → inv a b = true`. Lawful bind with associativity and identity theorems. Phase 1.10. |
+| **Claim-State Ladder** | `BEAUTIFUL_PROVISIONAL → CALIBRATED_ENGINEERING_DELTA → REVIEWED → VERIFIED`. No claim may skip a state. Promotion recorded in `docs/claims/manifest_v1.json`. |
+
+## PIST Trace Classifier
+
+| Term | Definition |
+|---|---|
+| **PistClassifyTrace** | Lean executable (`PistClassifyTrace.lean`) that reads trace JSON, computes spectral features with Q16_16 arithmetic, applies RRC shape thresholds, and infers tactic family. Sole classifier authority — Python shims may only format I/O. |
+| **Spectral Profile** | 10-feature vector from transition matrix: `matrix_size`, `rank`, `spectral_gap`, `density`, `trace_val`, `frobenius_norm`, `laplacian_zero_count`, `adjacency_eigenvalue_max`, `laplacian_eigenvalue_max`, `singular_value_max`. All Q16_16. |
+| **RRC Shape Thresholds** | Color-space mapping: λ ≥ 4.0 → `CognitiveLoadField` (red/Oberth), 2.0 ≤ λ < 4.0 → `SignalShapedRouteCompiler` (green/signal), λ < 2.0 → `HoldForUnlawfulOrUnderspecifiedShape` (blue/hold). Calibrated for 8×8 braid crossing matrices. |
+| **Tactic Family** | Classification of proof step names: rewrite, normalization, arithmetic, induction, algebraic, case_analysis, discharge, reflexivity, unknown. |
+| **rrc-watchdog** | Lean binary in podman container that verifies alignment between predicted and expected RRC shapes. Returns `alignmentStatus`, `score`, `warnings`. |
+
 ## Infrastructure
 
 | Term | Definition |