refactor(AmbientLattice): first-order correlationAlongExhaustion family equations and magnetization twin retirement

IsingModel/AmbientLattice/BetaDerivativeMagnetization.lean

@@ -1,111 +1,36 @@
 import IsingModel.AmbientLattice.Exhaustion
-import IsingModel.AmbientLattice.MagnetizationAlongExhaustion
 import IsingModel.AmbientLattice.BetaDerivative
-import IsingModel.AmbientLattice.BetaDerivativeFieldJ
 import IsingModel.BetaDerivative
 import IsingModel.FieldDerivative
 
 /-!
-# magnetizationAlongExhaustion regularity wrappers (Step 213, GJ §17.5)
-
-Narrow child module for the 10 `magnetizationAlongExhaustion`
-regularity wrappers (9 with `_gen` suffix plus
-`magnetizationAlongExhaustion_hasDerivAt_beta`): continuous +
-differentiable + differentiableAt + hasDerivAt in
-β / β_general_h / field / J directions. Extracted from
-`BetaDerivative.lean` in PR #2063. Each is a thin pass-through to the
-corresponding `correlationAlongExhaustion_*` lemma at `A = {i}`.
-The theorem names are unchanged from the former `BetaDerivative`
-declarations.
+# magnetizationAlongExhaustion `HasDerivAt` wrappers (Step 213, GJ §17.5)
+
+Narrow child module for the two `magnetizationAlongExhaustion`
+existence-form β-derivative wrappers
+`magnetizationAlongExhaustion_hasDerivAt_beta` (at `h = 0`) and
+`magnetizationAlongExhaustion_hasDerivAt_beta_general_h_gen` (at general
+`h`). Each is a thin pass-through to the corresponding
+`correlationAlongExhaustion_hasDerivAt_*` lemma at `A = {i}`. Extracted
+from `BetaDerivative.lean` in PR #2063; the theorem names are unchanged
+from the former `BetaDerivative` declarations.
+
+The `Continuous` / `Differentiable` regularity of
+`magnetizationAlongExhaustion` in the β / h / J directions lives in
+`AmbientLattice/SpecialCases/Magnetization.lean`; the six `_gen`-suffixed
+duplicates that used to sit here were retired in PR #4839 because each
+stated exactly the same proposition as its `SpecialCases` counterpart
+(same binders in the same order, and the β pair was already at general
+`h`). Their `h = 0` corollaries
+`magnetizationAlongExhaustion_{continuous, differentiable}_beta_gen`
+keep their names and moved to the same `SpecialCases` module.
 -/
 
 namespace IsingModel.Ambient
 
 variable {V : Type*} [DecidableEq V]
 
