Build tight (diagonal-free) per-stage increment chain

The weak derivBound carries a diagonal term ⟨σ_rσ_s⟩⟨σ_kσ_l⟩ whose shell
sum is ⟨σ_rσ_s⟩·O(|∂box_k|), which diverges with shell size and cannot
prove convergence of c_k. Re-derive the entire per-stage increment chain
with the tight ball-boundary Simon-Lieb bound derivBoundTight (cross
products only, via cor_4_3_3_scaled):

- Tight.lean: scaledCorrelation_one_sub_zero_le_derivBoundTight,
  correlation_sub_deleteEdges_le_derivBoundTight,
  derivBoundTight_le_of_correlation_le.
- PerStageIncrement.lean: correlation_pair_sub_inducedGraph_le_derivBoundTight,
  correlation_pair_two_box_le_derivBoundTight.
- CubicPerStageIncrement.lean:
  correlationAlongExhaustion_cubic_succ_sub_le_derivBoundTight.
- CubicShellInfiniteVolumeBound.lean:
  derivBoundTight_inducedGraph_cubic_le_infiniteVolume_sum.

Net diagonal-free bound:
  c_{k+1} − c_k ≤ β·J·∑_{⟨a,b⟩∈shell}[g{r,a}g{s,b} + g{r,b}g{s,a}]
(g = infinite-volume correlation), the summable form on which Phase B
spatial decay yields a geometric rate.

