refactor: remove 97 dead decoration lemmas + 2 unused imports (2026-07-17 tier2 cycle)

IsingModel/AmbientLattice/CorrelationInfinite/Bounds.lean

@@ -85,16 +85,6 @@ theorem correlationInfinite_lt_two
   have h := correlationInfinite_le_one G Λ p A
   linarith
 
-/-- **`correlationInfinite ∈ Icc (-1) 1`** (unconditional): combines
-`abs_correlationInfinite_le_one` lower and upper sides. -/
-theorem correlationInfinite_mem_Icc_neg_one_one
-    (G : SimpleGraph V) (Λ : Exhaustion V)
-    [∀ n, Fintype (inducedGraph G (Λ.volume n)).edgeSet]
-    (p : IsingParams ℝ) (A : Finset V) :
-    correlationInfinite G Λ p A ∈ Set.Icc (-1 : ℝ) 1 :=
-  ⟨neg_one_le_correlationInfinite G Λ p A,
-   correlationInfinite_le_one G Λ p A⟩
-
 /-- **Nonnegativity** (ferromagnetic): `correlationInfinite ≥ 0`.
 Uses `Λ.exhaust`: pick `N` with `A ⊆ Λ.volume N`; then
 `correlationAlongExhaustion G Λ p A N ≥ 0` by GKS-I, and this is
@@ -112,36 +102,6 @@ theorem correlationInfinite_nonneg
     exact correlationΛ_nonneg G (Λ.volume N) p hf _
   exact hval.trans (le_ciSup (correlationAlongExhaustion_bddAbove G Λ p A) N)
 
-/-- **`correlationInfinite ∈ Icc 0 1`** under ferromagnetic: combines
-`correlationInfinite_nonneg` and `correlationInfinite_le_one`. -/
-theorem correlationInfinite_mem_Icc_zero_one
-    (G : SimpleGraph V) (Λ : Exhaustion V)
-    [∀ n, Fintype (inducedGraph G (Λ.volume n)).edgeSet]
-    (p : IsingParams ℝ) (hf : Ferromagnetic p) (A : Finset V) :
-    correlationInfinite G Λ p A ∈ Set.Icc (0 : ℝ) 1 :=
-  ⟨correlationInfinite_nonneg G Λ p hf A,
-   correlationInfinite_le_one G Λ p A⟩
-
-/-- **`correlationInfinite ∈ Icc 0 2`** under ferromagnetic: combines
-`correlationInfinite_nonneg` and `correlationInfinite_le_one ≤ 2`. -/
-theorem correlationInfinite_mem_Icc_zero_two
-    (G : SimpleGraph V) (Λ : Exhaustion V)
-    [∀ n, Fintype (inducedGraph G (Λ.volume n)).edgeSet]
-    (p : IsingParams ℝ) (hf : Ferromagnetic p) (A : Finset V) :
-    correlationInfinite G Λ p A ∈ Set.Icc (0 : ℝ) 2 := by
-  have h := correlationInfinite_le_one G Λ p A
-  refine ⟨correlationInfinite_nonneg G Λ p hf A, ?_⟩
-  linarith
-
-/-- **`correlationInfinite ∈ Ioc 0 1`** when positive under ferromagnetic. -/
-theorem correlationInfinite_mem_Ioc_zero_one_of_pos
-    (G : SimpleGraph V) (Λ : Exhaustion V)
-    [∀ n, Fintype (inducedGraph G (Λ.volume n)).edgeSet]
-    (p : IsingParams ℝ) (_hf : Ferromagnetic p) (A : Finset V)
-    (hpos : 0 < correlationInfinite G Λ p A) :
-    correlationInfinite G Λ p A ∈ Set.Ioc (0 : ℝ) 1 :=
-  ⟨hpos, correlationInfinite_le_one G Λ p A⟩
-
 /-- **`correlationInfinite ∈ Ioo 0 2`** when positive under ferromagnetic. -/
 theorem correlationInfinite_mem_Ioo_zero_two_of_pos
     (G : SimpleGraph V) (Λ : Exhaustion V)
