refactor: drop unused triple_ratio_bound_bundle wrappers

IsingModel/AmbientLattice/Defs/HighTempPartition/TripleRatios.lean

@@ -67,116 +67,6 @@ theorem partitionFunctionΛ_high_temp_expansion_h_zero_triple_ratio_sandwich_bun
      G Λ J β hβJ).2,
    (freeEnergyΛ_high_temp_h_zero_ratio_sandwich_bundle G Λ J β hβJ hne).2⟩
 
-/-- **Λ-level ferromagnetic triple ratio sandwich bundle at β=0**. -/
-theorem
-partitionFunctionΛ_high_temp_expansion_h_zero_triple_ratio_sandwich_bundle_beta_zero_ferromagnetic
-    (G : SimpleGraph V) (Λ : Finset V)
-    [Fintype (inducedGraph G Λ).edgeSet]
-    (J β : ℝ) (hJ : 0 ≤ J) (hβ : 0 < β) (hne : 0 < Λ.card) :
-    (Real.cosh (β * J) ^ (inducedGraph G Λ).edgeFinset.card
-        ≤ partitionFunctionΛ G Λ (⟨J, 0, β⟩ : IsingParams ℝ) /
-            partitionFunctionΛ G Λ (⟨J, 0, 0⟩ : IsingParams ℝ) ∧
-      partitionFunctionΛ G Λ (⟨J, 0, β⟩ : IsingParams ℝ) /
-          partitionFunctionΛ G Λ (⟨J, 0, 0⟩ : IsingParams ℝ)
-          ≤ Real.exp (β * J * (inducedGraph G Λ).edgeFinset.card)) ∧
-    (((inducedGraph G Λ).edgeFinset.card : ℝ) * Real.log (Real.cosh (β * J))
-        ≤ Real.log (partitionFunctionΛ G Λ (⟨J, 0, β⟩ : IsingParams ℝ))
-            - Real.log (partitionFunctionΛ G Λ (⟨J, 0, 0⟩ : IsingParams ℝ)) ∧
-      Real.log (partitionFunctionΛ G Λ (⟨J, 0, β⟩ : IsingParams ℝ))
-          - Real.log (partitionFunctionΛ G Λ (⟨J, 0, 0⟩ : IsingParams ℝ))
-          ≤ β * J * (inducedGraph G Λ).edgeFinset.card) ∧
-    (((inducedGraph G Λ).edgeFinset.card : ℝ) / Λ.card *
-        Real.log (Real.cosh (β * J))
-        ≤ freeEnergyΛ G Λ (⟨J, 0, β⟩ : IsingParams ℝ)
-            - freeEnergyΛ G Λ (⟨J, 0, 0⟩ : IsingParams ℝ) ∧
-      freeEnergyΛ G Λ (⟨J, 0, β⟩ : IsingParams ℝ)
-          - freeEnergyΛ G Λ (⟨J, 0, 0⟩ : IsingParams ℝ)
-          ≤ β * J * (inducedGraph G Λ).edgeFinset.card / Λ.card) :=
-  partitionFunctionΛ_high_temp_expansion_h_zero_triple_ratio_sandwich_bundle_beta_zero
-    G Λ J β (mul_nonneg hβ.le hJ) hne
-
-/-- **Λ-level ferromagnetic triple ratio sandwich bundle at J=0**. -/
-theorem partitionFunctionΛ_high_temp_expansion_h_zero_triple_ratio_sandwich_bundle_ferromagnetic
-    (G : SimpleGraph V) (Λ : Finset V)
-    [Fintype (inducedGraph G Λ).edgeSet]
-    (J β : ℝ) (hJ : 0 ≤ J) (hβ : 0 < β) (hne : 0 < Λ.card) :
-    (Real.cosh (β * J) ^ (inducedGraph G Λ).edgeFinset.card
-        ≤ partitionFunctionΛ G Λ (⟨J, 0, β⟩ : IsingParams ℝ) /
-            partitionFunctionΛ G Λ (⟨0, 0, β⟩ : IsingParams ℝ) ∧
-      partitionFunctionΛ G Λ (⟨J, 0, β⟩ : IsingParams ℝ) /
-          partitionFunctionΛ G Λ (⟨0, 0, β⟩ : IsingParams ℝ)
-          ≤ Real.exp (β * J * (inducedGraph G Λ).edgeFinset.card)) ∧
-    (((inducedGraph G Λ).edgeFinset.card : ℝ) * Real.log (Real.cosh (β * J))
-        ≤ Real.log (partitionFunctionΛ G Λ (⟨J, 0, β⟩ : IsingParams ℝ))
-            - Real.log (partitionFunctionΛ G Λ (⟨0, 0, β⟩ : IsingParams ℝ)) ∧
-      Real.log (partitionFunctionΛ G Λ (⟨J, 0, β⟩ : IsingParams ℝ))
-          - Real.log (partitionFunctionΛ G Λ (⟨0, 0, β⟩ : IsingParams ℝ))
-          ≤ β * J * (inducedGraph G Λ).edgeFinset.card) ∧
-    (((inducedGraph G Λ).edgeFinset.card : ℝ) / Λ.card *
-        Real.log (Real.cosh (β * J))
-        ≤ freeEnergyΛ G Λ (⟨J, 0, β⟩ : IsingParams ℝ)
-            - freeEnergyΛ G Λ (⟨0, 0, β⟩ : IsingParams ℝ) ∧
-      freeEnergyΛ G Λ (⟨J, 0, β⟩ : IsingParams ℝ)
-          - freeEnergyΛ G Λ (⟨0, 0, β⟩ : IsingParams ℝ)
-          ≤ β * J * (inducedGraph G Λ).edgeFinset.card / Λ.card) :=
-  partitionFunctionΛ_high_temp_expansion_h_zero_triple_ratio_sandwich_bundle
-    G Λ J β (mul_nonneg hβ.le hJ) hne
-
-/-- **Λ-level triple (Z + log Z + f) ratio bound bundle at J=0**. -/
-theorem partitionFunctionΛ_high_temp_expansion_h_zero_triple_ratio_bound_bundle
-    (G : SimpleGraph V) (Λ : Finset V)
-    [Fintype (inducedGraph G Λ).edgeSet]
-    (J β : ℝ) (hβJ : 0 ≤ β * J) (hne : 0 < Λ.card) :
-    partitionFunctionΛ G Λ (⟨J, 0, β⟩ : IsingParams ℝ) /
-        partitionFunctionΛ G Λ (⟨0, 0, β⟩ : IsingParams ℝ)
-        ≤ Real.exp (β * J * (inducedGraph G Λ).edgeFinset.card) ∧
-    Real.log (partitionFunctionΛ G Λ (⟨J, 0, β⟩ : IsingParams ℝ))
-        - Real.log (partitionFunctionΛ G Λ (⟨0, 0, β⟩ : IsingParams ℝ))
-        ≤ β * J * (inducedGraph G Λ).edgeFinset.card ∧
-    freeEnergyΛ G Λ (⟨J, 0, β⟩ : IsingParams ℝ)
-        - freeEnergyΛ G Λ (⟨0, 0, β⟩ : IsingParams ℝ)
-        ≤ β * J * (inducedGraph G Λ).edgeFinset.card / Λ.card :=
-  ⟨partitionFunctionΛ_high_temp_expansion_h_zero_ratio_bound G Λ J β hβJ,
-   log_partitionFunctionΛ_high_temp_expansion_h_zero_ratio_bound G Λ J β hβJ,
-   freeEnergyΛ_high_temp_h_zero_ratio_bound G Λ J β hβJ hne⟩
-
-/-- **Λ-level triple ratio bound bundle at β=0**. -/
-theorem partitionFunctionΛ_high_temp_expansion_h_zero_triple_ratio_bound_bundle_beta_zero
-    (G : SimpleGraph V) (Λ : Finset V)
-    [Fintype (inducedGraph G Λ).edgeSet]
-    (J β : ℝ) (hβJ : 0 ≤ β * J) (hne : 0 < Λ.card) :
-    partitionFunctionΛ G Λ (⟨J, 0, β⟩ : IsingParams ℝ) /
-        partitionFunctionΛ G Λ (⟨J, 0, 0⟩ : IsingParams ℝ)
-        ≤ Real.exp (β * 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 ∧
-    freeEnergyΛ G Λ (⟨J, 0, β⟩ : IsingParams ℝ)
-        - freeEnergyΛ G Λ (⟨J, 0, 0⟩ : IsingParams ℝ)
-        ≤ β * J * (inducedGraph G Λ).edgeFinset.card / Λ.card :=
-  ⟨partitionFunctionΛ_high_temp_expansion_h_zero_ratio_bound_beta_zero
-     G Λ J β hβJ,
-   log_partitionFunctionΛ_high_temp_expansion_h_zero_ratio_bound_beta_zero
-     G Λ J β hβJ,
-   freeEnergyΛ_high_temp_h_zero_ratio_bound_beta_zero G Λ J β hβJ hne⟩
-
-/-- **Λ-level ferromagnetic triple ratio bound bundle at J=0**. -/
-theorem partitionFunctionΛ_high_temp_expansion_h_zero_triple_ratio_bound_bundle_ferromagnetic
-    (G : SimpleGraph V) (Λ : Finset V)
-    [Fintype (inducedGraph G Λ).edgeSet]
-    (J β : ℝ) (hJ : 0 ≤ J) (hβ : 0 < β) (hne : 0 < Λ.card) :
-    partitionFunctionΛ G Λ (⟨J, 0, β⟩ : IsingParams ℝ) /
-        partitionFunctionΛ G Λ (⟨0, 0, β⟩ : IsingParams ℝ)
-        ≤ Real.exp (β * J * (inducedGraph G Λ).edgeFinset.card) ∧
-    Real.log (partitionFunctionΛ G Λ (⟨J, 0, β⟩ : IsingParams ℝ))
-        - Real.log (partitionFunctionΛ G Λ (⟨0, 0, β⟩ : IsingParams ℝ))
-        ≤ β * J * (inducedGraph G Λ).edgeFinset.card ∧
-    freeEnergyΛ G Λ (⟨J, 0, β⟩ : IsingParams ℝ)
-        - freeEnergyΛ G Λ (⟨0, 0, β⟩ : IsingParams ℝ)
-        ≤ β * J * (inducedGraph G Λ).edgeFinset.card / Λ.card :=
-  partitionFunctionΛ_high_temp_expansion_h_zero_triple_ratio_bound_bundle
-    G Λ J β (mul_nonneg hβ.le hJ) hne
-
 /-- **Λ-level ferromagnetic f ratio bound at J=0**. -/
 theorem freeEnergyΛ_high_temp_h_zero_ratio_bound_ferromagnetic
     (G : SimpleGraph V) (Λ : Finset V)

IsingModel/Concrete/LatticeGraphCorrelation/HighTemperatureBounds.lean

@@ -170,7 +170,7 @@ wrappers on `latticeGraph d` at `h = 0` for
 `partitionFunctionΛ_latticeGraph` (with `J = 0` / `β = 0` / `bundle`
 variants plus ferromagnetic counterparts) now live in
 `IsingModel.Concrete.LatticeGraphCorrelation.HighTemperatureBoundsRatioBounds`.
-The 7 `triple_ratio_*` wrappers now live in
+The 4 `triple_ratio_sandwich_bundle` wrappers now live in
 `IsingModel.Concrete.LatticeGraphCorrelation.HighTemperatureBoundsTripleRatio`
 (narrowed in PR #1998), and the 12 `log_partitionFunctionΛ_latticeGraph`
 / `freeEnergyΛ_latticeGraph` ratio wrappers now live in

IsingModel/Concrete/LatticeGraphCorrelation/HighTemperatureBoundsRatioBounds.lean

@@ -7,8 +7,8 @@ import IsingModel.Concrete.LatticeGraphBED.LatticeBoundaryBED
 Narrow child module for the 10 §18.3-§18.4 concrete Λ-level
 `partitionFunctionΛ_latticeGraph` `ratio_sandwich` / `ratio_bound`
 wrappers on `latticeGraph d` at `h = 0` (with `J = 0` / `β = 0` /
-`bundle` variants plus ferromagnetic counterparts). The 7
-`triple_ratio_*` wrappers now live in
+`bundle` variants plus ferromagnetic counterparts). The 4
+`triple_ratio_sandwich_bundle` wrappers now live in
 `HighTemperatureBoundsTripleRatio.lean` (narrowed in PR #1998); the
 12 `log_partitionFunctionΛ_latticeGraph` / `freeEnergyΛ_latticeGraph`
 ratio wrappers now live in `HighTemperatureBoundsRatioLogFe.lean`
@@ -142,12 +142,10 @@ unchanged.
 
 /-! ## Moved: ℤ^d Λ-direct triple-ratio wrappers
 
-The 7 ℤ^d Λ-direct `triple_ratio_sandwich_bundle` and
-`triple_ratio_bound_bundle` wrappers (J = 0 / β = 0 trivial slices,
-ferromagnetic variants) now live in
+The 4 ℤ^d Λ-direct `triple_ratio_sandwich_bundle` wrappers (J = 0 /
+β = 0 trivial slices, ferromagnetic variants) now live in
 `IsingModel.Concrete.LatticeGraphCorrelation.HighTemperatureBoundsTripleRatio`.
-The earlier import path is preserved by re-exporting the new child
-from the umbrella module that aggregates both.
+The earlier import path is preserved by re-importing the new child.
 -/
 
 end Ambient

IsingModel/Concrete/LatticeGraphCorrelation/HighTemperatureBoundsTripleRatio.lean

@@ -2,13 +2,12 @@ import IsingModel.Lattice
 import IsingModel.Concrete.LatticeGraphBED.LatticeBoundaryBED
 
 /-!
-# ℤ^d Λ-direct triple-ratio (Z + log Z + f) sandwich / bound wrappers at h = 0
+# ℤ^d Λ-direct triple-ratio (Z + log Z + f) sandwich wrappers at h = 0
 
-Narrow child module for 7 §18.3-§18.4 concrete (`latticeGraph d`)
-Λ-direct `triple_ratio_sandwich_bundle` and
-`triple_ratio_bound_bundle` wrappers (J = 0 trivial slice, β = 0
-specialisation, ferromagnetic variants). Theorem names are unchanged
-from the former
+Narrow child module for 4 §18.3-§18.4 concrete (`latticeGraph d`)
+Λ-direct `triple_ratio_sandwich_bundle` wrappers (J = 0 trivial slice,
+β = 0 specialisation, ferromagnetic variants). Theorem names are
+unchanged from the former
 `Concrete/LatticeGraphCorrelation/HighTemperatureBoundsRatioBounds`
 declarations.
 -/
@@ -198,15 +197,6 @@ theorem partitionFunctionΛ_latticeGraph_h_zero_triple_ratio_sandwich_bundle_fer
   partitionFunctionΛ_latticeGraph_high_temp_expansion_h_zero_triple_ratio_sandwich_bundle
     d Λ J β (mul_nonneg hβ.le hJ) hne
 
-/-! ## Moved: Λ-direct triple_ratio_bound_bundle wrappers
-
-The three `partitionFunctionΛ_*_triple_ratio_bound_bundle` wrappers
-(direct, `_beta_zero`, `_ferromagnetic`) now live in
-`HighTemperatureBoundsTripleRatioBoundBundle.lean`. -/
-
-
-
-
 end Ambient
 
 end IsingModel

IsingModel/Concrete/LatticeGraphCorrelation/Umbrella/HighTemperature.lean

@@ -69,7 +69,6 @@ import IsingModel.Concrete.LatticeGraphCorrelation.HighTemperatureBoundsRatioBou
 import IsingModel.Concrete.LatticeGraphCorrelation.HighTemperatureBoundsRatioLogFe
 import IsingModel.Concrete.LatticeGraphCorrelation.HighTemperatureBoundsRatioLogFeBound
 import IsingModel.Concrete.LatticeGraphCorrelation.HighTemperatureBoundsTripleRatio
-import IsingModel.Concrete.LatticeGraphCorrelation.HighTemperatureBoundsTripleRatioBoundBundle
 import IsingModel.Concrete.LatticeGraphCorrelation.HighTemperatureCapstones
 import IsingModel.Concrete.LatticeGraphCorrelation.HighTemperatureCapstonesAlongEx
 import IsingModel.Concrete.LatticeGraphCorrelation.HighTemperatureCapstonesAlongExFreeEnergy

scripts/test_dead_candidate_scan.py

@@ -894,37 +894,40 @@ class FamilyCalibrationTest(unittest.TestCase):
     """
 
     def test_ferromagnetic_family_counts(self) -> None:
-        """245 candidates -> 114 safe / 44 uncertain / 52 load-bearing / 35 published.
-
-        Recalibrated when the PR #4667 continuity/strict-deviation bundle cluster
-        deleted five safe-to-delete ``_ferromagnetic`` bundle wrappers
-        (``freeEnergyΛ{,_latticeGraph}_high_temp_h_zero_continuity_bundle_ferromagnetic``,
-        ``partitionFunctionΛ{,_latticeGraph}_high_temp_expansion_h_zero_strict_deviation_bundle_ferromagnetic``,
-        ``partitionFunctionAlongExhaustion_high_temp_expansion_h_zero_strict_deviation_bundle_ferromagnetic``):
-        total and safe both drop by 5, and the other three classes are
+        """241 candidates -> 110 safe / 44 uncertain / 52 load-bearing / 35 published.
+
+        Recalibrated when the PR #4669 triple_ratio_bound_bundle / sandwich cluster
+        deleted four safe-to-delete ``_ferromagnetic`` bundle wrappers
+        (``partitionFunctionΛ_high_temp_expansion_h_zero_triple_ratio_sandwich_bundle_ferromagnetic``,
+        ``partitionFunctionΛ_high_temp_expansion_h_zero_triple_ratio_sandwich_bundle_beta_zero_ferromagnetic``,
+        ``partitionFunctionΛ_high_temp_expansion_h_zero_triple_ratio_bound_bundle_ferromagnetic``,
+        ``partitionFunctionΛ_latticeGraph_high_temp_expansion_h_zero_triple_ratio_bound_bundle_ferromagnetic``):
+        total and safe both drop by 4, and the other three classes are
         unchanged -- the healthy signature that no live lemma was reclassified.
-        (Was 250 -> 119 safe after PR #4665 removed two ratio_bound_bundle wrappers.)
+        (Was 245 -> 114 safe after PR #4667 removed five continuity/strict-deviation
+        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), 245)
-        self.assertEqual(counts.get(dcs.SAFE), 114)
+        self.assertEqual(len(verdicts), 241)
+        self.assertEqual(counts.get(dcs.SAFE), 110)
         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:
-        """131 of the 245 have no Lean consumer at all.
-
-        Was 135 of 250 before the PR #4667 bundle cluster; of the five deleted
-        ``_ferromagnetic`` bundle wrappers four were themselves zero-consumer, while
-        ``freeEnergyΛ_high_temp_h_zero_continuity_bundle_ferromagnetic`` fed the
-        ``_latticeGraph`` continuity leaf (also deleted here), so the count drops by
-        four.
+        """128 of the 241 have no Lean consumer at all.
+
+        Was 131 of 245 before the PR #4669 triple_ratio_bound_bundle / sandwich
+        cluster; of the four deleted ``_ferromagnetic`` bundle wrappers three were
+        themselves zero-consumer, while
+        ``partitionFunctionΛ_high_temp_expansion_h_zero_triple_ratio_bound_bundle_ferromagnetic``
+        fed the ``_latticeGraph`` bound-bundle leaf (also deleted here), so the count
+        drops by three.
         """
-        self.assertEqual(sum(1 for v in family_verdicts() if not v.consumers), 131)
+        self.assertEqual(sum(1 for v in family_verdicts() if not v.consumers), 128)
 
 
 class CanaryTest(unittest.TestCase):