feat: identify scaledCorrelation at s=0 with bond-deleted model — #2965 (#2973)

phasetr · claude · web-flow · commit da407f8e9ca1 · 2026-05-26T21:39:20.000+09:00
* feat: identify scaledCorrelation at s=0 with bond-deleted model (Part of #2965) * feat: identify scaledCorrelation at s=0 with bond-deleted model Add scaledBoltzmannWeight_zero / scaledPartitionFunction_zero / scaledGibbsExpectation_zero / scaledCorrelation_zero: 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 i.e. the free-boundary model on the sub-graph with E₀ bonds removed (via SimpleGraph.edgeFinset_deleteEdges and Finset.sum_sdiff). This makes the ball-boundary disconnection concrete and is the conceptual basis for the finite-volume-stage coupling toward the volume-convergence rate. Part of #2965 Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com> * docs: fix proof-guide attribution for s=0 bond-deleted lemmas (#2965) Move scaledCorrelation_zero supporting-material bullet out of the legacy 'PR #954' itemize into its own Issue #2965 paragraph (codex cross-check fix). Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com> --------- Co-authored-by: Claude Opus 4.7 <noreply@anthropic.com>
diff --git a/IsingModel/CouplingDerivative.lean b/IsingModel/CouplingDerivative.lean
@@ -1,5 +1,6 @@
 import IsingModel.GibbsMeasure
 import IsingModel.BetaDerivative
+import Mathlib.Combinatorics.SimpleGraph.DeleteEdges
 import Mathlib.Analysis.Calculus.Deriv.Add
 import Mathlib.Analysis.Calculus.Deriv.Mul
 import Mathlib.Analysis.Calculus.Deriv.Comp
@@ -98,6 +99,61 @@ theorem scaledCorrelation_one (G : SimpleGraph ι) [Fintype G.edgeSet]
   simp [scaledCorrelation, scaledGibbsExpectation, scaledPartitionFunction,
         scaledBoltzmannWeight_one, correlation, gibbsExpectation, partitionFunction]
 
+/-! ## The `s = 0` system is the bond-deleted model -/
+
+omit [DecidableEq ι] in
+/-- At `s = 0`: the scaled Boltzmann weight equals the Boltzmann weight of the
+**bond-deleted** graph `G.deleteEdges ↑E₀` (the `E₀` couplings switched off).
+The scaling factor `exp(−β·J·∑_{e∈E₀} σ_e)` exactly cancels the `E₀` edges'
+contribution to the Hamiltonian, since `E₀ ⊆ G.edgeFinset`. -/
+theorem scaledBoltzmannWeight_zero (G : SimpleGraph ι) [Fintype G.edgeSet]
+    (E₀ : Finset (Sym2 ι)) (hE₀_sub : E₀ ⊆ G.edgeFinset)
+    (p : IsingParams ℝ) (σ : Config ι)
+    [Fintype (G.deleteEdges ↑E₀).edgeSet] :
+    scaledBoltzmannWeight G E₀ p 0 σ = boltzmannWeight (G.deleteEdges ↑E₀) p σ := by
+  classical
+  have hsum : (∑ e ∈ (G.deleteEdges ↑E₀).edgeFinset, edgeSpin (K := ℝ) σ e)
+      + ∑ e ∈ E₀, edgeSpin (K := ℝ) σ e
+      = ∑ e ∈ G.edgeFinset, edgeSpin (K := ℝ) σ e := by
+    rw [SimpleGraph.edgeFinset_deleteEdges]
+    exact Finset.sum_sdiff hE₀_sub
+  rw [scaledBoltzmannWeight, boltzmannWeight, boltzmannWeight, ← Real.exp_add]
+  congr 1
+  simp only [hamiltonian, interactionEnergy, externalFieldEnergy]
+  linear_combination (-(p.β * p.J)) * hsum
+
+/-- At `s = 0`: the scaled partition function equals the partition function of the
+bond-deleted graph `G.deleteEdges ↑E₀`. -/
+theorem scaledPartitionFunction_zero (G : SimpleGraph ι) [Fintype G.edgeSet]
+    (E₀ : Finset (Sym2 ι)) (hE₀_sub : E₀ ⊆ G.edgeFinset)
+    (p : IsingParams ℝ) [Fintype (G.deleteEdges ↑E₀).edgeSet] :
+    scaledPartitionFunction G E₀ p 0 = partitionFunction (G.deleteEdges ↑E₀) p := by
+  unfold scaledPartitionFunction partitionFunction
+  exact Finset.sum_congr rfl fun σ _ => scaledBoltzmannWeight_zero G E₀ hE₀_sub p σ
+
+/-- At `s = 0`: the scaled Gibbs expectation equals the Gibbs expectation of the
+bond-deleted graph `G.deleteEdges ↑E₀`. -/
+theorem scaledGibbsExpectation_zero (G : SimpleGraph ι) [Fintype G.edgeSet]
+    (E₀ : Finset (Sym2 ι)) (hE₀_sub : E₀ ⊆ G.edgeFinset)
+    (p : IsingParams ℝ) (F : Config ι → ℝ) [Fintype (G.deleteEdges ↑E₀).edgeSet] :
+    scaledGibbsExpectation G E₀ p 0 F = gibbsExpectation (G.deleteEdges ↑E₀) p F := by
+  unfold scaledGibbsExpectation gibbsExpectation
+  rw [scaledPartitionFunction_zero G E₀ hE₀_sub p]
+  congr 1
+  exact Finset.sum_congr rfl fun σ _ => by
+    rw [scaledBoltzmannWeight_zero G E₀ hE₀_sub p σ]
+
+/-- At `s = 0`: the scaled correlation equals the correlation of the bond-deleted
+graph `G.deleteEdges ↑E₀`. This makes the `s = 0` system concrete: removing the
+`E₀` bonds yields the free-boundary model on the sub-graph, the conceptual basis
+for the ball-boundary disconnection arguments. -/
+theorem scaledCorrelation_zero (G : SimpleGraph ι) [Fintype G.edgeSet]
+    (E₀ : Finset (Sym2 ι)) (hE₀_sub : E₀ ⊆ G.edgeFinset)
+    (p : IsingParams ℝ) (A : Finset ι) [Fintype (G.deleteEdges ↑E₀).edgeSet] :
+    scaledCorrelation G E₀ p 0 A = correlation (G.deleteEdges ↑E₀) p A := by
+  unfold scaledCorrelation correlation
+  exact scaledGibbsExpectation_zero G E₀ hE₀_sub p (spinProduct A)
+
 /-! ## Derivative of Boltzmann weight -/
 
 omit [DecidableEq ι] in
diff --git a/docs/index.md b/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). Reference: GJ §17.8 pp. 316–318. (PRs #953, #954 Steps 136–137, Issue #951; #2972 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. Reference: GJ §17.8 pp. 316–318. (PRs #953, #954 Steps 136–137, Issue #951; #2972, #2973 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. |
diff --git a/tex/proof-guide.tex b/tex/proof-guide.tex
@@ -14507,6 +14507,19 @@ \subsection*{Step 137 -- GJ \S17.8 Thm 17.8.1: polynomial decay $\Rightarrow$ ex
   boundary bond set definitions.
 \end{itemize}
 
+\noindent\textbf{The $s=0$ system as the bond-deleted model (Issue \#2965).}
+\begin{itemize}
+\item \texttt{scaledCorrelation\_zero} (with \texttt{scaledBoltzmannWeight\_zero},
+  \texttt{scaledPartitionFunction\_zero}, \texttt{scaledGibbsExpectation\_zero}): the
+  $s=0$ system is the \emph{bond-deleted} model. For $E_0\subseteq G.\mathrm{edgeFinset}$
+  the scaling factor $\exp(-\beta J\sum_{e\in E_0}\sigma_e)$ exactly cancels the $E_0$
+  edges' Hamiltonian contribution, so
+  $\langle\sigma^A\rangle_{s=0}=\langle\sigma^A\rangle_{G\setminus E_0}$, i.e.\ the
+  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.
+\end{itemize}
+
 \noindent\textbf{Proof sketch.}
 Choose $R$ large so that $\alpha^{-1}:=\beta J\sum_{k\in\partial B_R}\langle\sigma_0\sigma_k\rangle_\infty<1$
 (possible by polynomial decay). Apply \texttt{scaledCorrelation\_at\_zero\_of\_sep} (origin inside $B_R$,
