refactor: drop the correlationΛ pair-singleton bundle cluster

[phasetr]

Motivation

Simplification refactor under the user's standing authorization, continuing the scanner-vetted deletions of #4648/#4651/#4655/#4657. A systematic scanner pass (.self-local/reports/remaining-safe-clusters-2026-07-22.md) enumerated the remaining self-contained safe-to-delete clusters; this PR takes the correlationΛ ... at_pair_singleton_bundle cluster (8 declarations, 2 closure-components). This is a distinct namespace from the correlationAlongExhaustion family removed in #4655 and has not been touched before. None of these _bundle lemmas is cited by docs/index.md or tex/proof-guide.tex; they only pair two already-proved facts with ⟨a,b⟩ and are consumed by nothing outside the deleted set.

Deleted declarations (8)

Ambient layer — IsingModel/AmbientLattice/Defs/HighTempCorrelation.lean:

• correlationΛ_high_temp_h_zero_at_pair_singleton_bundle
• correlationΛ_high_temp_h_zero_at_pair_singleton_bundle_ferromagnetic
• correlationΛ_high_temp_h_zero_at_pair_singleton_complete_summary
• correlationΛ_high_temp_h_zero_at_pair_singleton_trivial_slices_bundle

ℤ^d latticeGraph layer:

• correlationΛ_latticeGraph_high_temp_h_zero_at_pair_singleton_bundle (HighTemperatureBoundsCorrelationBasicBundles.lean)
• correlationΛ_latticeGraph_high_temp_h_zero_at_pair_singleton_bundle_ferromagnetic (HighTemperatureBoundsPairSingletonBundle.lean)
• correlationΛ_latticeGraph_high_temp_h_zero_at_pair_singleton_complete_summary (HighTemperatureBoundsPairSingletonBundle.lean)
• correlationΛ_latticeGraph_high_temp_h_zero_at_pair_singleton_trivial_slices_bundle (HighTemperatureBoundsPairSingletonBundle.lean)

HighTemperatureBoundsPairSingletonBundle.lean held all 3 _latticeGraph_ wrappers, so it becomes declaration-free and is deleted whole; its umbrella import (Umbrella/HighTemperature.lean) is dropped. Transitive reachability is preserved: the sibling HighTemperatureBoundsCorrelationBasicBundles.lean (kept) still imports LatticeGraphBED.LatticeBoundaryBED, and IsingModel.Lattice remains reachable from the umbrella by many other paths (confirmed green build). Two stale module-docstring prose mentions were updated in the same commit: the HighTemperatureBoundsCorrelationBasicBundles.lean header (five → four wrappers, dropped bullet) and the HighTemperatureBounds.lean "Moved: ℤ^d HT pair+singleton bundle wrappers" section.

Follow-up (commit 48d88aa3, doc comments only): review (dev-review + codex) found three further stale docstring mentions of the removed correlationΛ_latticeGraph_high_temp_h_zero_at_pair_singleton_bundle wrapper that the first commit missed. All three are now purged, with no declaration/statement change:

• HighTemperatureBounds.lean "Moved: correlationΛ pair / singleton basic wrappers" note — dropped pair+singleton bundle from the enumeration.
• HighTemperatureBoundsCorrelationBasic.lean module header — dropped the pair+singleton bundle list item.
• HighTemperatureBoundsCorrelationBasic.lean "Moved: pair sandwich / ferromagnetic / bundle wrappers" note — five → four wrappers, removed pair_singleton_bundle, matching the already-narrowed sibling HighTemperatureBoundsCorrelationBasicBundles.lean header.

The HighTemperatureBounds.lean:189 alongExhaustion note and the abstract correlation_high_temp_h_zero_at_pair_singleton_bundle declaration name a distinct, still-live family and are deliberately left untouched. After this follow-up, zero references to the 8 deleted names remain across IsingModel/, docs/, tex/.

Note (deviation from the research report): the report expected this correlationΛ cluster to carry no _ferromagnetic-named member; in fact 2 of the 8 (..._at_pair_singleton_bundle_ferromagnetic, both layers) do. They are legitimately safe-to-delete and their removal recalibrated the scanner's _ferromagnetic self-test fixture (see below).

Pre-deletion scanner output (scripts/dead_candidate_scan.py, textual + --lean)

--lean cross-check: 8 candidate(s) compared against the elaborated graph; no consumer seen by Lean was missed on a safe-to-delete verdict
== dead-candidate scan ==
canary: 1096 declarations carrying 'Λ'x1093, 'β'x1, 'σ'x2 each find themselves: PASS
canary: 10903 code citations in tex/proof-guide.tex, none broken across a line: PASS

-- published-result: 0 --

-- load-bearing: 0 --

-- uncertain: 0 --

