refactor: drop unused triple_ratio_bundle variants in FreeEnergyRatios

[phasetr]

Per the #4639 adoption rule.

Summary

Delete seven zero-consumer, reference-0 wrapper theorems from
IsingModel/Conditioning/HighTempClosed/FreeEnergyRatios.lean — pure
_beta_zero / _ferromagnetic re-bundlings of the four published base bundles,
with no consumer anywhere in the library, docs, or tex:

1. freeEnergy_high_temp_h_zero_ratio_sandwich_bundle_ferromagnetic
2. partitionFunction_high_temp_expansion_h_zero_triple_ratio_sandwich_bundle_beta_zero
3. partitionFunction_high_temp_expansion_h_zero_triple_ratio_sandwich_bundle_ferromagnetic
4. partitionFunction_high_temp_expansion_h_zero_triple_ratio_sandwich_bundle_beta_zero_ferromagnetic
5. partitionFunction_high_temp_expansion_h_zero_triple_ratio_bound_bundle_beta_zero
6. partitionFunction_high_temp_expansion_h_zero_triple_ratio_bound_bundle_ferromagnetic
7. partitionFunction_high_temp_expansion_h_zero_triple_ratio_bound_bundle_beta_zero_ferromagnetic

Protected base bundles (untouched, docs:2127 verbatim citations):
freeEnergy_high_temp_h_zero_ratio_sandwich_bundle,
partitionFunction_high_temp_expansion_h_zero_triple_ratio_sandwich_bundle,
partitionFunction_high_temp_expansion_h_zero_triple_ratio_bound_bundle,
partitionFunction_high_temp_expansion_h_zero_strict_deviation_bundle.
Every sibling layer (Lambda / AlongExhaustion / latticeGraph) is untouched;
proof power is unchanged.

Same-commit bookkeeping (permanent fix for stale-reference recurrence)

• docs/index.md §18.3: reconciled the abstract-layer prose that enumerated the
  now-deleted _beta_zero / _ferromagnetic variants (the beta=0 triple sandwich
  bundle went from "at abstract / Lambda / along-ex / Z^d Lambda / Z^d along-ex
  layers, ferromagnetic at all 5 layers" to 4 layers). Other-layer aggregates
  (PR Split AmbientLattice/SpecialCases/HighTemperatureBoundsRatioBounds triple_ratio wrappers #1994/Split Concrete/LatticeGraphCorrelation/HighTemperatureBoundsAlongExhaustionRatioBounds triple_ratio wrappers #1996/Split Concrete/LatticeGraphCorrelation/HighTemperatureBoundsRatioBounds Λ-direct triple_ratio wrappers #1998) left untouched.
• scripts/test_dead_candidate_scan.py: recalibrated the _ferromagnetic
  family fixtures.

Verification

• lake build (FreeEnergyRatios + HighTempClosed importer): PASS, zero warnings.
• audit_gate.py --full: V1-V4 PASS. --self-test: 166 OK.
• dead_candidate_scan.py --self-test: 79 OK (after fixture recalibration).
• lake exe GKSTest: PASS.
• git grep: the 7 deleted names are absent from IsingModel/, docs/, tex/;
  the 4 base bundles remain intact.

Fixture recalibration (breakdown invariant, only SAFE+total+zero-consumer drop by 5)

The 5 deleted decls ending in _ferromagnetic (#1,#3,#4,#6,#7) are the only ones
in the _ferromagnetic calibration family; #2 and #5 (plain _beta_zero) are
outside it.

ferromagnetic family: total 236 (was 241)
  safe-to-delete:  105 (was 110)   <- drops by 5
  uncertain:        44 (invariant)
  load-bearing:     52 (invariant)
  published-result: 35 (invariant)
  zero-consumer:   123 (was 128)   <- drops by 5

Healthy signature: only SAFE + total + zero-consumer drop by exactly 5; the other
three classes are invariant, so no live lemma was reclassified (#4655).

Post-deletion cascade check (base 4, textual)

-- published-result: 4 --
  freeEnergy_high_temp_h_zero_ratio_sandwich_bundle
      reason: cited verbatim in the public documentation
      cross-file consumer: IsingModel/AmbientLattice/Defs/HighTempPartition/Ratios.lean:243
  partitionFunction_high_temp_expansion_h_zero_strict_deviation_bundle
      reason: cited verbatim in the public documentation
  partitionFunction_high_temp_expansion_h_zero_triple_ratio_bound_bundle
      reason: cited verbatim in the public documentation
  partitionFunction_high_temp_expansion_h_zero_triple_ratio_sandwich_bundle
      reason: cited verbatim in the public documentation
-- load-bearing: 0 --
-- uncertain: 0 --
-- safe-to-delete: 0 --
-- cascade (informational, never auto-deleted): 0 --

Post-deletion cascade check (base 4, --lean build-backed)

--lean cross-check: 4 candidate(s) compared against the elaborated graph;
  no consumer seen by Lean was missed on a safe-to-delete verdict
-- published-result: 4 --
-- load-bearing: 0 --
-- uncertain: 0 --
-- safe-to-delete: 0 --
-- cascade (informational, never auto-deleted): 0 --

Cascade is zero: no base decl became reference-0.

LIMITS banner (scanner)

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.

🤖 Generated with Claude Code