diff --git a/CITATION.cff b/CITATION.cff
index f8ea1cef..377a61b8 100644
--- a/CITATION.cff
+++ b/CITATION.cff
@@ -57,10 +57,10 @@ references:
     url: "https://github.com/allaunthefox/Research-Stack"
     date-released: 2026-05-08
     license: Apache-2.0
-    notes: "Parent research repository from which SilverSight ports proven Lean modules, agent contracts, and fixed-point semantics."
+    notes: "Parent research repository (https://github.com/allaunthefox/Research-Stack). SilverSight ports proven Lean modules (`Semantics.FixedPoint`, `Semantics.SidonSets`, `Semantics.BraidEigensolid`, etc.), agent contracts, and the no-Float compute doctrine from this source."
 
-  # NOTE: The following four references are domain sources used by the
-  # PVGS_DQ_Bridge and BindingSite libraries. They are recorded as
+  # NOTE: The following four references are domain sources used by
+  # `formal/PVGS_DQ_Bridge/` and `formal/BindingSite/`. They are recorded as
   # `unpublished` until DOIs, arXiv IDs, or journal pages are confirmed.
   - type: unpublished
     authors:
@@ -72,7 +72,7 @@ references:
         given-names: "C."
     title: "Photon-Varied Gaussian States"
     year: 2025
-    notes: "Preprint / in-preparation. Identifier pending confirmation."
+    notes: "Binds to Research Stack `Semantics.PVGS_DQ_Bridge` → SilverSight `formal/PVGS_DQ_Bridge/`; preprint identifier pending confirmation."
   - type: unpublished
     authors:
       - family-names: "Chabaud"
@@ -81,7 +81,7 @@ references:
         given-names: "S."
     title: "Stellar representation of non-Gaussian quantum states"
     year: 2022
-    notes: "Full citation details pending DOI or arXiv ID."
+    notes: "Binds to Research Stack `Semantics.PVGS_DQ_Bridge` → SilverSight `formal/PVGS_DQ_Bridge/`; full citation details pending DOI or arXiv ID."
   - type: unpublished
     authors:
       - family-names: "Pizzimenti"
@@ -89,7 +89,7 @@ references:
       - family-names: "et al."
     title: "Wigner negativity of superpositions"
     year: 2024
-    notes: "Full citation details pending DOI or arXiv ID."
+    notes: "Binds to Research Stack `Semantics.BindingSite` / `Semantics.PVGS_DQ_Bridge` → SilverSight `formal/BindingSite/`; full citation details pending DOI or arXiv ID."
   - type: unpublished
     authors:
       - family-names: "Wassner"
@@ -97,7 +97,7 @@ references:
       - family-names: "et al."
     title: "Single quadrature noise tomography"
     year: 2025
-    notes: "Full citation details pending DOI or arXiv ID."
+    notes: "Binds to Research Stack `Semantics.PVGS_DQ_Bridge` → SilverSight `formal/PVGS_DQ_Bridge/`; full citation details pending DOI or arXiv ID."
 
   # ── Conceptual bindings ported from Research Stack ─────────────────────────
 
@@ -111,7 +111,7 @@ references:
       name: "California State University, San Bernardino"
     collection-title: "Electronic Theses, Projects, and Dissertations"
     url: "https://scholarworks.lib.csusb.edu/etd/855"
-    notes: "Combinatorics reference for Pascal-triangle extensions and Fermat-number patterns; binds to SilverSight Sidon-set and number-theory modules (e.g., SidonSets, SpherionTwinPrime)."
+    notes: "Binds to Research Stack `Semantics.SidonSets` → SilverSight `formal/CoreFormalism/SidonSets.lean`; supports Sidon-set constructions, Singer-theorem residues, and number-theory fixtures."
 
   - type: article
     title: "Close packing density of polydisperse hard spheres"
@@ -123,7 +123,7 @@ references:
     date-published: 2009-12
     doi: 10.1063/1.3276799
     journal: "The Journal of Chemical Physics"