-- safe-to-delete: 8 --
  IsingModel.Ambient.correlationΛ_high_temp_h_zero_at_pair_singleton_bundle  [theorem]  IsingModel/AmbientLattice/Defs/HighTempCorrelation.lean:351
      reason: no reference outside the delete set, no citation in the scanned documentation (README.md, docs/**/*.md, tex/proof-guide.tex)
      same-file consumer: IsingModel/AmbientLattice/Defs/HighTempCorrelation.lean:373 in IsingModel.Ambient.correlationΛ_high_temp_h_zero_at_pair_singleton_bundle_ferromagnetic
      cross-file consumer: IsingModel/Concrete/LatticeGraphCorrelation/HighTemperatureBoundsCorrelationBasicBundles.lean:72 in IsingModel.Ambient.correlationΛ_latticeGraph_high_temp_h_zero_at_pair_singleton_bundle
  IsingModel.Ambient.correlationΛ_high_temp_h_zero_at_pair_singleton_bundle_ferromagnetic  [theorem]  IsingModel/AmbientLattice/Defs/HighTempCorrelation.lean:366
      reason: no reference outside the delete set, no citation in the scanned documentation (README.md, docs/**/*.md, tex/proof-guide.tex)
      info: mentioned in prose at IsingModel/Concrete/LatticeGraphCorrelation/HighTemperatureBoundsPairSingletonBundle.lean:23 (doc comment) -- deleting it leaves that text stale
      cross-file consumer: IsingModel/Concrete/LatticeGraphCorrelation/HighTemperatureBoundsPairSingletonBundle.lean:34 in IsingModel.Ambient.correlationΛ_latticeGraph_high_temp_h_zero_at_pair_singleton_bundle_ferromagnetic
  IsingModel.Ambient.correlationΛ_high_temp_h_zero_at_pair_singleton_complete_summary  [theorem]  IsingModel/AmbientLattice/Defs/HighTempCorrelation.lean:381
      reason: no reference outside the delete set, no citation in the scanned documentation (README.md, docs/**/*.md, tex/proof-guide.tex)
      info: mentioned in prose at IsingModel/Concrete/LatticeGraphCorrelation/HighTemperatureBoundsPairSingletonBundle.lean:41 (doc comment) -- deleting it leaves that text stale
      cross-file consumer: IsingModel/Concrete/LatticeGraphCorrelation/HighTemperatureBoundsPairSingletonBundle.lean:56 in IsingModel.Ambient.correlationΛ_latticeGraph_high_temp_h_zero_at_pair_singleton_complete_summary
  IsingModel.Ambient.correlationΛ_high_temp_h_zero_at_pair_singleton_trivial_slices_bundle  [theorem]  IsingModel/AmbientLattice/Defs/HighTempCorrelation.lean:400
      reason: no reference outside the delete set, no citation in the scanned documentation (README.md, docs/**/*.md, tex/proof-guide.tex)
      info: mentioned in prose at IsingModel/Concrete/LatticeGraphCorrelation/HighTemperatureBoundsPairSingletonBundle.lean:62 (doc comment) -- deleting it leaves that text stale
      cross-file consumer: IsingModel/Concrete/LatticeGraphCorrelation/HighTemperatureBoundsPairSingletonBundle.lean:74 in IsingModel.Ambient.correlationΛ_latticeGraph_high_temp_h_zero_at_pair_singleton_trivial_slices_bundle
  IsingModel.Ambient.correlationΛ_latticeGraph_high_temp_h_zero_at_pair_singleton_bundle  [theorem]  IsingModel/Concrete/LatticeGraphCorrelation/HighTemperatureBoundsCorrelationBasicBundles.lean:63
      reason: no reference outside the delete set, no citation in the scanned documentation (README.md, docs/**/*.md, tex/proof-guide.tex)
  IsingModel.Ambient.correlationΛ_latticeGraph_high_temp_h_zero_at_pair_singleton_bundle_ferromagnetic  [theorem]  IsingModel/Concrete/LatticeGraphCorrelation/HighTemperatureBoundsPairSingletonBundle.lean:24
      reason: no reference outside the delete set, no citation in the scanned documentation (README.md, docs/**/*.md, tex/proof-guide.tex)
  IsingModel.Ambient.correlationΛ_latticeGraph_high_temp_h_zero_at_pair_singleton_complete_summary  [theorem]  IsingModel/Concrete/LatticeGraphCorrelation/HighTemperatureBoundsPairSingletonBundle.lean:42
      reason: no reference outside the delete set, no citation in the scanned documentation (README.md, docs/**/*.md, tex/proof-guide.tex)
  IsingModel.Ambient.correlationΛ_latticeGraph_high_temp_h_zero_at_pair_singleton_trivial_slices_bundle  [theorem]  IsingModel/Concrete/LatticeGraphCorrelation/HighTemperatureBoundsPairSingletonBundle.lean:63
      reason: no reference outside the delete set, no citation in the scanned documentation (README.md, docs/**/*.md, tex/proof-guide.tex)

-- cascade (informational, never auto-deleted): 0 --

-- documentation family labels (attributed to no declaration): 849 --
  (unchanged global docs-family label listing, attributed to no candidate)

-- coverage warnings: 0 (each forces `uncertain` on every candidate it could be citing) --

elapsed: 40.8s