-/-! ## Step 213: magnetizationAlongExhaustion regularity (β/h/J directions) -/
-
-/-- **magnetizationAlongExhaustion Continuous in β at h = 0** (Step 213, general G, Λ).
-Reduces to `correlationAlongExhaustion_continuous_beta_gen` at `A = {i}`. -/
-theorem magnetizationAlongExhaustion_continuous_beta_gen
-    (G : SimpleGraph V) (Λ : Exhaustion V)
-    [∀ n, Fintype (inducedGraph G (Λ.volume n)).edgeSet]
-    (J : ℝ) (i : V) (n : ℕ) :
-    Continuous
-      (fun β' => magnetizationAlongExhaustion G Λ (⟨J, 0, β'⟩ : IsingParams ℝ) i n) := by
-  simp only [magnetizationAlongExhaustion_apply]
-  exact correlationAlongExhaustion_continuous_beta_gen G Λ J {i} n
-
-/-- **magnetizationAlongExhaustion Differentiable in β at h = 0** (Step 213, general G, Λ). -/
-theorem magnetizationAlongExhaustion_differentiable_beta_gen
-    (G : SimpleGraph V) (Λ : Exhaustion V)
-    [∀ n, Fintype (inducedGraph G (Λ.volume n)).edgeSet]
-    (J : ℝ) (i : V) (n : ℕ) :
-    Differentiable ℝ
-      (fun β' => magnetizationAlongExhaustion G Λ (⟨J, 0, β'⟩ : IsingParams ℝ) i n) := by
-  simp only [magnetizationAlongExhaustion_apply]
-  exact correlationAlongExhaustion_differentiable_beta_gen G Λ J {i} n
-
-/-- **magnetizationAlongExhaustion Continuous in β at general h** (Step 250, general G, Λ).
-Extends Step 213 from h = 0 to general h via Step 249. -/
-theorem magnetizationAlongExhaustion_continuous_beta_general_h_gen
-    (G : SimpleGraph V) (Λ : Exhaustion V)
-    [∀ n, Fintype (inducedGraph G (Λ.volume n)).edgeSet]
-    (J h : ℝ) (i : V) (n : ℕ) :
-    Continuous
-      (fun β' => magnetizationAlongExhaustion G Λ (⟨J, h, β'⟩ : IsingParams ℝ) i n) := by
-  simp only [magnetizationAlongExhaustion_apply]
-  exact correlationAlongExhaustion_continuous_beta_general_h_gen G Λ J h {i} n
-
-/-- **magnetizationAlongExhaustion Differentiable in β at general h** (Step 250, general G, Λ). -/
-theorem magnetizationAlongExhaustion_differentiable_beta_general_h_gen
-    (G : SimpleGraph V) (Λ : Exhaustion V)
-    [∀ n, Fintype (inducedGraph G (Λ.volume n)).edgeSet]
-    (J h : ℝ) (i : V) (n : ℕ) :
-    Differentiable ℝ
-      (fun β' => magnetizationAlongExhaustion G Λ (⟨J, h, β'⟩ : IsingParams ℝ) i n) := by
-  simp only [magnetizationAlongExhaustion_apply]
-  exact correlationAlongExhaustion_differentiable_beta_general_h_gen G Λ J h {i} n
-
-/-- **magnetizationAlongExhaustion Continuous in h** (Step 213, general G, Λ). -/
-theorem magnetizationAlongExhaustion_continuous_field_gen
-    (G : SimpleGraph V) (Λ : Exhaustion V)
-    [∀ n, Fintype (inducedGraph G (Λ.volume n)).edgeSet]
-    (J β : ℝ) (i : V) (n : ℕ) :
-    Continuous
-      (fun h' => magnetizationAlongExhaustion G Λ (⟨J, h', β⟩ : IsingParams ℝ) i n) := by
-  simp only [magnetizationAlongExhaustion_apply]
-  exact correlationAlongExhaustion_continuous_field_gen G Λ J β {i} n
-
-/-- **magnetizationAlongExhaustion Differentiable in h** (Step 213, general G, Λ). -/
-theorem magnetizationAlongExhaustion_differentiable_field_gen
-    (G : SimpleGraph V) (Λ : Exhaustion V)
-    [∀ n, Fintype (inducedGraph G (Λ.volume n)).edgeSet]
-    (J β : ℝ) (i : V) (n : ℕ) :
-    Differentiable ℝ
-      (fun h' => magnetizationAlongExhaustion G Λ (⟨J, h', β⟩ : IsingParams ℝ) i n) := by
-  simp only [magnetizationAlongExhaustion_apply]
-  exact correlationAlongExhaustion_differentiable_field_gen G Λ J β {i} n
-
-/-- **magnetizationAlongExhaustion Continuous in J** (Step 213, general G, Λ). -/
-theorem magnetizationAlongExhaustion_continuous_J_gen
-    (G : SimpleGraph V) (Λ : Exhaustion V)
-    [∀ n, Fintype (inducedGraph G (Λ.volume n)).edgeSet]
-    (h β : ℝ) (i : V) (n : ℕ) :
-    Continuous
-      (fun J' => magnetizationAlongExhaustion G Λ (⟨J', h, β⟩ : IsingParams ℝ) i n) := by
-  simp only [magnetizationAlongExhaustion_apply]
-  exact correlationAlongExhaustion_continuous_J_gen G Λ h β {i} n
-
-/-- **magnetizationAlongExhaustion Differentiable in J** (Step 213, general G, Λ). -/
-theorem magnetizationAlongExhaustion_differentiable_J_gen
-    (G : SimpleGraph V) (Λ : Exhaustion V)
-    [∀ n, Fintype (inducedGraph G (Λ.volume n)).edgeSet]
-    (h β : ℝ) (i : V) (n : ℕ) :
-    Differentiable ℝ
-      (fun J' => magnetizationAlongExhaustion G Λ (⟨J', h, β⟩ : IsingParams ℝ) i n) := by
-  simp only [magnetizationAlongExhaustion_apply]
-  exact correlationAlongExhaustion_differentiable_J_gen G Λ h β {i} n
+/-! ## Step 213: magnetizationAlongExhaustion β-direction `HasDerivAt` -/
 
 /-- **β-derivative of `magnetizationAlongExhaustion` at `h = 0`** (GJ §17.5):
 The function `fun β' => magnetizationAlongExhaustion G Λ ⟨J, 0, β'⟩ i n`

