feat: scaledCorrelation difference bound (boundary MVT step, no separation) — #2965 (#2972)

* feat: scaledCorrelation one-sub-zero diff bound (Part of #2965)

* feat: extract scaledCorrelation difference bound (boundary MVT step)

Add scaledCorrelation_one_sub_zero_le_derivBound, the mean-value step of
ball_boundary_simon_lieb 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

This bounds the difference between two finite-volume systems differing only
on boundary edges E₀ — the finite-volume coupling step (Phase A) toward the
per-stage correlation increment bound for the volume-convergence rate.

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

@@ -148,5 +148,60 @@ theorem ball_boundary_simon_lieb (G : SimpleGraph ι) [Fintype G.edgeSet]
       Real.norm_of_nonneg (derivBound_nonneg G E₀ p hf r s)] at hmvt
   linarith
 
+/-- **Ball-boundary scaled-correlation difference bound** (the mean-value step of
+`ball_boundary_simon_lieb`, without the separation/vanishing hypothesis): for a
+ferromagnetic model at `h = 0` and an edge subset `E₀` avoiding the pair `{r,s}`,
+the difference between the full pair correlation (`s = 1`) and the
+boundary-removed scaled correlation (`s = 0`) is bounded by the boundary edge sum:
+
+  `scaledCorrelation G E₀ p 1 {r,s} − scaledCorrelation G E₀ p 0 {r,s}
+     ≤ derivBound G E₀ p r s`.
+
+This is exactly the MVT estimate inside `ball_boundary_simon_lieb` before the
+disconnection step is used; it bounds the *difference* of two systems that
+differ only on the boundary edges `E₀` — the finite-volume coupling step for the
+volume-convergence rate (Issue #2965, Phase A), without requiring `r, s` to be
+disconnected at `s = 0`. -/
+theorem scaledCorrelation_one_sub_zero_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) :
+    scaledCorrelation G E₀ p 1 {r, s} - scaledCorrelation G E₀ p 0 {r, s}
+      ≤ derivBound 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‖ ≤
+      ‖derivBound 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 (derivBound_nonneg G E₀ p hf r s)]
+    exact scaledCorrelation_pair_deriv_le_derivBound 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 (derivBound_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
+    _ ≤ derivBound G E₀ p r s := hmvt
+
 
 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). Reference: GJ §17.8 pp. 316–318. (PRs #953, #954 Steps 136–137, 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). Reference: GJ §17.8 pp. 316–318. (PRs #953, #954 Steps 136–137, Issue #951; #2972 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

@@ -14495,6 +14495,12 @@ \subsection*{Step 137 -- GJ \S17.8 Thm 17.8.1: polynomial decay $\Rightarrow$ ex
 \item \texttt{ball\_boundary\_simon\_lieb\_tight}: tight ball-boundary bound
   (no extra $\langle\sigma_r\sigma_s\rangle\cdot\langle\sigma_k\sigma_l\rangle$ term),
   using \texttt{cor\_4\_3\_3\_scaled}.
+\item \texttt{scaledCorrelation\_one\_sub\_zero\_le\_derivBound}: the mean-value step of
+  \texttt{ball\_boundary\_simon\_lieb} extracted without the disconnection/vanishing
+  hypothesis, $\langle\sigma_r\sigma_s\rangle_{s=1}-\langle\sigma_r\sigma_s\rangle_{s=0}
+  \le \mathrm{derivBound}$, bounding the difference between two finite-volume systems
+  differing only on the boundary edges $E_0$ (the finite-volume coupling step toward
+  the per-stage correlation increment for the volume-convergence rate, Issue \#2965).
 \item \texttt{scaledCorrelation\_at\_zero\_of\_sep} (axiom): when $E_0$ separates $r$ from $s$
   and $h=0$, $\langle\sigma_r\sigma_s\rangle_{s=0}=0$.
 \item \texttt{latticeBall d r}, \texttt{latticeBallBoundaryEdges d r}: lattice ball and