refactor: drop the third ratio_bound_bundle cluster

IsingModel/AmbientLattice/Defs/HighTempPartition/Ratios.lean

@@ -217,35 +217,6 @@ theorem log_partitionFunctionΛ_high_temp_expansion_h_zero_ratio_bound_beta_zero
   exact IsingModel.log_partitionFunction_high_temp_expansion_h_zero_ratio_bound_beta_zero
     (inducedGraph G Λ) J β hβJ
 
-/-- **Λ-level log Z ratio bound bundle**. -/
-theorem log_partitionFunctionΛ_high_temp_expansion_h_zero_ratio_bound_bundle
-    (G : SimpleGraph V) (Λ : Finset V)
-    [Fintype (inducedGraph G Λ).edgeSet]
-    (J β : ℝ) (hβJ : 0 ≤ β * J) :
-    Real.log (partitionFunctionΛ G Λ (⟨J, 0, β⟩ : IsingParams ℝ))
-        - Real.log (partitionFunctionΛ G Λ (⟨0, 0, β⟩ : IsingParams ℝ))
-        ≤ β * J * (inducedGraph G Λ).edgeFinset.card ∧
-    Real.log (partitionFunctionΛ G Λ (⟨J, 0, β⟩ : IsingParams ℝ))
-        - Real.log (partitionFunctionΛ G Λ (⟨J, 0, 0⟩ : IsingParams ℝ))
-        ≤ β * J * (inducedGraph G Λ).edgeFinset.card :=
-  ⟨log_partitionFunctionΛ_high_temp_expansion_h_zero_ratio_bound G Λ J β hβJ,
-   log_partitionFunctionΛ_high_temp_expansion_h_zero_ratio_bound_beta_zero
-     G Λ J β hβJ⟩
-
-/-- **Λ-level ferromagnetic log Z ratio bound bundle**. -/
-theorem log_partitionFunctionΛ_high_temp_expansion_h_zero_ratio_bound_bundle_ferromagnetic
-    (G : SimpleGraph V) (Λ : Finset V)
-    [Fintype (inducedGraph G Λ).edgeSet]
-    (J β : ℝ) (hJ : 0 ≤ J) (hβ : 0 < β) :
-    Real.log (partitionFunctionΛ G Λ (⟨J, 0, β⟩ : IsingParams ℝ))
-        - Real.log (partitionFunctionΛ G Λ (⟨0, 0, β⟩ : IsingParams ℝ))
-        ≤ β * J * (inducedGraph G Λ).edgeFinset.card ∧
-    Real.log (partitionFunctionΛ G Λ (⟨J, 0, β⟩ : IsingParams ℝ))
-        - Real.log (partitionFunctionΛ G Λ (⟨J, 0, 0⟩ : IsingParams ℝ))
-        ≤ β * J * (inducedGraph G Λ).edgeFinset.card :=
-  log_partitionFunctionΛ_high_temp_expansion_h_zero_ratio_bound_bundle
-    G Λ J β (mul_nonneg hβ.le hJ)
-
 /-- **Λ-level f ratio sandwich bundle**. -/
 theorem freeEnergyΛ_high_temp_h_zero_ratio_sandwich_bundle
     (G : SimpleGraph V) (Λ : Finset V)

IsingModel/Concrete/LatticeGraphCorrelation/HighTemperatureBoundsRatioLogFe.lean

@@ -139,13 +139,16 @@ log_partitionFunctionΛ_latticeGraph_high_temp_expansion_h_zero_ratio_sandwich_b
   log_partitionFunctionΛ_high_temp_expansion_h_zero_ratio_sandwich_bundle_ferromagnetic
     (IsingModel.latticeGraph d) Λ J β hJ hβ
 
-/-! ## Moved: Λ-direct ratio_bound_bundle wrappers
-
-The four Λ-direct `ratio_bound_bundle` wrappers
-(`log_partitionFunctionΛ_latticeGraph_*_ratio_bound_bundle`
-and `freeEnergyΛ_latticeGraph_*_ratio_bound_bundle`,
-each with `_ferromagnetic` variants) now live in
-`HighTemperatureBoundsRatioBoundBundle.lean`. -/
+/-! ## Removed: Λ-direct ratio_bound_bundle wrappers
+
+The Λ-direct `log_partitionFunctionΛ_latticeGraph_*_ratio_bound_bundle`
+conjunction wrappers (and their `_ferromagnetic` variants) were removed as
+unused bundles; they delegated directly to the ambient base
+`log_partitionFunctionΛ_high_temp_expansion_h_zero_ratio_bound` and
+`log_partitionFunctionΛ_high_temp_expansion_h_zero_ratio_bound_beta_zero`
+lemmas (in `AmbientLattice/Defs/HighTempPartition/Ratios.lean`), which remain.
+The companion `freeEnergyΛ_latticeGraph_*_ratio_bound_bundle` wrappers had
+already been dropped. -/
 
 
 