IsingModel/AmbientLattice/Exhaustion.lean

@@ -322,6 +322,43 @@ theorem correlationAlongExhaustion_of_not_subset
     correlationAlongExhaustion G Λ p A n = 0 := by
   simp only [correlationAlongExhaustion, hA, dite_false]
 
+/-- **Family form of `correlationAlongExhaustion_of_subset`** (GJ §4.6,
+pp. 67-70; §5.1, pp. 72-75): for a family of parameters `p : α → IsingParams ℝ`
+and `A ⊆ Λ.volume n`, the whole function `fun t => correlationAlongExhaustion
+G Λ (p t) A n` equals `fun t => correlationΛ G (Λ.volume n) (p t)
+(liftFinset A hA)`.
+
+The subset hypothesis does not mention the family parameter `t`, so the
+`dite` case split of `correlationAlongExhaustion` factors out of the family.
+This is the first-order companion of the pointwise lemma: it is an ordinary
+equation between functions and is therefore usable by `rw`, which is what the
+per-parameter regularity wrappers (`Continuous` / `Differentiable` in
+`β` / `h` / `J`) need. The family parameter `p` is explicit on purpose, so that
+rewriting never has to solve for a function-valued metavariable. -/
+theorem correlationAlongExhaustion_family_eq_of_subset
+    {α : Type*} (G : SimpleGraph V) (Λ : Exhaustion V)
+    [∀ n, Fintype (inducedGraph G (Λ.volume n)).edgeSet]
+    (p : α → IsingParams ℝ) {A : Finset V} {n : ℕ} (hA : A ⊆ Λ.volume n) :
+    (fun t => correlationAlongExhaustion G Λ (p t) A n)
+      = fun t => correlationΛ G (Λ.volume n) (p t) (liftFinset A hA) :=
+  funext fun t => correlationAlongExhaustion_of_subset G Λ (p t) hA
+
+/-- **Family form of `correlationAlongExhaustion_of_not_subset`** (GJ §4.6,
+pp. 67-70; §5.1, pp. 72-75): for a family of parameters `p : α → IsingParams ℝ`
+and `A ⊄ Λ.volume n`, the whole function `fun t => correlationAlongExhaustion
+G Λ (p t) A n` is the zero function.
+
+As for the subset case, the non-membership hypothesis is independent of the
+family parameter `t`, so the `dite` case split factors out. First-order
+companion of the pointwise lemma, `rw`-usable, with the family parameter `p`
+explicit. -/
+theorem correlationAlongExhaustion_family_eq_zero_of_not_subset
+    {α : Type*} (G : SimpleGraph V) (Λ : Exhaustion V)
+    [∀ n, Fintype (inducedGraph G (Λ.volume n)).edgeSet]
+    (p : α → IsingParams ℝ) {A : Finset V} {n : ℕ} (hA : ¬ A ⊆ Λ.volume n) :
+    (fun t => correlationAlongExhaustion G Λ (p t) A n) = fun _ : α => (0 : ℝ) :=
+  funext fun t => correlationAlongExhaustion_of_not_subset G Λ (p t) hA
+
 /-- For any finite `A`, the correlation along an exhaustion is
 eventually equal to the lifted correlation. -/
 theorem correlationAlongExhaustion_eventually