@@ -151,85 +111,5 @@ theorem correlationInfinite_mem_Ioo_zero_two_of_pos
     correlationInfinite G Λ p A ∈ Set.Ioo (0 : ℝ) 2 :=
   ⟨hpos, correlationInfinite_lt_two G Λ p A⟩
 
-/-- **`correlationInfinite ∈ Ico 0 2`** under ferromagnetic. -/
-theorem correlationInfinite_mem_Ico_zero_two
-    (G : SimpleGraph V) (Λ : Exhaustion V)
-    [∀ n, Fintype (inducedGraph G (Λ.volume n)).edgeSet]
-    (p : IsingParams ℝ) (hf : Ferromagnetic p) (A : Finset V) :
-    correlationInfinite G Λ p A ∈ Set.Ico (0 : ℝ) 2 :=
-  ⟨correlationInfinite_nonneg G Λ p hf A,
-   correlationInfinite_lt_two G Λ p A⟩
-
-/-- **`correlationInfinite ∈ Iio 2`** (unconditional). -/
-theorem correlationInfinite_mem_Iio_two
-    (G : SimpleGraph V) (Λ : Exhaustion V)
-    [∀ n, Fintype (inducedGraph G (Λ.volume n)).edgeSet]
-    (p : IsingParams ℝ) (A : Finset V) :
-    correlationInfinite G Λ p A ∈ Set.Iio (2 : ℝ) :=
-  correlationInfinite_lt_two G Λ p A
-
-/-- **`correlationInfinite ∈ Iic 1`** (unconditional). -/
-theorem correlationInfinite_mem_Iic_one
-    (G : SimpleGraph V) (Λ : Exhaustion V)
-    [∀ n, Fintype (inducedGraph G (Λ.volume n)).edgeSet]
-    (p : IsingParams ℝ) (A : Finset V) :
-    correlationInfinite G Λ p A ∈ Set.Iic (1 : ℝ) :=
-  correlationInfinite_le_one G Λ p A
-
-/-- **`correlationInfinite ∈ Ici 0`** under ferromagnetic. -/
-theorem correlationInfinite_mem_Ici_zero
-    (G : SimpleGraph V) (Λ : Exhaustion V)
-    [∀ n, Fintype (inducedGraph G (Λ.volume n)).edgeSet]
-    (p : IsingParams ℝ) (hf : Ferromagnetic p) (A : Finset V) :
-    correlationInfinite G Λ p A ∈ Set.Ici (0 : ℝ) :=
-  correlationInfinite_nonneg G Λ p hf A
-
-/-- **`correlationInfinite ∉ Iio 0`** under ferromagnetic. -/
-theorem correlationInfinite_not_mem_Iio_zero
-    (G : SimpleGraph V) (Λ : Exhaustion V)
-    [∀ n, Fintype (inducedGraph G (Λ.volume n)).edgeSet]
-    (p : IsingParams ℝ) (hf : Ferromagnetic p) (A : Finset V) :
-    correlationInfinite G Λ p A ∉ Set.Iio (0 : ℝ) :=
-  not_lt.mpr (correlationInfinite_nonneg G Λ p hf A)
-
-/-- **`correlationInfinite ∉ Ioi 1`** (unconditional): direct from
-`correlationInfinite_le_one`. -/
-theorem correlationInfinite_not_mem_Ioi_one
-    (G : SimpleGraph V) (Λ : Exhaustion V)
-    [∀ n, Fintype (inducedGraph G (Λ.volume n)).edgeSet]
-    (p : IsingParams ℝ) (A : Finset V) :
-    correlationInfinite G Λ p A ∉ Set.Ioi (1 : ℝ) :=
-  not_lt.mpr (correlationInfinite_le_one G Λ p A)
-
-/-- **`0 < correlationInfinite ↔ correlationInfinite ≠ 0`** under
-ferromagnetic: standard nonneg → pos iff ne_zero pattern. -/
-theorem correlationInfinite_pos_iff_ne_zero
-    (G : SimpleGraph V) (Λ : Exhaustion V)
-    [∀ n, Fintype (inducedGraph G (Λ.volume n)).edgeSet]
-    (p : IsingParams ℝ) (hf : Ferromagnetic p) (A : Finset V) :
-    0 < correlationInfinite G Λ p A ↔ correlationInfinite G Λ p A ≠ 0 :=
-  (correlationInfinite_nonneg G Λ p hf A).lt_iff_ne.trans
-    ⟨fun h => h.symm, fun h => h.symm⟩
-
-/-- **`correlationInfinite ≤ 0 ↔ correlationInfinite = 0`** under
-ferromagnetic: combines nonneg with antisymmetry. -/
-theorem correlationInfinite_le_zero_iff_eq_zero
-    (G : SimpleGraph V) (Λ : Exhaustion V)
-    [∀ n, Fintype (inducedGraph G (Λ.volume n)).edgeSet]
-    (p : IsingParams ℝ) (hf : Ferromagnetic p) (A : Finset V) :
-    correlationInfinite G Λ p A ≤ 0 ↔ correlationInfinite G Λ p A = 0 := by
-  refine ⟨?_, fun h => le_of_eq h⟩
-  intro hle
-  exact le_antisymm hle (correlationInfinite_nonneg G Λ p hf A)
-
-/-- **`¬(correlationInfinite < 0)`** under ferromagnetic: direct
-from `correlationInfinite_nonneg`. -/
-theorem correlationInfinite_not_lt_zero
-    (G : SimpleGraph V) (Λ : Exhaustion V)
-    [∀ n, Fintype (inducedGraph G (Λ.volume n)).edgeSet]
-    (p : IsingParams ℝ) (hf : Ferromagnetic p) (A : Finset V) :
-    ¬ (correlationInfinite G Λ p A < 0) :=
-  not_lt.mpr (correlationInfinite_nonneg G Λ p hf A)
-
 end Ambient
 end IsingModel