LIMITS: this scan is textual. It cannot see simp/aesop set usage, tactic-generated
references, open/export-shortened names, or metaprogrammed names. It does not check
autoImplicit binder drift (a `#check @` dump is a separate gate). Doc rows that depend
on a lemma without naming it are invisible. Run with --lean on a green build to
cross-check the elaborated dependency graph; run --explain for the full table.
A "safe-to-delete" verdict is a necessary, not a sufficient, condition for deletion.

All 8 classify safe-to-delete under both the textual scan and the --lean elaborated-graph cross-check (no consumer missed), cascade 0.

Post-deletion cascade re-run

The 8 deleted names no longer exist, so the faithful post-deletion check re-scans the 7 constituent lemmas the bundles consumed (correlationΛ_high_temp_h_zero_at_{singleton, pair_nonneg, pair_le_one, pair_J_zero, pair_beta_zero, singleton_J_zero, singleton_beta_zero}):

-- published-result: 0 --
-- load-bearing: 7 --
-- uncertain: 0 --
-- safe-to-delete: 0 --
-- cascade (informational, never auto-deleted): 0 --

Every constituent survives as load-bearing (each still referenced by _latticeGraph_ / trivial-slices / along-exhaustion wrappers) — the deletion orphaned nothing; cascade 0.

_ferromagnetic self-test recalibration

2 deleted names carry _ferromagnetic, so dead_candidate_scan.py --self-test's FamilyCalibrationTest recalibrates. Measured before → after:

• total: 261 → 259 (−2, the two deleted safe _ferromagnetic bundles)
• SAFE: 130 → 128 (−2), UNCERTAIN: 44 → 44, LOAD_BEARING: 52 → 52, PUBLISHED: 35 → 35 (unchanged)
• zero-consumer: 142 → 141 (−1; the _latticeGraph_ bundle-ferromagnetic wrapper was itself zero-consumer)

Only total, SAFE, and the zero-consumer count drop by exactly the deletion counts; the other three classes are unchanged — the healthy signature that no live lemma was reclassified. Fixture integers in scripts/test_dead_candidate_scan.py updated accordingly.

Verification

• Full scanner output with LIMITS: banner pasted (textual scan + --lean cross-check); all 8 safe-to-delete
• No remaining references anywhere (all 8 names + module name absent repo-wide, substring-checked)
• All stale docstring prose referencing the deleted wrapper purged (3 further mentions fixed in follow-up 48d88aa3; existing alongExhaustion / abstract correlation_* families left intact)
• Post-deletion cascade re-run with full output showing cascade 0
• No new reference-0 declaration created (7 constituents all load-bearing)
• lake build warning-free, error-free — "Build completed successfully (5061 jobs)"
• scripts/audit_gate.py --full V1–V4 PASS
• audit_gate.py --self-test (166 OK) and dead_candidate_scan.py --self-test (79 OK, after recalibration)
• _ferromagnetic fixture SAFE/UNCERTAIN/LOAD_BEARING/PUBLISHED split shown (SAFE −2, others unchanged)
• lake exe GKSTest PASS
• Declaration-name diff vs main = exactly 8 removed, 0 added (insertions are docstring/prose only)

🤖 Generated with Claude Code

[phasetr]

dev-issue-manager resolution-verification (round 5 of the #4639 adoption rule)

Verified independently (not from PR author's claims):

• rg for all 8 deleted declaration names across IsingModel/, docs/, tex/: zero hits at HEAD (48d88aa3).
• HighTemperatureBoundsPairSingletonBundle.lean confirmed deleted (file absent).
• The 3 stale-docstring mentions flagged by dev-review are gone; the still-live correlationAlongExhaustion_latticeGraph family and the abstract correlation_high_temp_h_zero_at_pair_singleton_bundle declaration are untouched, as intended.
• Fixture recalibration in scripts/test_dead_candidate_scan.py confirmed by diff: total 261→259, SAFE 130→128, UNCERTAIN/LOAD_BEARING/PUBLISHED unchanged (44/52/35), zero-consumer 142→141 — exactly matches the PR body's claimed healthy-signature recalibration (no keeper reclassified).
• Spot-checked persistence of the refactor: drop twelve dead pseudoMassG decoration lemmas #4641 keeper freeEnergyAlongExhaustion_nonneg_of_ferromagnetic: still present and still consumed by 3 call sites — confirms it was not touched by this deletion.
• 785a1370 (deletion) + 48d88aa3 (docstring follow-up) are both real, separate, non-amended commits — the follow-up correctly used a new commit rather than amending, consistent with "don't amend past the PR-early-creation placeholder."

Governance note: recommend the #4639 adoption-rule text be tightened to state explicitly that once a PR has a real implementation commit, follow-up fixes (e.g. review-flagged stale docstrings) must land as new commits, not amends — this round did it correctly; making the rule explicit prevents regression in future rounds.

Outstanding at time of this comment: CI (Lean Action CI / build) was still IN_PROGRESS — merge should wait for a green completion before proceeding.