feat: concrete bond-deletion correlation increment bundle — #2965 (#2974)

* feat: concrete bond-deletion correlation increment bundle (Part of #2965)

* feat: concrete bond-deletion correlation increment bundle

Combine the ball-boundary mean-value bound with the s=0 bond-deleted
identification into standard-correlation form:

- correlation_sub_deleteEdges_le_derivBound:
    correlation G p {r,s} − correlation (G.deleteEdges ↑E₀) p {r,s}
      ≤ derivBound G E₀ p r s
- correlation_deleteEdges_le: GKS bond-monotonicity (deleting bonds cannot
    increase a correlation), so the increment is nonnegative
- derivBound_le_card: derivBound ≤ β·J·(3·|E₀|) (each correlation product ≤ 1)
- correlation_sub_deleteEdges_le_card: coarse a-priori increment bound
    correlation G p {r,s} − correlation (G.deleteEdges ↑E₀) p {r,s} ≤ β·J·(3·|E₀|)

Part of #2965

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

---------

Co-authored-by: Claude Opus 4.7 <noreply@anthropic.com>

Author: phasetr

IsingModel/BallBoundarySimonLieb/WeakBound.lean

@@ -1,4 +1,5 @@
 import IsingModel.BallBoundarySimonLieb.Monotonicity
+import IsingModel.InfiniteVolume.MonotoneH
 
 /-!
 # Ball-boundary Simon-Lieb weak bound wrappers
@@ -203,5 +204,88 @@ theorem scaledCorrelation_one_sub_zero_le_derivBound (G : SimpleGraph ι)
         (Real.norm_eq_abs _).symm
     _ ≤ derivBound G E₀ p r s := hmvt
 
+/-! ## Concrete bond-deletion correlation increment -/
+
+/-- **Concrete bond-deletion correlation increment**: combining the ball-boundary
+mean-value bound `scaledCorrelation_one_sub_zero_le_derivBound` with the `s = 0`
+bond-deleted identification `scaledCorrelation_zero`, adding the bond set `E₀`
+raises the pair correlation `⟨σ_r σ_s⟩` by at most `derivBound`:
+
+  `correlation G p {r,s} − correlation (G.deleteEdges ↑E₀) p {r,s}
+     ≤ derivBound G E₀ p r s`.
+
+This expresses the finite-volume coupling step entirely in terms of standard
+correlations of the full and bond-deleted models (Issue #2965, Phase A). -/
+theorem correlation_sub_deleteEdges_le_derivBound (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}
+      ≤ derivBound G E₀ p r s := by
+  have h := scaledCorrelation_one_sub_zero_le_derivBound 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
+
+/-- **GKS bond-monotonicity**: deleting the bonds `E₀` (with `E₀ ⊆ G.edgeFinset`)
+cannot increase a correlation. Specialization of `scaledCorrelation_monotoneOn`
+at `0 ≤ 1` via the `s = 0`/`s = 1` identifications. -/
+theorem correlation_deleteEdges_le (G : SimpleGraph ι) [Fintype G.edgeSet]
+    (E₀ : Finset (Sym2 ι)) (hE₀_nd : ∀ e ∈ E₀, ¬e.IsDiag)
+    (hE₀_sub : E₀ ⊆ G.edgeFinset) (p : IsingParams ℝ) (hf : Ferromagnetic p)
+    (A : Finset ι) [Fintype (G.deleteEdges ↑E₀).edgeSet] :
+    correlation (G.deleteEdges ↑E₀) p A ≤ correlation G p A := by
+  have h : scaledCorrelation G E₀ p 0 A ≤ scaledCorrelation G E₀ p 1 A :=
+    scaledCorrelation_monotoneOn G E₀ hE₀_nd hE₀_sub p hf A
+      (Set.mem_Ici.mpr le_rfl) (Set.mem_Ici.mpr zero_le_one) zero_le_one
+  rwa [scaledCorrelation_zero G E₀ hE₀_sub p A, scaledCorrelation_one] at h
+
+/-- The ball-boundary derivative bound is at most `β·J·(3·|E₀|)`: each of the three
+correlation products in a summand is at most `1` (each factor lies in `[0,1]` by
+`gks_first` and `correlation_le_one`). -/
+theorem derivBound_le_card (G : SimpleGraph ι) [Fintype G.edgeSet]
+    (E₀ : Finset (Sym2 ι)) (p : IsingParams ℝ) (hf : Ferromagnetic p) (r s : ι) :
+    derivBound G E₀ p r s ≤ p.β * p.J * (3 * E₀.card) := by
+  unfold derivBound
+  apply mul_le_mul_of_nonneg_left _ (mul_nonneg hf.hβ.le hf.hJ)
+  calc ∑ e ∈ E₀, Sym2.lift ⟨fun k l =>
+          correlation G p {r, k} * correlation G p {s, l} +
+          correlation G p {r, l} * correlation G p {s, k} +
+          correlation G p {r, s} * correlation G p {k, l},
+        fun k l => by simp [Finset.pair_comm k l]; ring⟩ e
+      ≤ ∑ _e ∈ E₀, (3 : ℝ) := by
+        apply Finset.sum_le_sum
+        intro e _
+        obtain ⟨⟨k, l⟩, rfl⟩ := Quot.exists_rep e
+        simp only [Sym2.lift_mk]
+        have h1 : correlation G p {r, k} * correlation G p {s, l} ≤ 1 :=
+          mul_le_one₀ (correlation_le_one G p _) (gks_first G p hf _)
+            (correlation_le_one G p _)
+        have h2 : correlation G p {r, l} * correlation G p {s, k} ≤ 1 :=
+          mul_le_one₀ (correlation_le_one G p _) (gks_first G p hf _)
+            (correlation_le_one G p _)
+        have h3 : correlation G p {r, s} * correlation G p {k, l} ≤ 1 :=
+          mul_le_one₀ (correlation_le_one G p _) (gks_first G p hf _)
+            (correlation_le_one G p _)
+        linarith
+    _ = 3 * E₀.card := by rw [Finset.sum_const, nsmul_eq_mul]; ring
+
+/-- **Concrete bond-deletion increment cardinality bound**: combining
+`correlation_sub_deleteEdges_le_derivBound` with `derivBound_le_card`, adding the
+bond set `E₀` raises `⟨σ_r σ_s⟩` by at most `β·J·(3·|E₀|)` — a coarse a-priori
+bound on the finite-volume coupling step (Issue #2965, Phase A). -/
+theorem correlation_sub_deleteEdges_le_card (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}
+      ≤ p.β * p.J * (3 * E₀.card) :=
+  le_trans
+    (correlation_sub_deleteEdges_le_derivBound G E₀ hE₀_nd hE₀_sub p hf hh r s hrs hE₀_sep)
+    (derivBound_le_card G E₀ p hf r s)
+
 
 end IsingModel

docs/index.md

@@ -1326,7 +1326,7 @@ inventory (2026-04-17).
 | §17.5 | Lemma 17.5.2 anchored cubic capstone bundle | **Done (same-constant upper predicate + sandwich bundle)** | `lemma_17_5_2_cubic_origin_capstone_of_named_rate_on_self_Icc`, `lemma_17_5_2_cubic_origin_capstone_of_profile_lower_on_self_Icc`, `lemma_17_5_2_cubic_origin_capstone_of_cubicTanhProfileBound_on_self_Icc`, and `lemma_17_5_2_cubic_origin_capstone_of_cubicTanhProfileBound_on_Icc` (`Concrete/LatticeGraphCorrelation/Lemma_17_5_2/PseudoMassFromParamsCubicSandwich.lean`) repackage the anchored cubic sandwich wrappers so that callers receive, for the same HLS constant `K`, the convolution estimate, the named `Lemma_17_5_2_UpperBound` predicate, and the displayed two-sided `ofReal m⁻ ≤ latticeMass ≤ C m⁻` sandwich. The interval tanh-profile capstone keeps the final external analytic input to the derivative-limit hypothesis while obtaining the active range and lower profile from pointwise `cubicTanhProfileBound` on `Icc β₁ β₂`. Reference: Glimm--Jaffe, 2nd ed., §17.5 Theorem 17.5.1 and Lemma 17.5.2, pp. 311--312. |
 | §17.7 | `η ≥ 0`, `ζ ≥ 0` | **Done (finite + ∞-vol)** | `eta_nonneg_finite_vol` + `zeta_nonneg_finite_vol` (`PhaseTransition.lean`) + `Ambient.eta_nonneg_infinite_vol` + `Ambient.zeta_nonneg_infinite_vol` (`AmbientLattice.lean`) + ℤ^d `{eta,zeta}_nonneg_{finite,infinite}_vol_latticeGraph`. Explicit named aliases of `truncated2_nonneg`/`truncated2Infinite_nonneg` (GKS-II) and `cor_4_3_3`/`truncated4Infinite_nonpos_h_zero` (Lebowitz at `h = 0`). (PR #636.) |
 | §17.8 | Coupling derivative formula (Step 135) | **Done** | `scaledBoltzmannWeight G E₀ p s σ`: Boltzmann weight with E₀-bonds scaled by s (s=0: no E₀; s=1: full). `hasDerivAt_scaledBoltzmannWeight`: `d/ds w_s(σ) = β·J·(Σ_{E₀}σₑ)·w_s(σ)`. `hasDerivAt_scaledPartitionFunction`, `hasDerivAt_scaledCorrelation`: `d/ds ⟨σ^A⟩_s = β·J·Σ_{e=(u,v)∈E₀}(⟨σ^{AΔ{u,v}}⟩_s − ⟨σ^A⟩_s·⟨σ^{u,v}⟩_s)`. Reference: GJ §17.8 pp. 316–318. (PR #952 Step 135, Issue #951.) |
-| §17.8 | Ball-boundary Simon-Lieb inequality (Step 136) | **Done** | GKS-I for scaled model (`scaledCorrelation_nonneg`), GKS-II for scaled model (`scaledCorrelation_gks_second`, duplicate-variable trick), monotonicity in s (`scaledCorrelation_monotoneOn`). `ball_boundary_simon_lieb`: `⟨σ_r σ_s⟩ ≤ β·J·Σ_{(k,l)∈E₀}[⟨σ_r σ_k⟩·⟨σ_s σ_l⟩ + ⟨σ_r σ_l⟩·⟨σ_s σ_k⟩ + ⟨σ_r σ_s⟩·⟨σ_k σ_l⟩]`. Tight form `ball_boundary_simon_lieb_tight` (no extra term, uses `cor_4_3_3_scaled` axiom). `scaledCorrelation_odd_vanish` (h=0 → odd-card vanish for scaled model). The mean-value step of `ball_boundary_simon_lieb` is extracted separately as `scaledCorrelation_one_sub_zero_le_derivBound` (without the disconnection/vanishing hypothesis): `scaledCorrelation G E₀ p 1 {r,s} − scaledCorrelation G E₀ p 0 {r,s} ≤ derivBound G E₀ p r s`, bounding the *difference* between two finite-volume systems differing only on boundary edges `E₀` — the finite-volume coupling step toward the per-stage correlation increment bound for the volume-convergence rate (Issue #2965, Phase A). The `s = 0` system is identified concretely with the **bond-deleted** model: `scaledBoltzmannWeight_zero`, `scaledPartitionFunction_zero`, `scaledGibbsExpectation_zero`, and `scaledCorrelation_zero` (all in `CouplingDerivative.lean`) prove that at `s = 0` the scaling factor `exp(−β·J·∑_{e∈E₀} σ_e)` exactly cancels the `E₀` edges' Hamiltonian contribution (for `E₀ ⊆ G.edgeFinset`), so `scaledCorrelation G E₀ p 0 A = correlation (G.deleteEdges ↑E₀) p A` — the free-boundary model on the sub-graph with the `E₀` bonds removed (via `SimpleGraph.edgeFinset_deleteEdges` and `Finset.sum_sdiff`). This makes the ball-boundary disconnection (`scaledCorrelation_at_zero_of_sep`) concrete and is the conceptual basis for the finite-volume-stage coupling toward the volume-convergence rate. Reference: GJ §17.8 pp. 316–318. (PRs #953, #954 Steps 136–137, Issue #951; #2972, #2973 Issue #2965.) |
+| §17.8 | Ball-boundary Simon-Lieb inequality (Step 136) | **Done** | GKS-I for scaled model (`scaledCorrelation_nonneg`), GKS-II for scaled model (`scaledCorrelation_gks_second`, duplicate-variable trick), monotonicity in s (`scaledCorrelation_monotoneOn`). `ball_boundary_simon_lieb`: `⟨σ_r σ_s⟩ ≤ β·J·Σ_{(k,l)∈E₀}[⟨σ_r σ_k⟩·⟨σ_s σ_l⟩ + ⟨σ_r σ_l⟩·⟨σ_s σ_k⟩ + ⟨σ_r σ_s⟩·⟨σ_k σ_l⟩]`. Tight form `ball_boundary_simon_lieb_tight` (no extra term, uses `cor_4_3_3_scaled` axiom). `scaledCorrelation_odd_vanish` (h=0 → odd-card vanish for scaled model). The mean-value step of `ball_boundary_simon_lieb` is extracted separately as `scaledCorrelation_one_sub_zero_le_derivBound` (without the disconnection/vanishing hypothesis): `scaledCorrelation G E₀ p 1 {r,s} − scaledCorrelation G E₀ p 0 {r,s} ≤ derivBound G E₀ p r s`, bounding the *difference* between two finite-volume systems differing only on boundary edges `E₀` — the finite-volume coupling step toward the per-stage correlation increment bound for the volume-convergence rate (Issue #2965, Phase A). The `s = 0` system is identified concretely with the **bond-deleted** model: `scaledBoltzmannWeight_zero`, `scaledPartitionFunction_zero`, `scaledGibbsExpectation_zero`, and `scaledCorrelation_zero` (all in `CouplingDerivative.lean`) prove that at `s = 0` the scaling factor `exp(−β·J·∑_{e∈E₀} σ_e)` exactly cancels the `E₀` edges' Hamiltonian contribution (for `E₀ ⊆ G.edgeFinset`), so `scaledCorrelation G E₀ p 0 A = correlation (G.deleteEdges ↑E₀) p A` — the free-boundary model on the sub-graph with the `E₀` bonds removed (via `SimpleGraph.edgeFinset_deleteEdges` and `Finset.sum_sdiff`). This makes the ball-boundary disconnection (`scaledCorrelation_at_zero_of_sep`) concrete and is the conceptual basis for the finite-volume-stage coupling toward the volume-convergence rate. Combining the difference bound with the bond-deleted identification, `correlation_sub_deleteEdges_le_derivBound` (`WeakBound.lean`) gives the increment entirely in standard-correlation terms: `correlation G p {r,s} − correlation (G.deleteEdges ↑E₀) p {r,s} ≤ derivBound G E₀ p r s` (adding the bonds `E₀` raises `⟨σ_r σ_s⟩` by at most `derivBound`). `correlation_deleteEdges_le` records the matching GKS bond-monotonicity (deleting bonds cannot increase a correlation), so the increment is nonnegative, and `derivBound_le_card` (`derivBound ≤ β·J·(3·|E₀|)`, each correlation product `≤ 1`) yields the coarse a-priori cardinality bound `correlation_sub_deleteEdges_le_card`: `correlation G p {r,s} − correlation (G.deleteEdges ↑E₀) p {r,s} ≤ β·J·(3·|E₀|)`. Reference: GJ §17.8 pp. 316–318. (PRs #953, #954 Steps 136–137, Issue #951; #2972, #2973, #2974 Issue #2965.) |
 | §17.8 | `η ≤ 1` (Thm 17.8.1, Step 137) | **Done** | `HasPolynomialDecay d Λ p` (lim corr{0,x}·\|x\|^{d-1}=0), `latticeBall d r`, `latticeBallBoundaryEdges d r`, `scaledCorrelation_at_zero_of_sep` (**theorem**, PR #956 Step 138), `ball_boundary_tight_infinite` (axiom), `shellSup_contraction` (axiom), `shellSup_iterated_bound` (**theorem**, induction on k, PR Step 139), `pow_div_le_inv_mul_exp`, `correlationInfinite_polynomial_implies_exponential`: polynomial decay → `HasExponentialDecay`. Zero sorrys. Reference: GJ §17.8 pp. 316–318. (PRs #954 #955 #956 #957 Steps 137–139, Issue #951.) |
 | §17.9 | The Scaling Limit | **Out of scope** | Thm 17.9.1: single-phase φ^4/Ising expectations with uniform 2-pt bound (17.9.1) → subsequential convergence to Euclidean field theory. Requires Schwartz-space norms, Osterwalder-Schrader axioms, and continuum QFT compactness — outside current Lean infrastructure. |
 | §17.10 | Conjecture Γ^(6) ≤ 0 | **Out of scope** | Thm 17.10.1: if Γ^(6)(x,x,x,y,y,y) ≤ 0 then 0 ≤ Γ(x) ≤ e^{-3m\|x\|}. Requires 6-point vertex functions and QFT integration-by-parts. |

tex/proof-guide.tex

@@ -14518,6 +14518,18 @@ \subsection*{Step 137 -- GJ \S17.8 Thm 17.8.1: polynomial decay $\Rightarrow$ ex
   free-boundary correlation on $G.\mathrm{deleteEdges}\,E_0$ (proved via
   \texttt{SimpleGraph.edgeFinset\_deleteEdges} and \texttt{Finset.sum\_sdiff}). This
   makes the ball-boundary disconnection concrete.
+\item \texttt{correlation\_sub\_deleteEdges\_le\_derivBound}: combining the
+  mean-value bound with the bond-deleted identification, the increment is
+  $\langle\sigma_r\sigma_s\rangle_G-\langle\sigma_r\sigma_s\rangle_{G\setminus E_0}
+  \le\mathrm{derivBound}$ (adding the bonds $E_0$ raises $\langle\sigma_r\sigma_s\rangle$
+  by at most $\mathrm{derivBound}$), in standard-correlation terms.
+\item \texttt{correlation\_deleteEdges\_le}: GKS bond-monotonicity --- deleting bonds
+  cannot increase a correlation, so the increment is nonnegative.
+\item \texttt{derivBound\_le\_card} ($\mathrm{derivBound}\le\beta J\cdot 3|E_0|$, each
+  correlation product $\le 1$) and \texttt{correlation\_sub\_deleteEdges\_le\_card}:
+  the coarse a-priori cardinality bound
+  $\langle\sigma_r\sigma_s\rangle_G-\langle\sigma_r\sigma_s\rangle_{G\setminus E_0}
+  \le\beta J\cdot 3|E_0|$.
 \end{itemize}
 
 \noindent\textbf{Proof sketch.}