IsingModel/AmbientLattice/SpecialCases/Magnetization.lean

@@ -10,15 +10,23 @@ RegularityAtContinuousAtBeta,RegularityAtDifferentiableAt,
 RegularityAtDifferentiableAtBeta,RegularityContinuousBeta,
 RegularityDifferentiable,RegularityDifferentiableBeta}.lean`) as part of
 the #4563 cycle-10 fixed-cost consolidation. All 15 theorem
-names/statements/proofs are preserved verbatim; see the git history of the
+names/statements are preserved verbatim; see the git history of the
 deleted `Magnetization*.lean` for provenance.
 
 Contents (finite-stage along-exhaustion wrappers, each a thin pass-through
 to the corresponding ambient `magnetizationΛ_*` lemma):
 
 * parameter-direction convergence (β/h/J → ∞);
 * global `Continuous` / `Differentiable` regularity in β/h/J;
+* the `h = 0` corollaries `magnetizationAlongExhaustion_{continuous,
+  differentiable}_beta_gen`, re-homed here from
+  `AmbientLattice/BetaDerivativeMagnetization.lean`;
 * pointwise `ContinuousAt` / `DifferentiableAt` regularity in β/h/J.
+
+The six global regularity proofs case-split on `{i} ⊆ Λ.volume n` through the
+first-order family equations `correlationAlongExhaustion_family_eq_of_subset`
+and `correlationAlongExhaustion_family_eq_zero_of_not_subset`
+(`AmbientLattice/Exhaustion.lean`) instead of unfolding the `dite` by hand.
 -/
 
 namespace IsingModel
@@ -129,11 +137,13 @@ theorem magnetizationAlongExhaustion_differentiable_beta
     Differentiable ℝ (fun β' =>
       magnetizationAlongExhaustion G Λ
         (⟨J, h, β'⟩ : IsingParams ℝ) i n) := by
-  unfold magnetizationAlongExhaustion correlationAlongExhaustion
+  unfold magnetizationAlongExhaustion
   by_cases hi : ({i} : Finset V) ⊆ Λ.volume n
-  · simp only [hi, dif_pos]
+  · rw [correlationAlongExhaustion_family_eq_of_subset G Λ
+      (fun β' => (⟨J, h, β'⟩ : IsingParams ℝ)) hi]
     exact magnetizationΛ_differentiable_beta G (Λ.volume n) J h _
-  · simp only [hi, dif_neg, not_false_iff]
+  · rw [correlationAlongExhaustion_family_eq_zero_of_not_subset G Λ
+      (fun β' => (⟨J, h, β'⟩ : IsingParams ℝ)) hi]
     exact differentiable_const _
 
 /-- **Along-ex: magnetization Continuous in `β`** (general h). -/
@@ -144,13 +154,39 @@ theorem magnetizationAlongExhaustion_continuous_beta
     Continuous (fun β' =>
       magnetizationAlongExhaustion G Λ
         (⟨J, h, β'⟩ : IsingParams ℝ) i n) := by
-  unfold magnetizationAlongExhaustion correlationAlongExhaustion
+  unfold magnetizationAlongExhaustion
   by_cases hi : ({i} : Finset V) ⊆ Λ.volume n
-  · simp only [hi, dif_pos]
+  · rw [correlationAlongExhaustion_family_eq_of_subset G Λ
+      (fun β' => (⟨J, h, β'⟩ : IsingParams ℝ)) hi]
     exact magnetizationΛ_continuous_beta G (Λ.volume n) J h _
-  · simp only [hi, dif_neg, not_false_iff]
+  · rw [correlationAlongExhaustion_family_eq_zero_of_not_subset G Λ
+      (fun β' => (⟨J, h, β'⟩ : IsingParams ℝ)) hi]
     exact continuous_const
 
+/-- **Along-ex: magnetization Differentiable in `β` at `h = 0`**
+(Step 213, general `G`, `Λ`). The `h = 0` corollary of
+`magnetizationAlongExhaustion_differentiable_beta`; kept as a named result
+because Glimm–Jaffe §17.5 states the zero-field case separately. -/
+theorem magnetizationAlongExhaustion_differentiable_beta_gen
+    (G : SimpleGraph V) (Λ : Exhaustion V)
+    [∀ n, Fintype (inducedGraph G (Λ.volume n)).edgeSet]
+    (J : ℝ) (i : V) (n : ℕ) :
+    Differentiable ℝ
+      (fun β' => magnetizationAlongExhaustion G Λ (⟨J, 0, β'⟩ : IsingParams ℝ) i n) :=
+  magnetizationAlongExhaustion_differentiable_beta G Λ J 0 i n
+
+/-- **Along-ex: magnetization Continuous in `β` at `h = 0`**
+(Step 213, general `G`, `Λ`). The `h = 0` corollary of
+`magnetizationAlongExhaustion_continuous_beta`; kept as a named result
+because Glimm–Jaffe §17.5 states the zero-field case separately. -/
+theorem magnetizationAlongExhaustion_continuous_beta_gen
+    (G : SimpleGraph V) (Λ : Exhaustion V)
+    [∀ n, Fintype (inducedGraph G (Λ.volume n)).edgeSet]
+    (J : ℝ) (i : V) (n : ℕ) :
+    Continuous
+      (fun β' => magnetizationAlongExhaustion G Λ (⟨J, 0, β'⟩ : IsingParams ℝ) i n) :=
+  magnetizationAlongExhaustion_continuous_beta G Λ J 0 i n
+
 /-- **Along-ex: magnetization Differentiable in `h`**. -/
 theorem magnetizationAlongExhaustion_differentiable_field
     (G : SimpleGraph V) (Λ : Exhaustion V)
@@ -159,11 +195,13 @@ theorem magnetizationAlongExhaustion_differentiable_field
     Differentiable ℝ (fun h' =>
       magnetizationAlongExhaustion G Λ
         (⟨J, h', β⟩ : IsingParams ℝ) i n) := by
-  unfold magnetizationAlongExhaustion correlationAlongExhaustion
+  unfold magnetizationAlongExhaustion
   by_cases hi : ({i} : Finset V) ⊆ Λ.volume n
-  · simp only [hi, dif_pos]
+  · rw [correlationAlongExhaustion_family_eq_of_subset G Λ
+      (fun h' => (⟨J, h', β⟩ : IsingParams ℝ)) hi]
     exact magnetizationΛ_differentiable_field G (Λ.volume n) J β _
-  · simp only [hi, dif_neg, not_false_iff]
+  · rw [correlationAlongExhaustion_family_eq_zero_of_not_subset G Λ
+      (fun h' => (⟨J, h', β⟩ : IsingParams ℝ)) hi]
     exact differentiable_const _
 
 /-- **Along-ex: magnetization Differentiable in `J`**. -/
@@ -174,11 +212,13 @@ theorem magnetizationAlongExhaustion_differentiable_J
     Differentiable ℝ (fun J' =>
       magnetizationAlongExhaustion G Λ
         (⟨J', h, β⟩ : IsingParams ℝ) i n) := by
-  unfold magnetizationAlongExhaustion correlationAlongExhaustion
+  unfold magnetizationAlongExhaustion
   by_cases hi : ({i} : Finset V) ⊆ Λ.volume n
-  · simp only [hi, dif_pos]
+  · rw [correlationAlongExhaustion_family_eq_of_subset G Λ
+      (fun J' => (⟨J', h, β⟩ : IsingParams ℝ)) hi]
     exact magnetizationΛ_differentiable_J G (Λ.volume n) h β _
-  · simp only [hi, dif_neg, not_false_iff]
+  · rw [correlationAlongExhaustion_family_eq_zero_of_not_subset G Λ
+      (fun J' => (⟨J', h, β⟩ : IsingParams ℝ)) hi]
     exact differentiable_const _
 
 /-- **Along-ex: magnetization Continuous in `h` for `i ∈