IsingModel/AmbientLattice/MagnetizationAlongExhaustion.lean

@@ -129,17 +129,6 @@ noncomputable def susceptibilityAlongExhaustion
     susceptibilityΛ G (Λ.volume n) p ⟨i, h⟩
   else 0
 
-/-- **Unfolding of `susceptibilityAlongExhaustion`**: by definition the
-stagewise value is the dependent `if`-expression over membership. -/
-theorem susceptibilityAlongExhaustion_apply
-    (G : SimpleGraph V) (Λ : Exhaustion V)
-    [∀ n, Fintype (inducedGraph G (Λ.volume n)).edgeSet]
-    (p : IsingParams ℝ) (i : V) (n : ℕ) :
-    susceptibilityAlongExhaustion G Λ p i n
-      = if h : i ∈ Λ.volume n then
-          susceptibilityΛ G (Λ.volume n) p ⟨i, h⟩
-        else 0 := rfl
-
 /-- **Unfolding of `susceptibilityAlongExhaustion` when `i ∈ Λ.volume n`**:
 the stagewise value equals `susceptibilityΛ` at the lifted subtype site. -/
 theorem susceptibilityAlongExhaustion_of_mem

IsingModel/AmbientLattice/MagnetizationInfiniteSusceptibility.lean

@@ -54,17 +54,6 @@ theorem susceptibilityInfinite_eq_ciSup
     susceptibilityInfinite G Λ p i
       = ⨆ n, susceptibilityAlongExhaustion G Λ p i n := rfl
 