Each tight lemma mirrors its weak counterpart (#2972/#2974/#2989/#2992/
#2993/#2994/#2995); the component-factorization and observable-matching
infrastructure is bound-independent and reused unchanged.

Docs and proof-guide synced.

Part of #2965

Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>

Author: phasetr

IsingModel/AmbientLatticeSum/PerStageIncrement.lean

@@ -1,4 +1,5 @@
 import IsingModel.BallBoundarySimonLieb.WeakBound
+import IsingModel.BallBoundarySimonLieb.Tight
 import IsingModel.AmbientLatticeSum.InducedUnion
 
 /-!
@@ -241,4 +242,95 @@ theorem correlation_pair_two_box_le_derivBound (G : SimpleGraph V) {T₁ T₂ :
     correlation_inducedGraph_nested_finset G hsub p {⟨r, hr₁⟩, ⟨s, hs₁⟩}] at h1
   exact h1
 
+set_option linter.unusedFintypeInType false in
+/-- **Tight numeric per-stage correlation increment**: tight analogue of
+`correlation_pair_sub_inducedGraph_le_derivBound` bounding the same single-box
+increment by the *tight* `derivBoundTight` (cross products only, no diagonal
+`⟨σ_r σ_s⟩·⟨σ_k σ_l⟩` term). Composes `correlation_sub_deleteEdges_le_derivBoundTight`
+with `correlation_deleteEdges_filter_pair_eq`. Dropping the diagonal term is what
+makes the per-stage exhaustion increment summable under spatial decay (Issue #2965,
+Phase A→B). -/
+theorem correlation_pair_sub_inducedGraph_le_derivBoundTight (G : SimpleGraph V)
+    [Fintype G.edgeSet] (S : Finset V) (p : IsingParams ℝ) (hf : Ferromagnetic p)
+    (hh : p.h = 0) (r s : V) (hr : r ∈ S) (hs : s ∈ S) (hrs : r ≠ s)
+    (hsep : ∀ e ∈ G.edgeFinset.filter (straddlePred S),
+      ¬ Sym2.Mem r e ∧ ¬ Sym2.Mem s e)
+    [Fintype (G.deleteEdges ↑(G.edgeFinset.filter (straddlePred S))).edgeSet]
+    [Fintype (G.deleteEdges {e : Sym2 V | straddlePred S e}).edgeSet]
+    [Fintype (inducedGraph (G.deleteEdges {e : Sym2 V | straddlePred S e}) S).edgeSet]
+    [Fintype (inducedGraph (G.deleteEdges {e : Sym2 V | straddlePred S e}) Sᶜ).edgeSet]
+    [Fintype (((inducedGraph (G.deleteEdges {e : Sym2 V | straddlePred S e}) S).sum
+        (inducedGraph (G.deleteEdges {e : Sym2 V | straddlePred S e}) Sᶜ)).map
+      (Equiv.Finset.union S Sᶜ disjoint_compl_right).toEmbedding).edgeSet]
+    [Fintype (inducedGraph (G.deleteEdges {e : Sym2 V | straddlePred S e}) (S ∪ Sᶜ)).edgeSet]
+    [Fintype ((G.deleteEdges {e : Sym2 V | straddlePred S e}).induce
+      (↑(S ∪ Sᶜ) : Set V)).edgeSet]
+    [Fintype (inducedGraph G S).edgeSet] :
+    correlation G p {r, s}
+        - correlation (inducedGraph G S) p {⟨r, hr⟩, ⟨s, hs⟩}
+      ≤ derivBoundTight G (G.edgeFinset.filter (straddlePred S)) p r s := by
+  have hnd : ∀ e ∈ G.edgeFinset.filter (straddlePred S), ¬ e.IsDiag := fun e he =>
+    G.not_isDiag_of_mem_edgeFinset (Finset.mem_of_mem_filter e he)
+  have h1 := correlation_sub_deleteEdges_le_derivBoundTight G
+    (G.edgeFinset.filter (straddlePred S)) hnd (Finset.filter_subset _ _) p hf hh r s hrs hsep
+  rwa [correlation_deleteEdges_filter_pair_eq G S p hr hs] at h1
+
+set_option linter.unusedFintypeInType false in
+omit [Fintype V] in
+/-- **Tight two-box per-stage correlation increment** (Issue #2965, Phase A→B):
+tight analogue of `correlation_pair_two_box_le_derivBound`, bounding the nested-box
+pair correlation increment by the *tight* `derivBoundTight` over the cut edges of
+the `T₁`-slice. Composes the tight single-box increment
+`correlation_pair_sub_inducedGraph_le_derivBoundTight` with the double-induce
+identification `correlation_inducedGraph_nested_finset`. The cross-product-only
+`derivBoundTight` is what makes the cubic per-stage increment summable. -/
+theorem correlation_pair_two_box_le_derivBoundTight (G : SimpleGraph V) {T₁ T₂ : Finset V}
+    (hsub : T₁ ⊆ T₂) (p : IsingParams ℝ) (hf : Ferromagnetic p) (hh : p.h = 0)
+    {r s : V} (hr₁ : r ∈ T₁) (hs₁ : s ∈ T₁) (hrs : r ≠ s)
+    [Fintype (inducedGraph G T₂).edgeSet]
+    (hsep : ∀ e ∈ (inducedGraph G T₂).edgeFinset.filter
+        (straddlePred (T₁.subtype (· ∈ T₂))),
+      ¬ Sym2.Mem (⟨r, hsub hr₁⟩ : (↑T₂ : Type _)) e ∧
+        ¬ Sym2.Mem (⟨s, hsub hs₁⟩ : (↑T₂ : Type _)) e)
+    [Fintype ((inducedGraph G T₂).deleteEdges
+      ↑((inducedGraph G T₂).edgeFinset.filter
+        (straddlePred (T₁.subtype (· ∈ T₂))))).edgeSet]
+    [Fintype ((inducedGraph G T₂).deleteEdges
+      {e : Sym2 (↑T₂ : Type _) | straddlePred (T₁.subtype (· ∈ T₂)) e}).edgeSet]
+    [Fintype (inducedGraph ((inducedGraph G T₂).deleteEdges
+      {e : Sym2 (↑T₂ : Type _) | straddlePred (T₁.subtype (· ∈ T₂)) e})
+        (T₁.subtype (· ∈ T₂))).edgeSet]
+    [Fintype (inducedGraph ((inducedGraph G T₂).deleteEdges
+      {e : Sym2 (↑T₂ : Type _) | straddlePred (T₁.subtype (· ∈ T₂)) e})
+        (T₁.subtype (· ∈ T₂))ᶜ).edgeSet]
+    [Fintype (((inducedGraph ((inducedGraph G T₂).deleteEdges
+      {e : Sym2 (↑T₂ : Type _) | straddlePred (T₁.subtype (· ∈ T₂)) e})
+        (T₁.subtype (· ∈ T₂))).sum
+      (inducedGraph ((inducedGraph G T₂).deleteEdges
+        {e : Sym2 (↑T₂ : Type _) | straddlePred (T₁.subtype (· ∈ T₂)) e})
+          (T₁.subtype (· ∈ T₂))ᶜ)).map
+      (Equiv.Finset.union (T₁.subtype (· ∈ T₂)) (T₁.subtype (· ∈ T₂))ᶜ
+        disjoint_compl_right).toEmbedding).edgeSet]
+    [Fintype (inducedGraph ((inducedGraph G T₂).deleteEdges
+      {e : Sym2 (↑T₂ : Type _) | straddlePred (T₁.subtype (· ∈ T₂)) e})
+        ((T₁.subtype (· ∈ T₂)) ∪ (T₁.subtype (· ∈ T₂))ᶜ)).edgeSet]
+    [Fintype (((inducedGraph G T₂).deleteEdges
+      {e : Sym2 (↑T₂ : Type _) | straddlePred (T₁.subtype (· ∈ T₂)) e}).induce
+      (↑((T₁.subtype (· ∈ T₂)) ∪ (T₁.subtype (· ∈ T₂))ᶜ) : Set (↑T₂ : Type _))).edgeSet]
+    [Fintype (inducedGraph (inducedGraph G T₂) (T₁.subtype (· ∈ T₂))).edgeSet]
+    [Fintype (inducedGraph G T₁).edgeSet]
+    [Fintype ((inducedGraph G T₁).map (nestedFinsetEquiv hsub).symm.toEmbedding).edgeSet] :
+    correlation (inducedGraph G T₂) p {⟨r, hsub hr₁⟩, ⟨s, hsub hs₁⟩}
+        - correlation (inducedGraph G T₁) p {⟨r, hr₁⟩, ⟨s, hs₁⟩}
+      ≤ derivBoundTight (inducedGraph G T₂) ((inducedGraph G T₂).edgeFinset.filter
+          (straddlePred (T₁.subtype (· ∈ T₂)))) p ⟨r, hsub hr₁⟩ ⟨s, hsub hs₁⟩ := by
+  have hrs' : (⟨r, hsub hr₁⟩ : (↑T₂ : Type _)) ≠ ⟨s, hsub hs₁⟩ := by
+    simpa [Subtype.ext_iff] using hrs
+  have h1 := correlation_pair_sub_inducedGraph_le_derivBoundTight (inducedGraph G T₂)
+    (T₁.subtype (· ∈ T₂)) p hf hh ⟨r, hsub hr₁⟩ ⟨s, hsub hs₁⟩
+    (Finset.mem_subtype.mpr hr₁) (Finset.mem_subtype.mpr hs₁) hrs' hsep
+  rw [← pair_map_nestedFinsetEquiv_symm hsub hr₁ hs₁,
+    correlation_inducedGraph_nested_finset G hsub p {⟨r, hr₁⟩, ⟨s, hs₁⟩}] at h1
+  exact h1
+
 end IsingModel

IsingModel/BallBoundarySimonLieb/Tight.lean

@@ -245,4 +245,111 @@ theorem ball_boundary_simon_lieb_tight (G : SimpleGraph ι) [Fintype G.edgeSet]
       Real.norm_of_nonneg (derivBoundTight_nonneg G E₀ p hf r s)] at hmvt
   linarith
 
+/-- **Tight finite-volume coupling difference bound**: the `s = 1` minus `s = 0`
+scaled-correlation difference is at most the *tight* ball-boundary derivative
+bound `derivBoundTight` (no extra `⟨σ_r σ_s⟩·⟨σ_k σ_l⟩` diagonal term). This is the
+tight analogue of `scaledCorrelation_one_sub_zero_le_derivBound`
+(`WeakBound.lean`); same mean-value argument, but the per-`t` derivative is bounded
+by `derivBoundTight` via `scaledCorrelation_pair_deriv_le_derivBoundTight` (which
+drops the diagonal term using `cor_4_3_3_scaled`). Dropping the diagonal term is
+what makes the resulting per-stage increment *summable* over an exhaustion's cut
+edges (Issue #2965, Phase A→B). -/
+theorem scaledCorrelation_one_sub_zero_le_derivBoundTight (G : SimpleGraph ι)
+    [Fintype G.edgeSet] (E₀ : Finset (Sym2 ι)) (hE₀_nd : ∀ e ∈ E₀, ¬e.IsDiag)
+    (hE₀_sub : E₀ ⊆ G.edgeFinset)
+    (p : IsingParams ℝ) (hf : Ferromagnetic p) (hh : p.h = 0)
+    (r s : ι) (hrs : r ≠ s)
+    (hE₀_sep : ∀ e ∈ E₀, ¬ Sym2.Mem r e ∧ ¬ Sym2.Mem s e) :
+    scaledCorrelation G E₀ p 1 {r, s} - scaledCorrelation G E₀ p 0 {r, s}
+      ≤ derivBoundTight G E₀ p r s := by
+  have hderiv : ∀ t ∈ Set.Icc (0 : ℝ) 1,
+      HasDerivWithinAt (fun s' => scaledCorrelation G E₀ p s' {r, s})
+        (p.β * p.J * ∑ e ∈ E₀,
+          Sym2.lift ⟨fun u v =>
+            scaledCorrelation G E₀ p t (symmDiff {r, s} {u, v}) -
+            scaledCorrelation G E₀ p t {r, s} *
+            scaledCorrelation G E₀ p t {u, v},
+          fun u v => by simp [Finset.pair_comm v u]⟩ e)
+        (Set.Icc 0 1) t :=
+    fun t _ => (hasDerivAt_scaledCorrelation G E₀ hE₀_nd p t {r, s}).hasDerivWithinAt
+  have hbound : ∀ t ∈ Set.Ico (0 : ℝ) 1,
+      ‖p.β * p.J * ∑ e ∈ E₀,
+          Sym2.lift ⟨fun u v =>
+            scaledCorrelation G E₀ p t (symmDiff {r, s} {u, v}) -
+            scaledCorrelation G E₀ p t {r, s} *
+            scaledCorrelation G E₀ p t {u, v},
+          fun u v => by simp [Finset.pair_comm v u]⟩ e‖ ≤
+      ‖derivBoundTight G E₀ p r s‖ := by
+    intro t ht
+    rw [Real.norm_of_nonneg
+          (scaledCorrelation_deriv_nonneg' G E₀ hE₀_nd hE₀_sub p hf t ht.1 {r, s}),
+        Real.norm_of_nonneg (derivBoundTight_nonneg G E₀ p hf r s)]
+    exact scaledCorrelation_pair_deriv_le_derivBoundTight G E₀ hE₀_nd hE₀_sub p hf hh r s hrs
+      hE₀_sep t ht.1 ht.2.le
+  have hmvt := norm_image_sub_le_of_norm_deriv_le_segment_01' hderiv hbound
+  rw [Real.norm_of_nonneg (derivBoundTight_nonneg G E₀ p hf r s)] at hmvt
+  calc scaledCorrelation G E₀ p 1 {r, s} - scaledCorrelation G E₀ p 0 {r, s}
+      ≤ |scaledCorrelation G E₀ p 1 {r, s} - scaledCorrelation G E₀ p 0 {r, s}| :=
+        le_abs_self _
+    _ = ‖scaledCorrelation G E₀ p 1 {r, s} - scaledCorrelation G E₀ p 0 {r, s}‖ :=
+        (Real.norm_eq_abs _).symm
+    _ ≤ derivBoundTight G E₀ p r s := hmvt
+
+/-- **Tight bond-deletion correlation increment**: adding the bond set `E₀`
+(with `r, s` on no `E₀`-edge) raises the pair correlation `⟨σ_r σ_s⟩` by at most the
+*tight* ball-boundary derivative bound `derivBoundTight` (cross terms only):
+
+  `correlation G p {r,s} − correlation (G.deleteEdges ↑E₀) p {r,s}
+     ≤ derivBoundTight G E₀ p r s`.
+
+Tight analogue of `correlation_sub_deleteEdges_le_derivBound` (`WeakBound.lean`):
+combines the tight mean-value difference bound with the `s = 0` bond-deleted
+identification `scaledCorrelation_zero`. Because `derivBoundTight` carries only the
+cross products `⟨σ_r σ_k⟩·⟨σ_s σ_l⟩ + ⟨σ_r σ_l⟩·⟨σ_s σ_k⟩` (no diagonal
+`⟨σ_r σ_s⟩·⟨σ_k σ_l⟩` term), the resulting per-stage exhaustion increment is
+summable under spatial decay — the form needed for the volume-convergence rate
+(Issue #2965, Phase A→B). -/
+theorem correlation_sub_deleteEdges_le_derivBoundTight (G : SimpleGraph ι)
+    [Fintype G.edgeSet] (E₀ : Finset (Sym2 ι)) (hE₀_nd : ∀ e ∈ E₀, ¬e.IsDiag)
+    (hE₀_sub : E₀ ⊆ G.edgeFinset) (p : IsingParams ℝ) (hf : Ferromagnetic p)
+    (hh : p.h = 0) (r s : ι) (hrs : r ≠ s)
+    (hE₀_sep : ∀ e ∈ E₀, ¬ Sym2.Mem r e ∧ ¬ Sym2.Mem s e)
+    [Fintype (G.deleteEdges ↑E₀).edgeSet] :
+    correlation G p {r, s} - correlation (G.deleteEdges ↑E₀) p {r, s}
+      ≤ derivBoundTight G E₀ p r s := by
+  have h := scaledCorrelation_one_sub_zero_le_derivBoundTight G E₀ hE₀_nd hE₀_sub p hf hh
+    r s hrs hE₀_sep
+  rwa [scaledCorrelation_one, scaledCorrelation_zero G E₀ hE₀_sub p {r, s}] at h
+
+/-- **`derivBoundTight` monotonicity under correlation upper bounds**: tight
+analogue of `derivBound_le_of_correlation_le`. If a nonnegative
+`c : ι → ι → ℝ` dominates every two-point correlation, then `derivBoundTight` is
+dominated by the same edge sum (cross products only) with each correlation replaced
+by `c`. Each summand is a sum of two products of nonnegative correlations
+(`gks_first`), monotone under the pointwise bound (no symmetry of `c` is needed:
+the cross-product summand is symmetric in `k, l` by `+`-commutativity alone).
+Separates the boundary-sum decay step (Issue #2965, Phase A→B): one may substitute
+`c a b =` an infinite-volume decay bound without re-touching the `derivBoundTight`
+algebra. -/
+theorem derivBoundTight_le_of_correlation_le (G : SimpleGraph ι) [Fintype G.edgeSet]
+    (E₀ : Finset (Sym2 ι)) (p : IsingParams ℝ) (hf : Ferromagnetic p)
+    (r s : ι) (c : ι → ι → ℝ)
+    (hc_nonneg : ∀ a b, 0 ≤ c a b)
+    (hcorr : ∀ a b, correlation G p {a, b} ≤ c a b) :
+    derivBoundTight G E₀ p r s
+      ≤ p.β * p.J * ∑ e ∈ E₀, Sym2.lift ⟨fun k l =>
+          c r k * c s l + c r l * c s k,
+          fun k l => by
+            change c r k * c s l + c r l * c s k = c r l * c s k + c r k * c s l
+            ring⟩ e := by
+  unfold derivBoundTight
+  apply mul_le_mul_of_nonneg_left _ (mul_nonneg hf.hβ.le hf.hJ)
+  apply Finset.sum_le_sum
+  intro e _he
+  obtain ⟨⟨k, l⟩, rfl⟩ := Quot.exists_rep e
+  simp only [Sym2.lift_mk]
+  refine add_le_add ?_ ?_
+  · exact mul_le_mul (hcorr r k) (hcorr s l) (gks_first G p hf _) (hc_nonneg r k)
+  · exact mul_le_mul (hcorr r l) (hcorr s k) (gks_first G p hf _) (hc_nonneg r l)
+
 end IsingModel

IsingModel/Concrete/LatticeGraphCorrelation/CubicPerStageIncrement.lean

@@ -73,5 +73,40 @@ theorem correlationAlongExhaustion_cubic_succ_sub_le_derivBound (d : ℕ)
   exact correlation_pair_two_box_le_derivBound (latticeGraph d)
     (cubicBox_mono d (Nat.le_succ k)) p hf hh hr hs hrs hsep
 
+/-- **Tight cubic-exhaustion per-stage correlation increment** (Issue #2965,
+Phase A→B): tight analogue of `correlationAlongExhaustion_cubic_succ_sub_le_derivBound`
+bounding the successive correlation difference by the *tight* `derivBoundTight`
+(cross products only) over the cut edges of the `box_k`-slice. Instantiates the
+tight two-box increment `correlation_pair_two_box_le_derivBoundTight` on
+`box_k ⊆ box_{k+1}`. The cross-product-only form is what makes `c_{k+1} − c_k`
+summable under the infinite-volume spatial decay. -/
+theorem correlationAlongExhaustion_cubic_succ_sub_le_derivBoundTight (d : ℕ)
+    (p : IsingParams ℝ) (hf : Ferromagnetic p) (hh : p.h = 0)
+    {r s : Fin d → ℤ} (hrs : r ≠ s) (k : ℕ)
+    (hr : r ∈ cubicBox d k) (hs : s ∈ cubicBox d k)
+    (hsep : ∀ e ∈ (inducedGraph (latticeGraph d) (cubicBox d (k + 1))).edgeFinset.filter
+        (straddlePred ((cubicBox d k).subtype (· ∈ cubicBox d (k + 1)))),
+      ¬ Sym2.Mem (⟨r, cubicBox_mono d (Nat.le_succ k) hr⟩ : (↑(cubicBox d (k + 1)) : Type _)) e ∧
+        ¬ Sym2.Mem (⟨s, cubicBox_mono d (Nat.le_succ k) hs⟩ :
+          (↑(cubicBox d (k + 1)) : Type _)) e) :
+    correlationAlongExhaustion (latticeGraph d) (cubicExhaustion d) p {r, s} (k + 1)
+        - correlationAlongExhaustion (latticeGraph d) (cubicExhaustion d) p {r, s} k
+      ≤ derivBoundTight (inducedGraph (latticeGraph d) (cubicBox d (k + 1)))
+          ((inducedGraph (latticeGraph d) (cubicBox d (k + 1))).edgeFinset.filter
+            (straddlePred ((cubicBox d k).subtype (· ∈ cubicBox d (k + 1))))) p
+          ⟨r, cubicBox_mono d (Nat.le_succ k) hr⟩ ⟨s, cubicBox_mono d (Nat.le_succ k) hs⟩ := by
+  have hsubk : ({r, s} : Finset (Fin d → ℤ)) ⊆ (cubicExhaustion d).volume k := by
+    change ({r, s} : Finset (Fin d → ℤ)) ⊆ cubicBox d k
+    rw [Finset.insert_subset_iff, Finset.singleton_subset_iff]; exact ⟨hr, hs⟩
+  have hsubk1 : ({r, s} : Finset (Fin d → ℤ)) ⊆ (cubicExhaustion d).volume (k + 1) :=
+    hsubk.trans (cubicBox_mono d (Nat.le_succ k))
+  rw [correlationAlongExhaustion, correlationAlongExhaustion,
+    dif_pos hsubk1, dif_pos hsubk, correlationΛ, correlationΛ,
+    liftFinset_pair hsubk1 (cubicBox_mono d (Nat.le_succ k) hr)
+      (cubicBox_mono d (Nat.le_succ k) hs),
+    liftFinset_pair hsubk hr hs]
+  exact correlation_pair_two_box_le_derivBoundTight (latticeGraph d)
+    (cubicBox_mono d (Nat.le_succ k)) p hf hh hr hs hrs hsep
+
 end Ambient
 end IsingModel

IsingModel/Concrete/LatticeGraphCorrelation/CubicShellInfiniteVolumeBound.lean

@@ -92,5 +92,34 @@ theorem derivBound_inducedGraph_cubic_le_infiniteVolume_sum (d : ℕ)
     (fun α β => correlationInfinite_nonneg (latticeGraph d) (cubicExhaustion d) p hf _)
     (fun α β => correlation_inducedGraph_cubic_le_correlationInfinite d p n α β)
 
+/-- **Tight cubic-shell `derivBoundTight` bounded by an infinite-volume cross sum**
+(Issue #2965, Phase A→B): tight analogue of
+`derivBound_inducedGraph_cubic_le_infiniteVolume_sum` using the
+cross-product-only `derivBoundTight`. For sites `r, s ∈ box_n` and any edge set
+`E₀`, `derivBoundTight … E₀ … ⟨r,_⟩ ⟨s,_⟩` is bounded by `β·J` times the edge sum
+of the infinite-volume cross products `g{r,a}·g{s,b} + g{r,b}·g{s,a}` (no diagonal
+`g{r,s}·g{a,b}` term). Combined with the tight per-stage increment
+`correlationAlongExhaustion_cubic_succ_sub_le_derivBoundTight`, this gives
+`c_{k+1} − c_k` bounded by a **summable** infinite-volume cross boundary sum — the
+diagonal-free form on which the Phase B spatial decay yields a geometric rate. -/
+theorem derivBoundTight_inducedGraph_cubic_le_infiniteVolume_sum (d : ℕ)
+    (p : IsingParams ℝ) (hf : Ferromagnetic p) (n : ℕ)
+    (E₀ : Finset (Sym2 (↑(cubicBox d n) : Type _)))
+    {r s : Fin d → ℤ} (hr : r ∈ cubicBox d n) (hs : s ∈ cubicBox d n) :
+    derivBoundTight (inducedGraph (latticeGraph d) (cubicBox d n)) E₀ p ⟨r, hr⟩ ⟨s, hs⟩
+      ≤ p.β * p.J * ∑ e ∈ E₀, Sym2.lift ⟨fun a b =>
+          correlationInfinite (latticeGraph d) (cubicExhaustion d) p {r, a.val} *
+              correlationInfinite (latticeGraph d) (cubicExhaustion d) p {s, b.val} +
+            correlationInfinite (latticeGraph d) (cubicExhaustion d) p {r, b.val} *
+              correlationInfinite (latticeGraph d) (cubicExhaustion d) p {s, a.val},
+          fun a b => by
+            change _ * _ + _ * _ = _ * _ + _ * _
+            ring⟩ e := by
+  exact derivBoundTight_le_of_correlation_le (inducedGraph (latticeGraph d) (cubicBox d n)) E₀ p hf
+    ⟨r, hr⟩ ⟨s, hs⟩
+    (fun α β => correlationInfinite (latticeGraph d) (cubicExhaustion d) p {α.val, β.val})
+    (fun α β => correlationInfinite_nonneg (latticeGraph d) (cubicExhaustion d) p hf _)
+    (fun α β => correlation_inducedGraph_cubic_le_correlationInfinite d p n α β)
+
 end Ambient
 end IsingModel