refactor: mathlib-only umbrella import downgrades from shake (2026-07-17 cycle 4)

[phasetr]

Scope

Apply mathlib-only umbrella import downgrades suggested by shake output. A downgrade is included if and only if:

• All removed imports are Mathlib.* modules
• All added imports are Mathlib.* modules
• Change is self-contained within a single file

Each file's downgrade is mechanically independent and can be reverted if shake produces a false positive.

Exclusions (BAN LIST)

Do not include:

• Any edit touching an IsingModel.* import line (umbrella-preservation rule)
• Downstream-coupled chains unless they are mathlib-only
• Any downgrades related to issues [refactor measurement] Profile current-main Lean bottlenecks before selecting one candidate #4533, chore(benchmark): archive #4519 static evidence revisions 18–22 #4520, H2-local-hook, or other repo-flagged problematic sites

Acceptance Gates

All the following must pass locally and in CI before merge:

1. lake build IsingModel completes with zero warnings
2. lake exe GKSTest passes all tests
3. audit_gate.py --full exits with code 0
4. Umbrella-preservation grep check: git diff <base>..HEAD | grep -E '^[+-].*IsingModel' | wc -l equals 0
5. Per-file revert rule: for any file where shake suggested a false positive, revert that file's changes only (do not revert the entire PR)

Related Context

• Issue-manager adjudication: Third /goal re-issuance (this session) authorizes cycle 4 refactoring
• Design report: .self-local/reports/design-refactor-c4-2026-07-17.md (13 blocks designed)
• Previous cycles: refactor: shake-driven import cleanup + CI audit gate (cycle 3) #4542 (cycle 3), refactor: split MayerMontroll and LayerPerronExistence along section boundaries + leftover cleanup #4539 (cycle 2), chore(issues): close-out mirror sync for #4535 refactor cycle #4537 (cycle 1)

Outcome (2026-07-17, build-verified)

9 of 13 designed blocks applied; 4 reverted as build-proven false positives (shake
suggestions are candidates only — lake build is the arbiter, per the #4541 governance note).
See .self-local/reports/implement-4544-2026-07-17.md for the full per-file table.

Reverted (4, all build errors on apply):

• Basic.lean — deriving Fintype needs Tactic.DeriveFintype (shake dropped it)
• Hamiltonian.lean — ring tactic needs more than Tactic.Ring.Basic
• Inequalities/WeightedExpectation.lean — same ring tactic gap
• ClusterExpansion/MayerCore/SurjectiveLogWeight.lean — positivity tactic gap

Applied (9): Dobrushin/SingleSiteInfluence.lean, ClusterExpansion/RootedParentActive.lean,
ComplexAnalyticity/Compactness.lean, Peierls/LiminfBound.lean, Peierls/LowTempTail.lean,
Concrete/.../MassContinuityUniformInfLipschitz.lean, ClusterExpansion/SourceLogCoefficient.lean,
ClusterExpansion/PiFinsetSeparation.lean, TransferMatrix/LayerCylinderGraph.lean.

Gates: lake build IsingModel zero warnings, lake exe GKSTest PASS, audit_gate.py --full
PASS (V1/V2/V3), umbrella-preservation grep empty (verified independently by issue-manager:
git diff -U0 69da4efb..HEAD -- IsingModel/ | grep -E '^[+-]import IsingModel' → 0 matches).

Deferred (not this PR): 668 IsingModel.* umbrella downgrades + 298 coupled chains remain
enumerated-and-deferred pending an explicit umbrella-convention ruling from the user. This
exhausts the mathlib-only subset of the third /goal issuance; the repo-internal 668/298 set
requires user decision before any future cycle can proceed on it.

PR Reference

Closed by #4545.