feat: numeric per-stage correlation increment (Phase A) — #2965

IsingModel/AmbientLatticeSum/PerStageIncrement.lean

@@ -0,0 +1,115 @@
+import IsingModel.BallBoundarySimonLieb.WeakBound
+import IsingModel.AmbientLatticeSum.InducedUnion
+
+/-!
+# Numeric per-stage correlation increment (Issue #2965, Phase A)
+
+Composes the ball-boundary bond-deletion increment
+`correlation_sub_deleteEdges_le_derivBound` (`WeakBound.lean`) with the
+component-factorization bridge `correlation_deleteEdges_straddle_eq_inducedGraph`
+(`InducedUnion.lean`) to obtain, for a pair `r, s` interior to a region `S`, the
+finite-volume coupling increment between the full model and the isolated induced
+subgraph on `S`:
+
+`correlation G p {r,s} − correlation (inducedGraph G S) p {⟨r,_⟩,⟨s,_⟩}
+  ≤ derivBound G (G.edgeFinset.filter straddle) p r s`.
+
+## Main declaration
+
+* `IsingModel.correlation_pair_sub_inducedGraph_le_derivBound`.
+-/
+
+namespace IsingModel
+
+open Finset Ambient
+
+variable {V : Type*} [Fintype V] [DecidableEq V]
+
+/-- The straddle (cut) predicate for a region `S`: an edge straddles `S` when its
+endpoints lie on different sides of `· ∈ S`. Marked `@[reducible]` so it unfolds
+during instance synthesis / unification to match the inline straddle set of the
+component-factorization lemmas. -/
+@[reducible] private def straddlePred (S : Finset V) : Sym2 V → Prop :=
+  fun e => ¬ Sym2.lift ⟨fun a b => ((a ∈ S) ↔ (b ∈ S)), fun a b => by simp [iff_comm]⟩ e
+
+noncomputable instance (S : Finset V) : DecidablePred (straddlePred S) :=
+  Classical.decPred _
+
+omit [Fintype V] in
+/-- The pair `{⟨r,_⟩, ⟨s,_⟩} : Finset ↥S` maps under the subtype inclusion to the
+raw pair `{r, s} : Finset V`. -/
+private theorem pair_map_val_eq (S : Finset V) {r s : V} (hr : r ∈ S) (hs : s ∈ S) :
+    ({⟨r, hr⟩, ⟨s, hs⟩} : Finset (↑S : Type _)).map ⟨Subtype.val, Subtype.val_injective⟩
+      = ({r, s} : Finset V) := by
+  rw [Finset.map_insert, Finset.map_singleton]
+  rfl
+
+set_option linter.unusedFintypeInType false in
+/-- **Bond-deleted-graph correlation = isolated induced-subgraph correlation** for
+a pair `{r, s}` interior to `S`: composes `deleteEdges_filter_edgeFinset_eq`
+(#2987), `correlation_congr_all` (#2986), the observable identity
+`triple_map_subtypeUnivEquiv_eq` (#2988) / `pair_map_val_eq`, and the
+component-factorization capstone `correlation_deleteEdges_straddle_eq_inducedGraph`
+(#2986). Stated separately from the increment to keep elaboration light. -/
+private theorem correlation_deleteEdges_filter_pair_eq (G : SimpleGraph V)
+    [Fintype G.edgeSet] (S : Finset V) (p : IsingParams ℝ) {r s : V}
+    (hr : r ∈ S) (hs : s ∈ S)
+    [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.deleteEdges ↑(G.edgeFinset.filter (straddlePred S))) p {r, s}
+      = correlation (inducedGraph G S) p {⟨r, hr⟩, ⟨s, hs⟩} := by
+  have hge : G.deleteEdges (↑(G.edgeFinset.filter (straddlePred S)))
+      = G.deleteEdges {e : Sym2 V | straddlePred S e} :=
+    SimpleGraph.deleteEdges_filter_edgeFinset_eq G (straddlePred S)
+  have hobs : ((({⟨r, hr⟩, ⟨s, hs⟩} : Finset (↑S : Type _)).map
+        ⟨Sum.inl, Sum.inl_injective⟩).map
+        (Equiv.Finset.union S Sᶜ disjoint_compl_right).toEmbedding).map
+        (Equiv.subtypeUnivEquiv (p := fun x => x ∈ (↑(S ∪ Sᶜ) : Set V))
+          (fun x => by rw [Finset.union_compl, Finset.coe_univ]; exact Set.mem_univ x)).toEmbedding
+      = ({r, s} : Finset V) := by
+    rw [triple_map_subtypeUnivEquiv_eq, pair_map_val_eq]
+  have h2986 := correlation_deleteEdges_straddle_eq_inducedGraph G S p {⟨r, hr⟩, ⟨s, hs⟩}
+  rw [hobs] at h2986
+  exact (correlation_congr_all hge p {r, s}).trans h2986
+
+set_option linter.unusedFintypeInType false in
+/-- **Numeric per-stage correlation increment**: for a pair `r, s` interior to `S`
+(neither on a cut edge), the full-model pair correlation exceeds the isolated
+induced-subgraph pair correlation by at most the ball-boundary `derivBound` over
+the cut edges. Composes `correlation_sub_deleteEdges_le_derivBound` (#2974) with
+`correlation_deleteEdges_filter_pair_eq`. -/
+theorem correlation_pair_sub_inducedGraph_le_derivBound (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⟩}
+      ≤ derivBound 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_derivBound 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
+
+end IsingModel

docs/index.md

@@ -373,8 +373,9 @@ Named specializations at `A = {i}`:
 | `correlation_induce_univ` | `correlation (G.induce Set.univ) p A = correlation G p (A.map (Equiv.Set.univ V))` — since `G.induce Set.univ ≃g G` (mathlib `induceUnivIso`), pushing the observable along the relabeling preserves the correlation. Connects `inducedGraph _ univ` statements (the left side of `correlation_inducedGraph_deleteEdges_union_inl`) back to the raw graph `G` (the form of `correlation_sub_deleteEdges_le_derivBound`) for the per-stage increment assembly (Issue #2965, Phase A) | `InducedUnion.lean` | Component split (Issue #2965) |
 | `correlation_induce_of_forall_mem` | `(∀ x, x ∈ s) ⇒ correlation (G.induce s) p A = correlation G p (A.map (Equiv.subtypeUnivEquiv hs))` — generalizes `correlation_induce_univ` from `Set.univ` to any full set `s` (via `G.induce s ≃g G`). Applies to `s = ↑(S ∪ Sᶜ)` (full by `Finset.union_compl`), letting the capstone's `inducedGraph _ (S ∪ Sᶜ)` left side connect to the raw bond-deleted graph **without** forcing the propositional `S ∪ Sᶜ = univ` at the type level — the clean route through the per-stage-increment type-transport (Issue #2965, Phase A) | `InducedUnion.lean` | Component split (Issue #2965) |
 | `correlation_congr_all` | `G₁ = G₂ ⇒ @correlation _ inst₁ _ G₁ e₁ p A = @correlation _ inst₂ _ G₂ e₂ p A` — strengthens `correlation_congr_of_eq` to absorb differences in the vertex `Fintype` **and** `edgeSet Fintype` instances, since `Fintype` is `Subsingleton` (`Fintype.subsingleton`). Bridges `Finset.Subtype.fintype` (from `inducedGraph`) vs the `Set`-induce vertex `Fintype` | `InducedUnion.lean` | Component split (Issue #2965) |
-| `correlation_deleteEdges_straddle_eq_inducedGraph` | **Per-stage-increment form.** `correlation (G.deleteEdges {straddle S}) p (((A.map inl).map union).map subtypeUnivEquiv) = correlation (inducedGraph G S) p A` — the *raw* bond-deleted graph's correlation of an `S`-supported observable equals the isolated induced-subgraph correlation. Composes `correlation_induce_of_forall_mem` (on `↑(S∪Sᶜ)`) ∘ `correlation_congr_all` ∘ `correlation_inducedGraph_deleteEdges_union_inl`. Intended to pair with the ball-boundary increment `correlation_sub_deleteEdges_le_derivBound` (#2974) toward the per-stage increment (that composition — finite edge-set, observable reduction to `{r,s}` — not yet formalized) | `InducedUnion.lean` | Component split (Issue #2965) |
+| `correlation_deleteEdges_straddle_eq_inducedGraph` | **Per-stage-increment form.** `correlation (G.deleteEdges {straddle S}) p (((A.map inl).map union).map subtypeUnivEquiv) = correlation (inducedGraph G S) p A` — the *raw* bond-deleted graph's correlation of an `S`-supported observable equals the isolated induced-subgraph correlation. Composes `correlation_induce_of_forall_mem` (on `↑(S∪Sᶜ)`) ∘ `correlation_congr_all` ∘ `correlation_inducedGraph_deleteEdges_union_inl`. Pairs with the ball-boundary increment `correlation_sub_deleteEdges_le_derivBound` (#2974) to give the numeric per-stage increment `correlation_pair_sub_inducedGraph_le_derivBound` (#2989) | `InducedUnion.lean` | Component split (Issue #2965) |
 | `triple_map_subtypeUnivEquiv_eq` | `(((A.map inl).map union).map subtypeUnivEquiv) = A.map ⟨Subtype.val, _⟩` — the triple-mapped `S`-observable (through `Sum.inl`, `Equiv.Finset.union S Sᶜ`, `Equiv.subtypeUnivEquiv`) equals the plain subtype-inclusion image of `A` in `V`. Identifies the observable of `correlation_deleteEdges_straddle_eq_inducedGraph` with the raw `V`-vertex observable (e.g. `{r,s}` for the pair), matching `correlation_sub_deleteEdges_le_derivBound` (Issue #2965, Phase A) | `InducedUnion.lean` | Component split (Issue #2965) |
+| `correlation_pair_sub_inducedGraph_le_derivBound` | **Numeric per-stage correlation increment (Phase A).** For `r,s ∈ S`, `r ≠ s`, ferromagnetic, `h=0`, and `r,s` not on any cut (straddle) edge: `correlation G p {r,s} − correlation (inducedGraph G S) p {⟨r,_⟩,⟨s,_⟩} ≤ derivBound G (G.edgeFinset.filter straddle) p r s`. Composes the ball-boundary bond-deletion increment `correlation_sub_deleteEdges_le_derivBound` (#2974) with the component-factorization bridge `correlation_deleteEdges_straddle_eq_inducedGraph` (#2986) via `deleteEdges_filter_edgeFinset_eq` (#2987) + `correlation_congr_all` + `triple_map_subtypeUnivEquiv_eq` (#2988). The full-model pair correlation exceeds the isolated induced-subgraph pair correlation by at most the boundary `derivBound` over the cut edges | `PerStageIncrement.lean` | Per-stage increment (Issue #2965) |
 | `correlation_inducedGraph_deleteEdges_union_inl` | **Phase A component-factorization capstone (Finset route).** For `S ⊆ W`, deleting the cut edges between `S` and `Sᶜ` gives `correlation (inducedGraph (G.deleteEdges {straddle S}) (S ∪ Sᶜ)) p ((A.map inl).map union) = correlation (inducedGraph G S) p A` — the bond-deleted model's correlation of an `S`-supported observable equals the correlation in the isolated induced subgraph on `S` of the original model. Assembled from `correlation_inducedGraph_union_inl_of_no_cross` ∘ `correlation_congr_of_eq (inducedGraph_deleteEdges_eq_of_not_internal)`, with the no-cross/not-internal hypotheses discharged by `deleteEdges_straddle_no_cross`/`straddle_not_mem_of_same_side`. Sidesteps the `Equiv.sumCompl` instance pathology (Issue #2980) entirely | `InducedUnion.lean` | Component split (Issue #2965) |
 | `partitionFunction_ge_one_of_ferromagnetic` / `log_partitionFunction_nonneg_of_ferromagnetic` | `Z_G ≥ 1` (ferromagnetic), log form | `FreeEnergy.lean` | Step 5/Fekete infra |
 | `{log_,}partitionFunction{,Λ}_inducedGraph_le_of_disjoint_union` | `Disjoint Λ₁ Λ₂ ⇒ Z_{Λ₁} ≤ Z_{Λ₁∪Λ₂}` (ferromagnetic), log / multiplicative and generic / `Λ`-wrapped forms | `AmbientLatticeSum.lean` | Monotonicity step toward Fekete |

tex/proof-guide.tex

@@ -12684,10 +12684,10 @@ \subsection{Super-additivity on Finset disjoint union
 observable equals the isolated induced-subgraph correlation. Composes
 \texttt{correlation\_induce\_of\_forall\_mem} (on the full set
 $\uparrow(S\cup S^{c})$), \texttt{correlation\_congr\_all}, and the
-component-factorization capstone below. It is intended to pair with the
-ball-boundary increment \texttt{correlation\_sub\_deleteEdges\_le\_derivBound}
-toward the per-stage exhaustion increment bound; that composition (finite
-edge-set, observable reduction to the pair $\{r,s\}$) is not yet formalized here.
+component-factorization capstone below. It pairs with the ball-boundary
+increment \texttt{correlation\_sub\_deleteEdges\_le\_derivBound} to give the
+numeric per-stage increment
+\texttt{correlation\_pair\_sub\_inducedGraph\_le\_derivBound} (below).
 \end{theorem}
 
 \begin{proposition}[\texttt{IsingModel.triple\_map\_subtypeUnivEquiv\_eq}]
@@ -12704,9 +12704,39 @@ \subsection{Super-additivity on Finset disjoint union
 match for the per-stage increment; together with
 \texttt{deleteEdges\_filter\_edgeFinset\_eq} and \texttt{correlation\_congr\_all}
 the remaining gap to the numeric increment is only the discharge of the
-ball-boundary hypotheses for the straddle-edge finset.
+ball-boundary hypotheses for the straddle-edge finset (now carried out in the
+theorem below).
 \end{proposition}
 
+\begin{theorem}[\texttt{IsingModel.correlation\_pair\_sub\_inducedGraph\_le\_derivBound}
+(numeric per-stage correlation increment, Issue \#2965 Phase A)]
+For $r,s\in S$, $r\neq s$, ferromagnetic parameters at $h=0$, with $r,s$ on no
+cut (straddle) edge,
+\[
+  \langle\sigma_r\sigma_s\rangle_{G}
+    - \langle\sigma_r\sigma_s\rangle_{\mathrm{inducedGraph}\,G\,S}
+  \le \mathrm{derivBound}\,G\,(G.\mathrm{edgeFinset.filter}\,\mathrm{straddle})\,r\,s,
+\]
+i.e.\ the full-model pair correlation exceeds the isolated induced-subgraph pair
+correlation by at most the ball-boundary $\mathrm{derivBound}$ over the cut edges.
+\end{theorem}
+
+\begin{proof}
+Apply the ball-boundary bond-deletion increment
+\texttt{correlation\_sub\_deleteEdges\_le\_derivBound} with
+$E_0=G.\mathrm{edgeFinset.filter}\,\mathrm{straddle}$ (its hypotheses: edges are
+non-diagonal, $E_0\subseteq G.\mathrm{edgeFinset}$, and the interior hypothesis
+that $r,s$ avoid the cut), then rewrite the bond-deleted correlation via
+\texttt{correlation\_deleteEdges\_filter\_pair\_eq}: by
+\texttt{deleteEdges\_filter\_edgeFinset\_eq} the filtered-finset deletion equals
+the straddle-set deletion, \texttt{correlation\_congr\_all} matches the
+correlations, and \texttt{triple\_map\_subtypeUnivEquiv\_eq} /
+\texttt{pair\_map\_val\_eq} identify the pair observable, so the
+component-factorization capstone applies. Marking the straddle predicate
+\texttt{@[reducible]} and stating the bridge as a separate lemma keeps the
+elaboration within the heartbeat budget.
+\end{proof}
+
 \begin{theorem}[\texttt{IsingModel.correlation\_inducedGraph\_deleteEdges\_union\_inl}
 (Phase A component-factorization capstone, Finset route)]
 For a region $S\subseteq W$, deleting the cut edges between $S$ and its complement