Drop five reference-0 Lee-Yang subdomain/domain declarations found via #4648 cascade

[phasetr]

Motivation

PR #4648 (drop three duplicated Lee-Yang subdomain declarations) reported one cascade: deleting
one_mem_leeYangSubdomain' exposed the canonical one_mem_leeYangSubdomain (Locus.lean:385) as
reference-0 (its only consumer in the repository was the duplicate that PR #4648 removed).
Re-scanning the surrounding module for siblings found four more reference-0 declarations that
predate #4648:

• one_mem_leeYangSubdomain (IsingModel/ComplexAnalyticity/Locus.lean:385)
• one_mem_leeYangDomain (IsingModel/ComplexAnalyticity/Locus.lean:390)
• leeYangSubdomain_eq_inter_preimage (IsingModel/ComplexAnalyticity/Locus.lean:377)
• leeYangSubdomain_one_eq (IsingModel/ComplexAnalyticity/Locus.lean:395)
• Ioi_subset_leeYangDomain_real_preimage (IsingModel/ComplexAnalyticity/RealAxis.lean:79)

scripts/dead_candidate_scan.py classifies all five as safe-to-delete: zero published-result,
zero load-bearing, zero uncertain. rg over docs/, tex/proof-guide.tex, README.md confirms
none of the five names is cited anywhere; the docs/index.md Lee-Yang subdomain row (line ~534)
lists only leeYangSubdomain + abs_spinSum_le + exp_neg_beta_hamiltonian_re_pos +
partitionFunctionComplex_re_pos_of_leeYangSubdomain + _mem_slitPlane_of_leeYangSubdomain +
freeEnergyComplex_analyticAt_h_of_leeYangSubdomain as the published result set for this
subdomain — none of the five candidates above is among them. one_mem_leeYangSubdomain's doc
comment ("Convenient for downstream arguments needing a basepoint") is the decorative
"would-be-convenient" style lean-coding-conventions flags for removal, not a cited result.

Scope

Decoration removal within the existing Lee-Yang subdomain module (IsingModel/ComplexAnalyticity/)
under the same standing authorization as #4599/#4601/#4638/#4641/#4648 (reference-0 cleanup of
GJ-adjacent scaffolding, not a new refactor initiative). This is a continuation of an
already-authorized pattern, not new scope.

Proposal

• Run scripts/dead_candidate_scan.py (textual + --lean cross-check) against these five names
  immediately before deletion (re-verify at current HEAD; do not rely on this issue's scan alone).
• Delete only names that re-verify as safe-to-delete with no cascade onto a load-bearing sibling.
• Follow the Fix dead-sweep candidate extraction to require internal-dependency + docs/tex citation checks (10/22 false positives found in Profile.lean audit) #4639 adoption rule: paste full scanner output (incl. LIMITS: banner) in the PR body.

Acceptance criteria

• Scanner re-verifies all five (or the surviving subset) as safe-to-delete at PR HEAD
• --lean cross-check pasted
• No citation in docs/index.md / tex/proof-guide.tex / README.md for any deleted name
• lake build warning-free
• scripts/audit_gate.py --full V1-V4 pass
• lake exe GKSTest pass
• CI green
• Reference-0 fallout re-checked (no new cascade left unreported)

Related

• PR refactor: drop three duplicated Lee-Yang subdomain declarations #4648 / issue Tracking: drop Lee-Yang subdomain duplicate declarations (#4648) #4649 (source of this finding, first operational use of Fix dead-sweep candidate extraction to require internal-dependency + docs/tex citation checks (10/22 false positives found in Profile.lean audit) #4639 adoption rule)
• Issue Fix dead-sweep candidate extraction to require internal-dependency + docs/tex citation checks (10/22 false positives found in Profile.lean audit) #4639 (adoption rule for scanner-verified deletions)

[phasetr]

PR Created

PR #4651 has been created for this refactor task.

• Branch: refactor/drop-lee-yang-convenience-lemmas
• Status: Draft PR (early creation, implementation phase pending)
• Target: Five unreferenced Lee-Yang convenience lemmas
• Scope: No impact on public Lee-Yang theorem or public results documented in docs/index.md

Verification checklist (to be completed during implementation):

• Dead candidate scan with full LIMITS: banner
• --lean cross-check run
• lake build warning-free
• scripts/audit_gate.py V1-V4 pass
• lake exe GKSTest pass
• CI green

Next: implementation and verification phases.