-/-- **Unfolding of `susceptibilityInfinite`**:
-`susceptibilityInfinite G Λ p i = ⨆ n, susceptibilityAlongExhaustion G Λ p i n`,
-by definition. (Alias of `susceptibilityInfinite_eq_ciSup` for uniformity
-with `magnetizationInfinite_apply`.) -/
-theorem susceptibilityInfinite_apply
-    (G : SimpleGraph V) (Λ : Exhaustion V)
-    [∀ n, Fintype (inducedGraph G (Λ.volume n)).edgeSet]
-    (p : IsingParams ℝ) (i : V) :
-    susceptibilityInfinite G Λ p i
-      = ⨆ n, susceptibilityAlongExhaustion G Λ p i n := rfl
-
 /-- **Nonnegativity of `susceptibilityInfinite`** under ferromagnetism:
 `0 ≤ susceptibilityInfinite G Λ p i`.
 

IsingModel/AmbientLattice/SpontaneousMagnetization.lean

@@ -210,15 +210,6 @@ noncomputable def spontaneousMagnetization
     (J β : ℝ) (i : V) : ℝ :=
   spontaneousCorrelation G Λ J β {i}
 
-/-- **Unfolding of `spontaneousMagnetization`**:
-`spontaneousMagnetization G Λ J β i = spontaneousCorrelation G Λ J β {i}`. -/
-theorem spontaneousMagnetization_apply
-    (G : SimpleGraph V) (Λ : Exhaustion V)
-    [∀ n, Fintype (inducedGraph G (Λ.volume n)).edgeSet]
-    (J β : ℝ) (i : V) :
-    spontaneousMagnetization G Λ J β i = spontaneousCorrelation G Λ J β {i} :=
-  rfl
-
 /-- **Agreement at singletons**: `spontaneousCorrelation` on `{i}`
 equals `spontaneousMagnetization`. Holds by definition. -/
 theorem spontaneousCorrelation_singleton_eq_spontaneousMagnetization

IsingModel/AmbientLattice/TruncatedFunctions/TwoPoint.lean

@@ -245,138 +245,6 @@ theorem truncated2Infinite_sq_le_one
     pow_le_pow_left₀ (abs_nonneg _) h 2
   simpa [sq_abs] using this
 