@@ -190,11 +230,13 @@ theorem magnetizationAlongExhaustion_continuous_field
     Continuous (fun h' =>
       magnetizationAlongExhaustion G Λ
         (⟨J, h', β⟩ : IsingParams ℝ) i n) := by
-  unfold magnetizationAlongExhaustion correlationAlongExhaustion
+  unfold magnetizationAlongExhaustion
   by_cases hi : ({i} : Finset V) ⊆ Λ.volume n
-  · simp only [hi, dif_pos]
+  · rw [correlationAlongExhaustion_family_eq_of_subset G Λ
+      (fun h' => (⟨J, h', β⟩ : IsingParams ℝ)) hi]
     exact magnetizationΛ_continuous_field G (Λ.volume n) J β _
-  · simp only [hi, dif_neg, not_false_iff]
+  · rw [correlationAlongExhaustion_family_eq_zero_of_not_subset G Λ
+      (fun h' => (⟨J, h', β⟩ : IsingParams ℝ)) hi]
     exact continuous_const
 
 /-- **Along-ex: magnetization Continuous in `J`**. -/
@@ -205,11 +247,13 @@ theorem magnetizationAlongExhaustion_continuous_J
     Continuous (fun J' =>
       magnetizationAlongExhaustion G Λ
         (⟨J', h, β⟩ : IsingParams ℝ) i n) := by
-  unfold magnetizationAlongExhaustion correlationAlongExhaustion
+  unfold magnetizationAlongExhaustion
   by_cases hi : ({i} : Finset V) ⊆ Λ.volume n
-  · simp only [hi, dif_pos]
+  · rw [correlationAlongExhaustion_family_eq_of_subset G Λ
+      (fun J' => (⟨J', h, β⟩ : IsingParams ℝ)) hi]
     exact magnetizationΛ_continuous_J G (Λ.volume n) h β _
-  · simp only [hi, dif_neg, not_false_iff]
+  · rw [correlationAlongExhaustion_family_eq_zero_of_not_subset G Λ
+      (fun J' => (⟨J', h, β⟩ : IsingParams ℝ)) hi]
     exact continuous_const
 
 /-! ### pointwise magnetization regularity