-    notes: "Anchor paper for polydisperse close-packing theory; binds to braid-eigensolid and meta-solid phase models (BraidEigensolid, BraidSpherionBridge, BaselineComparison)."
+    notes: "Binds to Research Stack `Semantics.BraidEigensolid` / `Semantics.BraidSpherionBridge` / `Semantics.BaselineComparison` → SilverSight `formal/BraidEigensolid.lean` / `formal/BraidSpherionBridge.lean`; anchor paper for polydisperse close-packing theory used in eigensolid convergence proofs."
 
   - type: article
     title: "Fractionation effects in phase equilibria of polydisperse hard-sphere colloids"
@@ -135,7 +135,7 @@ references:
     date-published: 2004-10
     doi: 10.1103/physreve.70.041410
     journal: "Physical Review E"
-    notes: "Full fractionation phase equilibria for polydisperse hard spheres; terminal polydispersity ~14% binds to the meta-solid 1/7 mixing threshold."
+    notes: "Binds to Research Stack `Semantics.BraidEigensolid` / `Semantics.MetaSolid` → SilverSight `formal/BraidEigensolid.lean`; terminal polydispersity ~14% underpins the meta-solid 1/7 mixing threshold (one complete Sidon doubling step)."
 
   - type: article
     title: "Random-close packing limits for monodisperse and polydisperse hard spheres"
@@ -147,7 +147,7 @@ references:
     date-published: 2014
     doi: 10.1039/c3sm52959b
     journal: "Soft Matter"
-    notes: "Definitive RCP limits for monodisperse (~0.64) and polydisperse spheres; conceptual reference for eigensolid packing bounds."
+    notes: "Binds to Research Stack `Semantics.BraidEigensolid` → SilverSight `formal/BraidEigensolid.lean`; definitive random-close-packing limits for monodisperse (~0.64) and polydisperse spheres used in eigensolid packing-bound claims."
 
   - type: article
     title: "Freezing of polydisperse hard spheres"
@@ -159,7 +159,7 @@ references:
     date-published: 1999
     doi: 10.1103/physreve.59.618
     journal: "Physical Review E"
-    notes: "Fractionating phase behavior of polydisperse hard spheres; supports braid/meta-solid phase-transition fixtures."
+    notes: "Binds to Research Stack `Semantics.BraidEigensolid` / `Semantics.BaselineComparison` → SilverSight `formal/BraidEigensolid.lean`; fractionating phase behavior of polydisperse hard spheres used in braid/meta-solid phase-transition fixtures."
 
   - type: article
     title: "A Differentiable Interior-Point Method in Single Precision"
@@ -172,7 +172,7 @@ references:
         given-names: "Zachary"
     date-published: 2026-05
     url: "https://arxiv.org/abs/2605.17913"
-    notes: "Differentiable primal-dual IPM with bounded KKT systems for low-precision / fixed-point arithmetic; binds to SilverSight Q16_16 fixed-point computation (FixedPoint, Q16InverseProof)."
+    notes: "Binds to Research Stack `Semantics.FixedPoint` / `Semantics.Q16InverseProof` → SilverSight `formal/CoreFormalism/FixedPoint.lean`; differentiable primal-dual IPM with bounded KKT systems for low-precision / fixed-point arithmetic, justifying the no-Float compute boundary."
 
   - type: article
     title: "Stabilizing Recurrent Dynamics for Test-Time Scalable Latent Reasoning in Looped Language Models"
@@ -193,4 +193,4 @@ references:
         given-names: "Yu-Feng"
     date-published: 2026-05
     url: "https://arxiv.org/abs/2605.26733"
-    notes: "STARS regularizes spectral radius of the Jacobian using power iterations with JVPs; conceptual reference for recurrent / looped dynamics in search and classification loops."
+    notes: "Binds to Research Stack `Semantics.AVMIsa.*` / `Semantics.Run` → SilverSight `Core/SilverSightCore.lean` AVM transition function; STARS regularizes spectral radius of the Jacobian using power iterations with JVPs, relevant to recurrent / looped AVM search dynamics."