-/-- **`truncated2Infinite < 2`** for ferromagnetic `p`: direct from
-`truncated2Infinite ≤ 1 < 2`. Useful for `Ioo 0 2` membership when
-combining with strict positivity. -/
-theorem truncated2Infinite_lt_two
-    (G : SimpleGraph V) (Λ : Exhaustion V)
-    [∀ n, Fintype (inducedGraph G (Λ.volume n)).edgeSet]
-    (p : IsingParams ℝ) (hf : Ferromagnetic p) (i j : V) :
-    truncated2Infinite G Λ p i j < 2 := by
-  have h := truncated2Infinite_le_one G Λ p hf i j
-  linarith
-
-/-- **`truncated2Infinite ∈ Ioo 0 2`** when `0 < truncated2`** under
-ferromagnetic: combines `_lt_two` (PR #1728 candidate) with the
-strict positivity hypothesis. -/
-theorem truncated2Infinite_mem_Ioo_zero_two_of_pos
-    (G : SimpleGraph V) (Λ : Exhaustion V)
-    [∀ n, Fintype (inducedGraph G (Λ.volume n)).edgeSet]
-    (p : IsingParams ℝ) (hf : Ferromagnetic p) (i j : V)
-    (hpos : 0 < truncated2Infinite G Λ p i j) :
-    truncated2Infinite G Λ p i j ∈ Set.Ioo (0 : ℝ) 2 :=
-  ⟨hpos, truncated2Infinite_lt_two G Λ p hf i j⟩
-
-/-- **`truncated2Infinite ∈ Icc 0 1`** for ferromagnetic `p`: combines
-`truncated2Infinite_nonneg` and `truncated2Infinite_le_one`. -/
-theorem truncated2Infinite_mem_Icc_zero_one
-    (G : SimpleGraph V) (Λ : Exhaustion V)
-    [∀ n, Fintype (inducedGraph G (Λ.volume n)).edgeSet]
-    (p : IsingParams ℝ) (hf : Ferromagnetic p) (i j : V) :
-    truncated2Infinite G Λ p i j ∈ Set.Icc (0 : ℝ) 1 :=
-  ⟨truncated2Infinite_nonneg G Λ p hf i j,
-   truncated2Infinite_le_one G Λ p hf i j⟩
-
-/-- **`truncated2Infinite ∈ Ioc 0 1`** when `0 < truncated2` under
-ferromagnetic: strict positivity + ≤ 1. -/
-theorem truncated2Infinite_mem_Ioc_zero_one_of_pos
-    (G : SimpleGraph V) (Λ : Exhaustion V)
-    [∀ n, Fintype (inducedGraph G (Λ.volume n)).edgeSet]
-    (p : IsingParams ℝ) (hf : Ferromagnetic p) (i j : V)
-    (hpos : 0 < truncated2Infinite G Λ p i j) :
-    truncated2Infinite G Λ p i j ∈ Set.Ioc (0 : ℝ) 1 :=
-  ⟨hpos, truncated2Infinite_le_one G Λ p hf i j⟩
-
-/-- **`truncated2Infinite ∈ Ico 0 2`** under ferromagnetic. -/
-theorem truncated2Infinite_mem_Ico_zero_two
-    (G : SimpleGraph V) (Λ : Exhaustion V)
-    [∀ n, Fintype (inducedGraph G (Λ.volume n)).edgeSet]
-    (p : IsingParams ℝ) (hf : Ferromagnetic p) (i j : V) :
-    truncated2Infinite G Λ p i j ∈ Set.Ico (0 : ℝ) 2 :=
-  ⟨truncated2Infinite_nonneg G Λ p hf i j,
-   truncated2Infinite_lt_two G Λ p hf i j⟩
-
-/-- **`truncated2Infinite ∈ Iio 2`** under ferromagnetic. -/
-theorem truncated2Infinite_mem_Iio_two
-    (G : SimpleGraph V) (Λ : Exhaustion V)
-    [∀ n, Fintype (inducedGraph G (Λ.volume n)).edgeSet]
-    (p : IsingParams ℝ) (hf : Ferromagnetic p) (i j : V) :
-    truncated2Infinite G Λ p i j ∈ Set.Iio (2 : ℝ) :=
-  truncated2Infinite_lt_two G Λ p hf i j
-
-/-- **`truncated2Infinite ∈ Iic 1`** under ferromagnetic. -/
-theorem truncated2Infinite_mem_Iic_one
-    (G : SimpleGraph V) (Λ : Exhaustion V)
-    [∀ n, Fintype (inducedGraph G (Λ.volume n)).edgeSet]
-    (p : IsingParams ℝ) (hf : Ferromagnetic p) (i j : V) :
-    truncated2Infinite G Λ p i j ∈ Set.Iic (1 : ℝ) :=
-  truncated2Infinite_le_one G Λ p hf i j
-
-/-- **`truncated2Infinite ∈ Ici 0`** under ferromagnetic. -/
-theorem truncated2Infinite_mem_Ici_zero
-    (G : SimpleGraph V) (Λ : Exhaustion V)
-    [∀ n, Fintype (inducedGraph G (Λ.volume n)).edgeSet]
-    (p : IsingParams ℝ) (hf : Ferromagnetic p) (i j : V) :
-    truncated2Infinite G Λ p i j ∈ Set.Ici (0 : ℝ) :=
-  truncated2Infinite_nonneg G Λ p hf i j
-
-/-- **`truncated2Infinite ∉ Iio 0`** under ferromagnetic. -/
-theorem truncated2Infinite_not_mem_Iio_zero
-    (G : SimpleGraph V) (Λ : Exhaustion V)
-    [∀ n, Fintype (inducedGraph G (Λ.volume n)).edgeSet]
-    (p : IsingParams ℝ) (hf : Ferromagnetic p) (i j : V) :
-    truncated2Infinite G Λ p i j ∉ Set.Iio (0 : ℝ) :=
-  not_lt.mpr (truncated2Infinite_nonneg G Λ p hf i j)
-
-/-- **`truncated2Infinite ∉ Ioi 1`** under ferromagnetic. -/
-theorem truncated2Infinite_not_mem_Ioi_one
-    (G : SimpleGraph V) (Λ : Exhaustion V)
-    [∀ n, Fintype (inducedGraph G (Λ.volume n)).edgeSet]
-    (p : IsingParams ℝ) (hf : Ferromagnetic p) (i j : V) :
-    truncated2Infinite G Λ p i j ∉ Set.Ioi (1 : ℝ) :=
-  not_lt.mpr (truncated2Infinite_le_one G Λ p hf i j)
-
-/-- **`truncated2Infinite ∉ Ioi 2`** under ferromagnetic: stronger than
-`_lt_two`. -/
-theorem truncated2Infinite_not_mem_Ioi_two
-    (G : SimpleGraph V) (Λ : Exhaustion V)
-    [∀ n, Fintype (inducedGraph G (Λ.volume n)).edgeSet]
-    (p : IsingParams ℝ) (hf : Ferromagnetic p) (i j : V) :
-    truncated2Infinite G Λ p i j ∉ Set.Ioi (2 : ℝ) := by
-  intro h_lt
-  rw [Set.mem_Ioi] at h_lt
-  have h := truncated2Infinite_le_one G Λ p hf i j
-  linarith
-
-/-- **`0 < truncated2Infinite ↔ truncated2Infinite ≠ 0`** under
-ferromagnetic: standard nonneg → pos iff ne_zero pattern. -/
-theorem truncated2Infinite_pos_iff_ne_zero
-    (G : SimpleGraph V) (Λ : Exhaustion V)
-    [∀ n, Fintype (inducedGraph G (Λ.volume n)).edgeSet]
-    (p : IsingParams ℝ) (hf : Ferromagnetic p) (i j : V) :
-    0 < truncated2Infinite G Λ p i j ↔ truncated2Infinite G Λ p i j ≠ 0 :=
-  (truncated2Infinite_nonneg G Λ p hf i j).lt_iff_ne.trans
-    ⟨fun h => h.symm, fun h => h.symm⟩
-
-/-- **`truncated2Infinite ≤ 0 ↔ truncated2Infinite = 0`** under
-ferromagnetic: combines nonneg with antisymmetry. -/
-theorem truncated2Infinite_le_zero_iff_eq_zero
-    (G : SimpleGraph V) (Λ : Exhaustion V)
-    [∀ n, Fintype (inducedGraph G (Λ.volume n)).edgeSet]
-    (p : IsingParams ℝ) (hf : Ferromagnetic p) (i j : V) :
-    truncated2Infinite G Λ p i j ≤ 0 ↔ truncated2Infinite G Λ p i j = 0 := by
-  refine ⟨?_, fun h => le_of_eq h⟩
-  intro hle
-  exact le_antisymm hle (truncated2Infinite_nonneg G Λ p hf i j)
-
-/-- **`¬(truncated2Infinite < 0)`** under ferromagnetic. -/
-theorem truncated2Infinite_not_lt_zero
-    (G : SimpleGraph V) (Λ : Exhaustion V)
-    [∀ n, Fintype (inducedGraph G (Λ.volume n)).edgeSet]
-    (p : IsingParams ℝ) (hf : Ferromagnetic p) (i j : V) :
-    ¬ (truncated2Infinite G Λ p i j < 0) :=
-  not_lt.mpr (truncated2Infinite_nonneg G Λ p hf i j)
-
 /-- **Exhaustion-independence of `truncated2Infinite`**: the value
 does not depend on the choice of exhaustion.  Follows from
 `correlationInfinite_indep_exhaustion` applied to each of the three