Option-D reference-0 cleanup campaign: item-specific dead-declaration deletion (post-_bundle-exhaustion)

[phasetr]

Authorization

The user has explicitly authorized (2026-07-24) investigation and deletion of genuinely-dead reference-0 declarations:

時間と労力がかかっても構わない. 慎重に調べて余計なものは削除しろ

This campaign conducts item-specific dead-declaration deletion from the ~1,665-candidate reference-0 pool identified after the exhausted _bundle pattern sweep (#4665–#4690, main 9a7b2c3).

Context & related: see .self-local/reports/handoff-2026-07-24-campaign-exhausted.md and memory project_refactor_buildspeed_2026_07_20.md.

Scope

This issue does NOT authorize:

• New theorems (Generalize alternatingConnectedSubgraphSum(completeGraph n) and retire K0/K2/K3/K4 hardcoded base cases #4642 "Generalize alternatingConnectedSubgraphSum(completeGraph n)...")
• Module re-merges (Re-merge AmbientLattice/SpecialCases per-theorem module splits (pilot: 10 Magnetization* modules, measured 10.5x median fixed-cost reduction) #4563 "Re-merge AmbientLattice/SpecialCases per-theorem module splits...")

Those remain separately gated.

Folded-in work: #4559 items

Issue #4559 "Follow-up: detached subtree, zero-ref decl, unused import (out of #4557 dedup scope)" contains three pre-vetted items that now fall under this Option-D authorization and are incorporated as the first work batch:

1. Item 1: Delete IsingModel/ClusterExpansion/MayerCore/Truncations.lean and MayerTermThreeEval.lean (doc-sync-gated, conditionally).
2. Item 2: alternatingConnectedSubgraphSum_cycleGraph_seven (already resolved by refactor: drop six reference-0 declarations covered by the general cycle closed form #4636 cleanup).
3. Item 3: Remove unused import from IsingModel/ClusterExpansion/StrictPositivity/IffCharacterisations.lean:1 (pure hygiene, first-batch target).

#4559 will be closed once its 3 items are fully disposed via PRs.

Keep-Criteria (frozen, authoritative for this campaign)

A reference-0 declaration MUST BE KEPT (i.e., is NOT deletion-eligible) if it is ANY of:

• (a) an endpoint GJ-book result / final proposition (the deliverable itself; by nature has no internal consumer)
• (b) a Lee-Yang capstone
• (c) an infinite-volume deliverable
• (d) parked OZ infrastructure cited in docs/index.md (SL-A/SL-B/SL-C/D1a/D1b toward Thm 17.5.1 lsc, tracked under GJ Theorem 17.5.1 — true-mass (latticeMass) continuity on the high-temperature window #4386/📐 GJ §17.5 Thm 17.5.1 lsc half — random-current OZ two-point lower bound (thread) — subissue of #4386 #4418) — verified live location: docs/index.md line 1729 area, sum_prod_eq_sum_doubled_subFinset etc.
• (e) a ℤ^d latticeGraph Λ-layer / tanh / ferromagnetic / high-temp specialization that CLAUDE.local.md mandates as concrete-model deliverable API surface bundled into GJ-proposition PRs (per "1 GJ 命題 + helper + 合成 + 系 + tanh 変換 + Λ-layer wrap" bundling rule)
• (f) cited by docs/index.md or tex/proof-guide.tex (grep both before any deletion)
• (g) referenced by the GKSTest executable or any decide/property test

Only declarations that are reference-0 AND fail ALL of (a)–(g) AND do not transitively feed any kept result are deletion-eligible. When uncertain, KEEP — do not resolve ambiguity in favor of deletion. This mirrors the already-litigated false-positive lesson (10/22 in Profile.lean audit, #4639) and the two REFUTED tier-2 candidates from 2026-07-21 recorded in project_abstraction_candidates_2026_07_21.md.

Per-PR Verification Protocol

For each PR claiming reference-0 deletions, dev-issue-manager applies after closure:

1. Evidence-of-dead check: every deleted declaration must have a recorded rg -n scan showing zero consumers (both declaration-side and consumer-side, per the 2026-07-21 lesson), AND explicit confirmation it fails all keep-criteria (a)–(g) with citation of the grep/search used for each. Unicode-aware tokenization only (no naive ASCII word-boundary scanner — recurring bug noted 2026-07-21).

2. Build health: lake build reproduces zero warnings post-deletion (not just pre-deletion baseline).

3. Axiom/sorry hygiene: grep -rn "sorry" IsingModel/ = 0, grep -rn "^axiom" IsingModel/ = 0 (or repo-standard axiom-decl scan), and #print axioms on any touched/downstream theorem still yields exactly [propext, Classical.choice, Quot.sound].

4. Docs/tex staleness: rg docs/index.md and tex/proof-guide.tex for the deleted declaration names — zero stale references remain (any hit must be fixed in the same PR, not deferred).

5. Three-layer sync: canonical (docs/index.md, if it ever cites the item), local mirror .self-local/issues/<n>.md, and the GitHub issue body/checklist all reflect the actual deletion set (no ledger drift), following the pattern already used in .self-local/issues/4691.md.

Any single failure above → PR does not close its issue; issue-manager reports unresolved.

Status

• Umbrella issue created (this issue)
• Item B PR (import hygiene, Follow-up: detached subtree, zero-ref decl, unused import (out of #4557 dedup scope) #4559 item 3): merged (refactor(optionD-batch1): make IffCharacterisations' true dependency (TanhBounds) explicit; add explicit CycleSeven import to AnalyticityLambdaPolymer #4693)
• Item A PR (decl deletion, Follow-up: detached subtree, zero-ref decl, unused import (out of #4557 dedup scope) #4559 items 1–2): merged (refactor: remove unused explicit Mayer order-3 lemmas + retract §18.4 order-3 docs claim #4702 decl deletion + docs: retract §18.4 Mayer order-3 claims left stale by #4702 #4705 docs/tex
  retraction of the resulting stale references)

[phasetr]

Completion record (dev-pr-clerk)

This campaign is technically complete; only the user's explicit close approval is outstanding
(feedback_approval_required: close is a per-issue user approval item, not a default action).
Evidence:

• Item A (decl deletion, folded-in Follow-up: detached subtree, zero-ref decl, unused import (out of #4557 dedup scope) #4559 items 1–2): merged as PR refactor: remove unused explicit Mayer order-3 lemmas + retract §18.4 order-3 docs claim #4702 (deleted
  IsingModel/ClusterExpansion/MayerCore/Truncations.lean and MayerTermThreeEval.lean, 4
  reference-0 declarations) + PR docs: retract §18.4 Mayer order-3 claims left stale by #4702 #4705 (docs/tex retraction of the resulting stale references at
  docs/index.md:2128 and tex/proof-guide.tex). git grep for mayerExpansionTerm_three /
  mayerPartialSum_three / MayerTermThreeEval / MayerCore/Truncations over docs/ + tex/ on
  main a3046ce6 → 0 hits.
• Item B (import hygiene, folded-in Follow-up: detached subtree, zero-ref decl, unused import (out of #4557 dedup scope) #4559 item 3): merged as PR refactor(optionD-batch1): make IffCharacterisations' true dependency (TanhBounds) explicit; add explicit CycleSeven import to AnalyticityLambdaPolymer #4693 — IffCharacterisations.lean
  now imports its true direct dependency TanhBounds instead of the transitive CycleSeven edge.
• All folded-in Follow-up: detached subtree, zero-ref decl, unused import (out of #4557 dedup scope) #4559 items disposed; the wider Option-D reference-0 pool is exhausted under the
  frozen keep-criteria (a)–(g) per .self-local/reports/handoff-2026-07-24-campaign-exhausted.md.

No further technical work is outstanding on this issue.