ci(scripts): advisory check that names in a PR description exist at the head #1086

Several PR descriptions reviewed on 2026-10-25 named declarations that do not exist at the PR head (#1042: three; #1080: nine, e.g. nonceSignOracle, IsDiffUniversal, secureNonceMAC_of_isPRF; #1062 and #1068 had similar slips). The description is the durable source mapping, so each slip costs a review round, and reviewers find them by hand.

Proposal. An advisory script scripts/check_pr_names.py that extracts backticked Lean-identifier-like tokens from a PR description (or any Markdown file) and reports those that are not declared at the checked-out revision: in Complexity/, ComplexityTests/, abstracts/, the pinned cslib and Mathlib sources under .lake/packages, and core/Std where cheap. It should be conservative (skip tokens that are clearly not names: expressions with spaces/operators, file paths, numbers, Lean keywords; resolve dotted names by suffix and through namespace blocks well enough to avoid noise), print a short list of unresolved names, and exit 0 by default (--strict to fail). Wire it into CI as a non-blocking notice on pull_request events (the body is in the event payload), similar to parallel_defs.py's advisory notice (#1057), and mention it in CONTRIBUTING's PR checklist so authors run scripts/check_pr_names.py --pr N before requesting review. Tests in scripts/test_check_pr_names.py.

Done when: script + tests + advisory CI step + one-line CONTRIBUTING mention, with a run against #1080's body at c69067ba showing it catches the nonexistent names and few false positives on two or three recently merged PR bodies.

Tooling only; no Lean changes. — coordinator-jetski-0df14a81