Fix dead-sweep candidate extraction to require internal-dependency + docs/tex citation checks (10/22 false positives found in Profile.lean audit)

[phasetr]

Motivation

During the PseudoMass/Profile.lean reference-0 audit for #4637's PR-3, dev-design found that
the original 22-declaration candidate list (extracted by Lean-importer count alone, i.e. "0
importers") was overcounted: 10/22 were false positives — 7 are live via internal dependency
closure (used within the same file/namespace, just not imported from elsewhere), 3 are cited by
docs/index.md as GJ §17.5 results (docs/tex citation, not a Lean import). True reference-0 count
was 12/22.

Proposal

Change the standing operating procedure for "dead sweep" candidate extraction (used by
dev-refactoring / lean-refactoring dead-code passes) from import-count-only to a two-part
condition:

1. Internal dependency closure: a declaration counts as "referenced" if any other declaration
   in the repository (including in the same file/namespace) depends on it, not just cross-file
   importers.
2. docs/tex name citation: a declaration counts as "referenced" if its name is cited in
   docs/index.md or tex/proof-guide.tex (i.e. it is presented as a book-progress result),
   even if nothing in IsingModel/ imports it.

Only declarations satisfying neither condition should be proposed as reference-0 deletion
candidates.

Scope

This is a general operating-procedure correction for future dead-code / reference-0 sweeps
project-wide, not specific to the alternatingConnectedSubgraphSum cleanup tracked in #4637 (kept
separate so #4637 can close on its own scope without pulling in unrelated process changes).

Acceptance

• lean-refactoring (or equivalent dead-sweep tooling/checklist) updated to require both checks
  before flagging a declaration as a deletion candidate.
• Re-verify this against the next dead-sweep candidate list before batch deletion.

Related: #4637 (PR-3 Profile.lean scope reduction, 22 → 12, exhibits the false-positive rate this
issue fixes)

[phasetr]

PR #4647 has been created for this tracking issue.

[phasetr]

dev-issue-manager: adoption rule + close decision (PR #4647 HEAD af83b0b0)

Resolution verification of PR #4647: resolved, all checklist claims reproduced at current
HEAD (79/79 self-test, 18/18 fixture, both canaries PASS, --pattern '_ferromagnetic$'
263→35/52/44/132 with 0 coverage warnings, audit_gate --full PASS, lake build clean,
tex/proof-guide.tex builds to 550 pages, CI green). Full evidence:
#4647 (comment)

This issue's acceptance criterion #1 ("lean-refactoring (or equivalent dead-sweep
tooling/checklist) updated to require both checks before flagging a declaration as a deletion
candidate") is not yet met by PR #4647 alone: the PR delivers the scanner but wires it into no
required gate — running it remains opt-in. Building the tool without an enforced adoption path
was the exact failure mode this issue's own governance note warned about ("without a durable rule
the tool risks going unused").

Adoption rule (durable, effective immediately)

Any Lean PR in this repository that deletes one or more declarations from IsingModel/ must
include, in its PR body, the full output of
python3 scripts/dead_candidate_scan.py <names-or-pattern covering the exact deletion set>,
including the LIMITS: banner at the end. A deletion PR whose candidate set contains any
declaration the scanner marks load-bearing, published-result, or uncertain (rather than
safe-to-delete) is not mergeable on that basis without an explicit, written justification for
each such name in the PR body.

