refactor: drop the correlationΛ pair-singleton bundle cluster

IsingModel/AmbientLattice/Defs/HighTempCorrelation.lean

@@ -346,70 +346,6 @@ theorem correlationΛ_high_temp_h_zero_at_singleton_eq_zero_le_one
   ⟨correlationΛ_high_temp_h_zero_at_singleton G Λ J β i,
    (correlationΛ_high_temp_h_zero_at_singleton G Λ J β i).symm ▸ zero_le_one⟩
 
-/-- **Λ pair+singleton bundle at h=0**: combines pair sandwich and
-singleton vanishing. -/
-theorem correlationΛ_high_temp_h_zero_at_pair_singleton_bundle
-    (G : SimpleGraph V) (Λ : Finset V)
-    [Fintype (inducedGraph G Λ).edgeSet]
-    (J β : ℝ) (hβJ : 0 ≤ β * J) (i j : ↑Λ) :
-    correlationΛ G Λ (⟨J, 0, β⟩ : IsingParams ℝ) ({i} : Finset ↑Λ) = 0 ∧
-      0 ≤ correlationΛ G Λ (⟨J, 0, β⟩ : IsingParams ℝ) ({i, j} : Finset ↑Λ) ∧
-      correlationΛ G Λ (⟨J, 0, β⟩ : IsingParams ℝ) ({i, j} : Finset ↑Λ) ≤ 1 :=
-  ⟨correlationΛ_high_temp_h_zero_at_singleton G Λ J β i,
-   correlationΛ_high_temp_h_zero_at_pair_nonneg G Λ J β hβJ i j,
-   correlationΛ_high_temp_h_zero_at_pair_le_one G Λ J β i j⟩
-
-/-- **Λ pair+singleton bundle under ferromagnetic at h = 0**: under
-`0 ≤ J, 0 < β`, packages `⟨σ_i⟩^Λ = 0`, `0 ≤ ⟨σ_iσ_j⟩^Λ`, and
-`⟨σ_iσ_j⟩^Λ ≤ 1` into a single triple. Λ-layer wrapper of
-`correlation_high_temp_h_zero_at_pair_singleton_bundle_ferromagnetic`. -/
-theorem correlationΛ_high_temp_h_zero_at_pair_singleton_bundle_ferromagnetic
-    (G : SimpleGraph V) (Λ : Finset V)
-    [Fintype (inducedGraph G Λ).edgeSet]
-    (J β : ℝ) (hJ : 0 ≤ J) (hβ : 0 < β) (i j : ↑Λ) :
-    correlationΛ G Λ (⟨J, 0, β⟩ : IsingParams ℝ) ({i} : Finset ↑Λ) = 0 ∧
-      0 ≤ correlationΛ G Λ (⟨J, 0, β⟩ : IsingParams ℝ) ({i, j} : Finset ↑Λ) ∧
-      correlationΛ G Λ (⟨J, 0, β⟩ : IsingParams ℝ) ({i, j} : Finset ↑Λ) ≤ 1 :=
-  correlationΛ_high_temp_h_zero_at_pair_singleton_bundle G Λ J β
-    (mul_nonneg hβ.le hJ) i j
-
-/-- **Λ pair + singleton complete-summary bundle at h = 0**: under
-`0 ≤ β·J`, single statement bundling pair upper bound, pair sandwich
-lower, singleton vanishing, and pair vanishing at `J = 0` / `β = 0`
-trivial slices. Λ-layer wrapper of
-`correlation_high_temp_h_zero_at_pair_singleton_complete_summary`. -/
-theorem correlationΛ_high_temp_h_zero_at_pair_singleton_complete_summary
-    (G : SimpleGraph V) (Λ : Finset V)
-    [Fintype (inducedGraph G Λ).edgeSet]
-    (J β : ℝ) (hβJ : 0 ≤ β * J) (i j : ↑Λ) :
-    correlationΛ G Λ (⟨J, 0, β⟩ : IsingParams ℝ) ({i, j} : Finset ↑Λ) ≤ 1 ∧
-      0 ≤ correlationΛ G Λ (⟨J, 0, β⟩ : IsingParams ℝ) ({i, j} : Finset ↑Λ) ∧
-      correlationΛ G Λ (⟨J, 0, β⟩ : IsingParams ℝ) ({i} : Finset ↑Λ) = 0 ∧
-      correlationΛ G Λ (⟨0, 0, β⟩ : IsingParams ℝ) ({i, j} : Finset ↑Λ) = 0 ∧
-      correlationΛ G Λ (⟨J, 0, 0⟩ : IsingParams ℝ) ({i, j} : Finset ↑Λ) = 0 :=
-  ⟨correlationΛ_high_temp_h_zero_at_pair_le_one G Λ J β i j,
-   correlationΛ_high_temp_h_zero_at_pair_nonneg G Λ J β hβJ i j,
-   correlationΛ_high_temp_h_zero_at_singleton G Λ J β i,
-   correlationΛ_high_temp_h_zero_at_pair_J_zero G Λ β i j,
-   correlationΛ_high_temp_h_zero_at_pair_beta_zero G Λ J i j⟩
-
-/-- **Λ pair + singleton trivial-slices full bundle at h = 0**:
-at `J = 0` and `β = 0`, both Λ-pair and Λ-singleton correlations vanish.
-Λ-layer wrapper of
-`correlation_high_temp_h_zero_at_pair_singleton_trivial_slices_bundle`. -/
-theorem correlationΛ_high_temp_h_zero_at_pair_singleton_trivial_slices_bundle
-    (G : SimpleGraph V) (Λ : Finset V)
-    [Fintype (inducedGraph G Λ).edgeSet]
-    (J β : ℝ) (i j : ↑Λ) :
-    correlationΛ G Λ (⟨0, 0, β⟩ : IsingParams ℝ) ({i} : Finset ↑Λ) = 0 ∧
-      correlationΛ G Λ (⟨J, 0, 0⟩ : IsingParams ℝ) ({i} : Finset ↑Λ) = 0 ∧
-      correlationΛ G Λ (⟨0, 0, β⟩ : IsingParams ℝ) ({i, j} : Finset ↑Λ) = 0 ∧
-      correlationΛ G Λ (⟨J, 0, 0⟩ : IsingParams ℝ) ({i, j} : Finset ↑Λ) = 0 :=
-  ⟨correlationΛ_high_temp_h_zero_at_singleton_J_zero G Λ β i,
-   correlationΛ_high_temp_h_zero_at_singleton_beta_zero G Λ J i,
-   correlationΛ_high_temp_h_zero_at_pair_J_zero G Λ β i j,
-   correlationΛ_high_temp_h_zero_at_pair_beta_zero G Λ J i j⟩
-
 /-- **Λ pair correlation single-edge tanh lower bound (GJ §18.3 / FV (3.46))**:
 under `0 ≤ β·J` and an edge `s(i, j) ∈ (inducedGraph G Λ).edgeSet`,
 `⟨σ_iσ_j⟩^Λ ≥ tanh(β·J) / 2^|E_Λ|` where `i, j : ↑Λ`. Λ-layer wrapper

