diff --git a/AGENTS.md b/AGENTS.md
index 739ff11759..f80a463b6a 100644
--- a/AGENTS.md
+++ b/AGENTS.md
@@ -396,8 +396,11 @@ and [API review with explicit nonblocking nits](https://github.com/leanprover/cs
 
 When a declaration claims to formalize a cited result, the PR quotes the source statement with its
 exact locator and maps the source's notation to the Lean statement: quantifiers, models, encodings
-and resource conventions. Reviewers check that mapping rather than an impression. New mathematics
-and new proof ideas need no source; label them as original.
+and resource conventions. Reviewers check that mapping rather than an impression. Text presented as
+a quotation is copied from the pinned source version, with its locator checked there rather than
+taken from an issue, a PR or other library text; anything else is labeled as a paraphrase. Reviewers
+check quotations against the source, and a quoted passage that is not in the source blocks approval.
+New mathematics and new proof ideas need no source; label them as original.
 
 Whether a new definition needs checked examples on both sides (an instance where it holds and one
 where it fails) is for the author and reviewers to judge; reviewers may ask for them when a