IsingModel/Concrete/LatticeGraphCorrelation/MagnetizationPointwiseRegularity.lean

@@ -1,6 +1,5 @@
 import IsingModel.Lattice
-import IsingModel.AmbientLattice.BetaDerivative
-import IsingModel.AmbientLattice.BetaDerivativeMagnetization
+import IsingModel.AmbientLattice.SpecialCases.Magnetization
 
 /-!
 # Concrete pointwise regularity wrappers for lattice magnetization
@@ -28,8 +27,8 @@ theorem magnetizationAlongExhaustion_latticeGraph_continuousAt_beta
     ContinuousAt (fun β' =>
       Ambient.magnetizationAlongExhaustion (IsingModel.latticeGraph d) Λ
         (⟨J, h, β'⟩ : IsingParams ℝ) i n) β :=
-  (Ambient.magnetizationAlongExhaustion_continuous_beta_general_h_gen
-    (IsingModel.latticeGraph d) Λ J h i n).continuousAt
+  Ambient.magnetizationAlongExhaustion_continuousAt_beta
+    (IsingModel.latticeGraph d) Λ J h β i n
 
 /-- **ℤ^d along-ex: `magnetizationAlongExhaustion` DifferentiableAt β** (general h). -/
 theorem magnetizationAlongExhaustion_latticeGraph_differentiableAt_beta
@@ -40,8 +39,8 @@ theorem magnetizationAlongExhaustion_latticeGraph_differentiableAt_beta
     DifferentiableAt ℝ (fun β' =>
       Ambient.magnetizationAlongExhaustion (IsingModel.latticeGraph d) Λ
         (⟨J, h, β'⟩ : IsingParams ℝ) i n) β :=
-  (Ambient.magnetizationAlongExhaustion_differentiable_beta_general_h_gen
-    (IsingModel.latticeGraph d) Λ J h i n).differentiableAt
+  Ambient.magnetizationAlongExhaustion_differentiableAt_beta
+    (IsingModel.latticeGraph d) Λ J h β i n
 
 /-! ## Moved: field/J pointwise wrappers