IsingModel/Concrete/LatticeGraphCorrelation/HighTemperatureBounds.lean

@@ -87,22 +87,12 @@ theorem freeEnergyΛ_latticeGraph_high_temp_h_zero_sandwich
 The §18.3-§18.4 concrete `correlationΛ_latticeGraph` basic high-temperature
 wrappers at `h = 0` (pair nonneg, pair `≤ 1`, singleton / pair trivial-slice
 vanishings at `J = 0` and `β = 0`, pair sandwich, singleton / pair
-ferromagnetic, singleton `= 0 ∧ ≤ 1`, pair+singleton bundle) now live in
+ferromagnetic, singleton `= 0 ∧ ≤ 1`) now live in
 `IsingModel.Concrete.LatticeGraphCorrelation.HighTemperatureBoundsCorrelationBasic`.
 The earlier import path is preserved by re-importing the new child.
 -/
 
 
-/-! ## Moved: ℤ^d HT pair+singleton bundle wrappers
-
-The 3 ℤ^d
-`correlationΛ_latticeGraph_high_temp_h_zero_at_pair_singleton_*`
-bundle wrappers (`_bundle_ferromagnetic`, `_complete_summary`,
-`_trivial_slices_bundle`) now live in
-`IsingModel.Concrete.LatticeGraphCorrelation.HighTemperatureBoundsPairSingletonBundle`.
-The earlier import path is preserved by re-importing the new child.
--/
-
 /-! ## Moved: §18.7 high-temperature exponential decay capstones
 
 The §18.7 high-temperature pair-correlation exponential-decay capstone

IsingModel/Concrete/LatticeGraphCorrelation/HighTemperatureBoundsCorrelationBasic.lean

@@ -7,9 +7,9 @@ import IsingModel.Concrete.LatticeGraphBED.LatticeBoundaryBED
 Narrow child module for the §18.3-§18.4 concrete `correlationΛ_latticeGraph`
 basic high-temperature wrappers at `h = 0`: pair nonneg, pair `≤ 1`,
 singleton / pair trivial-slice vanishings at `J = 0` and `β = 0`, pair
-sandwich, singleton / pair ferromagnetic, singleton `= 0 ∧ ≤ 1`, and the
-pair+singleton bundle. Bundle / single-edge-bound / capstone / §18.7
-exponential-decay wrappers remain in the parent `HighTemperatureBounds`.
+sandwich, singleton / pair ferromagnetic, and singleton `= 0 ∧ ≤ 1`.
+Bundle / single-edge-bound / capstone / §18.7 exponential-decay wrappers
+remain in the parent `HighTemperatureBounds`.
 The theorem names are unchanged from the former `HighTemperatureBounds`
 declarations.
 -/
@@ -47,9 +47,9 @@ trivial-slice wrappers (singleton/pair at J = 0 and β = 0) now live in
 
 /-! ## Moved: pair sandwich / ferromagnetic / bundle wrappers
 
