refactor dedup: mayerExpansionTerm_eq_zero_of_no_polymers

[phasetr]

Duplicate theorem dedup: mayerExpansionTerm_eq_zero_of_no_polymers

Background

Following refactor campaign cycles 1-7 (PR #4536–#4554, cycles completed 2026-07-17, main=7447d9e1),
umbrella-detached module wiring (cycle 7, #4553) exposed a genuine duplicate declaration during build:
mayerExpansionTerm_eq_zero_of_no_polymers exists in two locations.

Duplicate locations

• MayerCore (weaker, n≥1): IsingModel/ClusterExpansion/MayerCore/Truncations.lean:84
• CycleSeven (general, supersedes): IsingModel/ClusterExpansion/StrictPositivity/CycleSeven.lean:47

The CycleSeven version is reachable and general; the MayerCore version is detached and restricted.

User decision (2026-07-17)

Delete one twin, wire survivor into umbrella. Survivor selection (which theorem to keep) is TBD pending dev-design independent judgment.

Acceptance criteria

• Lake build: zero warnings
• audit_gate.py V1–V3: all PASS
• #print axioms: [propext, Classical.choice, Quot.sound] only (axiom-free)
• No sorry / admit / native_decide
• Survivor theorem referenced from single location (no duplicate paths)

Authorization basis

Gate (a) explicit user instruction (refactor campaign cycle 8, 2026-07-17).
See handoff: .self-local/reports/handoff-session-refactor-2026-07-17.md § "Open user-decision items" item 1.

[phasetr]

Closed by PR #4558 (squash-merge commit f61cd03).

Duplicate declaration mayerExpansionTerm_eq_zero_of_no_polymers removed from IsingModel/ClusterExpansion/MayerCore/Truncations.lean:84 (kept in reachable ClusterExpansion/StrictPositivity/CycleSeven.lean:47).

Note: umbrella wiring was transitively satisfied before this PR. The dedup cycle (issue #4553, cycle 7) had identified this duplicate for user decision (#4559); PR #4558 executes the removal decision, but no new umbrella wiring diff was introduced (dev-issue-manager verified). The Truncations.lean module was already unreachable before this PR; this PR merely removes the duplicate declaration from it.