refactor: drop the third ratio_bound_bundle cluster

[phasetr]

Summary

Simplification refactor under the user's standing authorization, continuing the
scanner-vetted ratio_bound_bundle deletions of #4661 (six base-Conditioning
wrappers) and #4663 (eight freeEnergy-stem wrappers). This PR removes the next
self-contained closure-component: the log_partitionFunctionΛ stem vertical
slice (4 declarations). All four are pure conjunction wrappers that only pair the
already-proved _ratio_bound / _ratio_bound_beta_zero facts with ⟨·, ·⟩;
nothing outside the closure references them, so the deletion cascade is empty.

Removed (4 declarations)

Base Λ-level bundles in AmbientLattice/Defs/HighTempPartition/Ratios.lean:

• log_partitionFunctionΛ_high_temp_expansion_h_zero_ratio_bound_bundle
• log_partitionFunctionΛ_high_temp_expansion_h_zero_ratio_bound_bundle_ferromagnetic

The two latticeGraph wrappers, which were the only declarations in
Concrete/LatticeGraphCorrelation/HighTemperatureBoundsRatioBoundBundle.lean
(file removed entirely, umbrella import dropped):

• log_partitionFunctionΛ_latticeGraph_high_temp_expansion_h_zero_ratio_bound_bundle
• log_partitionFunctionΛ_latticeGraph_high_temp_expansion_h_zero_ratio_bound_bundle_ferromagnetic

Self-contained / umbrella / underlying lemmas

• Self-contained: the two base bundles are consumed only by their own
  _ferromagnetic sibling and the two latticeGraph wrappers (all in-set); the
  latticeGraph wrappers are leaves. Cascade is zero.
• Umbrella re-export surface preserved (per refactor: drop the second ratio_bound_bundle cluster #4663 Med finding, not narrowed):
  the removed file imported IsingModel.Lattice and
  Concrete.LatticeGraphBED.LatticeBoundaryBED. Both remain transitively
  reachable from Umbrella/HighTemperature.lean via the still-imported
  HighTemperatureBoundsRatioLogFe (which imports both directly). Whole build
  green confirms no consumer lost an import.
• Underlying lemmas remain: log_partitionFunctionΛ_high_temp_expansion_h_zero_ratio_bound
  and _ratio_bound_beta_zero stay (still consumed by the triple-ratio bundle and
  the LogBoundOnlySingletons wrappers).
• The stale "Moved" docstring in HighTemperatureBoundsRatioLogFe.lean is updated
  in the same commit.

Scanner evidence

Pre-deletion textual verdict (all four safe-to-delete)

python3 scripts/dead_candidate_scan.py --pattern 'ratio_bound_bundle' --report-only
classified the full family as 1 published-result / 2 load-bearing / 2 uncertain
/ 29 safe-to-delete. All four deleted names were in safe-to-delete
(no reference outside the delete set, no citation in the scanned documentation).

Post-deletion textual re-scan (cascade for this component = 0)

python3 scripts/dead_candidate_scan.py --pattern 'ratio_bound_bundle' --report-only:

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

published-result / load-bearing / uncertain all unchanged; safe-to-delete
29 → 25 (−4 = exactly the deleted decls). The cascade: 7 is the scanner's
forward-looking "if you deleted all 25 remaining safe candidates" set (the
untouched triple_ratio_bound_bundle batch + underlying _ratio_bound lemmas);
those underlying lemmas remain live (consumed outside the touched family), so
this component's own cascade is empty.

--lean build-backed cross-check (elaborated graph, green build)

python3 scripts/dead_candidate_scan.py --pattern 'log_partitionFunctionΛ.*_ratio_bound' --lean
on the touched family:

-- uncertain: 0 --
-- safe-to-delete: 0 --
-- cascade (informational, never auto-deleted): 0 --
-- documentation family labels (attributed to no declaration): 849 --
-- coverage warnings: 0 (each forces `uncertain` on every candidate it could be citing) --
elapsed: 29.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.

The elaborated dependency graph confirms 0 cascade from the deletion.

_ferromagnetic fixture calibration (unchanged split)

Two of the four deleted decls are _ferromagnetic, so
test_dead_candidate_scan.py calibration is retuned. The split is the healthy
no-reclassification signature — only total and safe drop by the deletion count:

metric	before	after
total	252	250 (−2)
safe-to-delete	121	119 (−2)
uncertain	44	44
load-bearing	52	52
published-result	35	35
zero-consumer	136	135 (−1)

(zero-consumer −1: only the latticeGraph leaf ferro wrapper was zero-consumer;
the base ferro wrapper feeds that leaf.)

Verification

• lake build — completed successfully (5058 jobs), warning-free in touched
  modules (the only info: lines are pre-existing Try this diagnostics in the
  untouched TransferMatrix/TwoSiteInteractingLayerOpenBoundaryWindow.lean).
• scripts/audit_gate.py --full — V1–V4 PASS.
• scripts/audit_gate.py --self-test — 166 OK (skipped=1).
• scripts/dead_candidate_scan.py --self-test — 79 OK (after fixture retune).
• lake exe GKSTest — All tests passed.
• Deleted names absent repo-wide; underlying _ratio_bound lemmas retained.

🤖 Generated with Claude Code