-The five `correlationΛ_latticeGraph_high_temp_h_zero_*` wrappers
+The four `correlationΛ_latticeGraph_high_temp_h_zero_*` wrappers
 (`pair_sandwich`, `singleton_ferromagnetic`, `pair_ferromagnetic`,
-`singleton_eq_zero_le_one`, `pair_singleton_bundle`) now live in
+`singleton_eq_zero_le_one`) now live in
 `HighTemperatureBoundsCorrelationBasicBundles.lean`. -/
 
 

IsingModel/Concrete/LatticeGraphCorrelation/HighTemperatureBoundsCorrelationBasicBundles.lean

@@ -3,15 +3,14 @@ import IsingModel.Concrete.LatticeGraphBED.LatticeBoundaryBED
 /-!
 # ℤ^d Λ-induced high-temperature h=0 sandwich / ferromagnetic / bundle wrappers
 
-Narrow child module for five ℤ^d Λ-induced
+Narrow child module for four ℤ^d Λ-induced
 `correlationΛ_latticeGraph_high_temp_h_zero_*` wrappers extracted from
 `HighTemperatureBoundsCorrelationBasic.lean`:
 
 * `_at_pair_sandwich`,
 * `_at_singleton_ferromagnetic`,
 * `_at_pair_ferromagnetic`,
-* `_at_singleton_eq_zero_le_one`,
-* `_at_pair_singleton_bundle`.
+* `_at_singleton_eq_zero_le_one`.
 -/
 
 namespace IsingModel
@@ -58,19 +57,5 @@ theorem correlationΛ_latticeGraph_high_temp_h_zero_at_singleton_eq_zero_le_one
   correlationΛ_high_temp_h_zero_at_singleton_eq_zero_le_one
     (IsingModel.latticeGraph d) Λ J β i
 
-/-- **ℤ^d Λ pair+singleton bundle at h=0**: combines pair sandwich and
-singleton vanishing. -/
-theorem correlationΛ_latticeGraph_high_temp_h_zero_at_pair_singleton_bundle
-    (d : ℕ) (Λ : Finset (Fin d → ℤ)) (J β : ℝ)
-    (hβJ : 0 ≤ β * J) (i j : ↑Λ) :
-    correlationΛ (IsingModel.latticeGraph d) Λ
-        (⟨J, 0, β⟩ : IsingParams ℝ) ({i} : Finset ↑Λ) = 0 ∧
-      0 ≤ correlationΛ (IsingModel.latticeGraph d) Λ
-          (⟨J, 0, β⟩ : IsingParams ℝ) ({i, j} : Finset ↑Λ) ∧
-      correlationΛ (IsingModel.latticeGraph d) Λ
-          (⟨J, 0, β⟩ : IsingParams ℝ) ({i, j} : Finset ↑Λ) ≤ 1 :=
-  correlationΛ_high_temp_h_zero_at_pair_singleton_bundle
-    (IsingModel.latticeGraph d) Λ J β hβJ i j
-
 end Ambient
 end IsingModel

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.HighTemperatureBoundsPairSingletonBundle
 import IsingModel.Concrete.LatticeGraphCorrelation.HighTemperatureBoundsRatioBoundBundle
 import IsingModel.Concrete.LatticeGraphCorrelation.HighTemperatureBoundsRatioBounds
 import IsingModel.Concrete.LatticeGraphCorrelation.HighTemperatureBoundsRatioBoundsBound

scripts/test_dead_candidate_scan.py

@@ -894,20 +894,30 @@ class FamilyCalibrationTest(unittest.TestCase):
     """
 
     def test_ferromagnetic_family_counts(self) -> None:
-        """261 candidates -> 130 safe / 44 uncertain / 52 load-bearing / 35 published."""
+        """259 candidates -> 128 safe / 44 uncertain / 52 load-bearing / 35 published.
+
+        Recalibrated when PR #4659 deleted the two safe-to-delete
+        ``correlationΛ*_high_temp_h_zero_at_pair_singleton_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.
+        """
         verdicts = family_verdicts()
         counts: dict[str, int] = {}
         for verdict in verdicts:
             counts[verdict.verdict] = counts.get(verdict.verdict, 0) + 1
-        self.assertEqual(len(verdicts), 261)
-        self.assertEqual(counts.get(dcs.SAFE), 130)
+        self.assertEqual(len(verdicts), 259)
+        self.assertEqual(counts.get(dcs.SAFE), 128)
         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:
-        """142 of the 261 have no Lean consumer at all."""
-        self.assertEqual(sum(1 for v in family_verdicts() if not v.consumers), 142)
+        """141 of the 259 have no Lean consumer at all.
+
+        Was 142 of 261 before PR #4659; the deleted ``_latticeGraph_`` bundle
+        ferromagnetic wrapper was itself zero-consumer, so the count drops by one.
+        """
+        self.assertEqual(sum(1 for v in family_verdicts() if not v.consumers), 141)
 
 
 class CanaryTest(unittest.TestCase):