IsingModel/Concrete/LatticeGraphCorrelation/Umbrella/HighTemperature.lean

@@ -63,7 +63,6 @@ import IsingModel.Concrete.LatticeGraphCorrelation.HighTemperatureBoundsFreeEner
 import IsingModel.Concrete.LatticeGraphCorrelation.HighTemperatureBoundsFreeEnergyInfiniteDeviationAndRatio
 import IsingModel.Concrete.LatticeGraphCorrelation.HighTemperatureBoundsLambdaCompleteSummary
 import IsingModel.Concrete.LatticeGraphCorrelation.HighTemperatureBoundsNumerator
-import IsingModel.Concrete.LatticeGraphCorrelation.HighTemperatureBoundsRatioBoundBundle
 import IsingModel.Concrete.LatticeGraphCorrelation.HighTemperatureBoundsRatioBounds
 import IsingModel.Concrete.LatticeGraphCorrelation.HighTemperatureBoundsRatioBoundsBound
 import IsingModel.Concrete.LatticeGraphCorrelation.HighTemperatureBoundsRatioBoundsBoundBundle

scripts/test_dead_candidate_scan.py

@@ -894,32 +894,33 @@ class FamilyCalibrationTest(unittest.TestCase):
     """
 
     def test_ferromagnetic_family_counts(self) -> None:
-        """252 candidates -> 121 safe / 44 uncertain / 52 load-bearing / 35 published.
+        """250 candidates -> 119 safe / 44 uncertain / 52 load-bearing / 35 published.
 
-        Recalibrated when the PR #4663 second ratio_bound_bundle cluster deleted the
-        four safe-to-delete ``freeEnergy{Λ,AlongExhaustion}{,_latticeGraph}_high_temp*_h_zero_ratio_bound_bundle_ferromagnetic``
-        wrappers: total and safe both drop by 4, and the other three classes are
+        Recalibrated when the PR #4665 third ratio_bound_bundle cluster deleted the
+        two safe-to-delete ``log_partitionFunctionΛ{,_latticeGraph}_high_temp_expansion_h_zero_ratio_bound_bundle_ferromagnetic``
+        wrappers: total and safe both drop by 2, and the other three classes are
         unchanged -- the healthy signature that no live lemma was reclassified.
-        (Was 256 -> 125 safe after PR #4661 removed three base-Conditioning wrappers.)
+        (Was 252 -> 121 safe after PR #4663 removed four freeEnergy-stem wrappers.)
         """
         verdicts = family_verdicts()
         counts: dict[str, int] = {}
         for verdict in verdicts:
             counts[verdict.verdict] = counts.get(verdict.verdict, 0) + 1
-        self.assertEqual(len(verdicts), 252)
-        self.assertEqual(counts.get(dcs.SAFE), 121)
+        self.assertEqual(len(verdicts), 250)
+        self.assertEqual(counts.get(dcs.SAFE), 119)
         self.assertEqual(counts.get(dcs.UNCERTAIN), 44)
         self.assertEqual(counts.get(dcs.LOAD_BEARING), 52)
         self.assertEqual(counts.get(dcs.PUBLISHED), 35)
 
     def test_zero_consumer_count(self) -> None:
-        """136 of the 252 have no Lean consumer at all.
+        """135 of the 250 have no Lean consumer at all.
 
-        Was 138 of 256 before the PR #4663 second cluster; two of the four deleted
-        ratio_bound_bundle ferromagnetic wrappers (the two ``_latticeGraph`` leaves)
-        were themselves zero-consumer, so the count drops by two.
+        Was 136 of 252 before the PR #4665 third cluster; of the two deleted
+        log_partitionFunctionΛ ratio_bound_bundle ferromagnetic wrappers only the
+        ``_latticeGraph`` leaf was itself zero-consumer (the base wrapper feeds that
+        leaf), so the count drops by one.
         """
-        self.assertEqual(sum(1 for v in family_verdicts() if not v.consumers), 136)
+        self.assertEqual(sum(1 for v in family_verdicts() if not v.consumers), 135)
 
 
 class CanaryTest(unittest.TestCase):