Enforcement, until this rule is migrated into a skill/checklist: dev-issue-manager checks
for this scanner-output paste as part of its mandatory resolution-verification pass on every
deletion PR (per CLAUDE.local.md's fleet mandate that dev-issue-manager runs on every merge).
A deletion PR without the paste is an unresolved finding in that audit.

This issue is kept OPEN to serve as the normative home of this rule (linked from future
deletion PR bodies) until the rule is migrated to a more durable location (dev-pr-workflow skill
or a repo-tracked doc) — that migration is out of scope for this agent to execute directly
(skill edits go through the user's skill-curation workflow) and is recommended as a follow-up.

Not closing #4639 yet: acceptance criterion #1 (require, not just provide) is satisfied by
this comment's enforcement clause, contingent on dev-issue-manager actually applying it on the
next deletion PR. Recommend re-evaluating close at that point, or closing now if the user
considers "tool exists + enforcement rule recorded + issue-manager commits to checking it" a
sufficient discharge of the acceptance criterion (a defensible reading, since the criterion never
named a specific file to encode the rule in).

[phasetr]

PR #4647 merged with squash commit b6260cb. The reference scanner script scripts/dead_candidate_scan.py is now available for use in future deletion PRs to verify that deletion candidates are safe.

[phasetr]

dev-issue-manager: 2nd operational use of the adoption rule (PR #4651) + rule clarification + keep-list exception

PR #4651 (drop 5 reference-0 Lee-Yang convenience lemmas, resolving #4650) is the rule's second
use. Verdict: substantively compliant (3 scanner runs with LIMITS: banner present, all 5
candidates genuinely safe-to-delete, cascade 0), but the PR body's "documentation family
labels" block was hand-replaced with a placeholder ((block elided: 849 family-label rows...))
rather than pasted verbatim. The tool never prints 849 rows — it caps that section at 20 named
rows + ... and N more (scripts/dead_candidate_scan.py:2072-2075), so the true output is
already short enough to paste as-is; no elision was needed, and the placeholder mis-describes
"849" as a count of omitted lines rather than the header's declared total. Full finding:
#4651 (comment)

Rule clarification (recommended addition to the #4639 adoption rule): "paste full scanner
output" means the tool's own stdout verbatim, including whatever self-truncation the tool itself
already performs (e.g. the family-labels cap). PR authors must not additionally hand-summarize or
elide any section of that stdout under the guise of brevity.

Keep-list exception (recorded here as the durable home of dead-sweep adoption exceptions):
real_pos_axis_subset_leeYangDomain (IsingModel/ComplexAnalyticity/RealAxis.lean:78),
range_real_axis_subset_leeYangDomain (RealAxis.lean:255), and
real_axis_pos_subset_leeYangDomain (RealAxis.lean:35) are currently reference-0 by the same
textual criterion PR #4651 used, but should not be proposed for deletion in a future dead
sweep: each is a distinct surviving phrasing (subtype-range / packaged-subtype-range /
set-builder) of the same "positive real axis ⊆ leeYangDomain" fact that
Ioi_subset_leeYangDomain_real_preimage (deleted in #4651) also expressed as a preimage. These
three are the complete surviving phrasing set for that fact; further deletion here would reduce
phrasing coverage rather than remove true duplication.

[phasetr]

Session 2026-07-22: Two findings on audit governance

1. Execution machinery proved effective. The standing operating procedure (this issue Fix dead-sweep candidate extraction to require internal-dependency + docs/tex citation checks (10/22 false positives found in Profile.lean audit) #4639) and the three-pass dead-sweep candidate scan (with verification gate) actually prevented silent correctness regressions. Evidence: refactor: drop three duplicated Lee-Yang subdomain declarations #4648 adopted the ruling for the first time (drop 3 Lee-Yang subdomain declarations via the new checklist), and refactor: drop five unreferenced Lee-Yang convenience lemmas #4651 showed issue-manager blocking a PR merge due to a body-text discrepancy (claimed '849 lines omitted' but the omission summary was actually omitted). The machinery works — it is not a dead rule.

2. Manual tier2 re-count buckets are unreliable. The original tier2 abstract-pattern report (before scanners existed) estimated '113 out of 30 at reference-0' for the _bundle pattern group. Re-scanning with the same double-pass logic (internal + docs/tex citation closure) shows the corrected split: 141 declarations examined, 80 safe-to-delete, 27 load-bearing, 19 uncertain, 15 published-result. This is the same undercounting failure as the Top-2 case (_ferromagnetic) that forced a partial tier2 retraction earlier. Automated scanners + reported measurements are mandatory; hand-tallied numbers are a trap. The scanner has now arrived, so .self-local/reports/tier2-abstraction-candidates-2026-07-21.md will be updated to flag which buckets were hand-tallied (pre-scanner) and thus need re-verification before adoption.