feat: bond-deleted correlation = isolated induced subgraph (Phase A capstone, Finset route) — #2965

IsingModel/AmbientLatticeSum/InducedUnion.lean

@@ -321,4 +321,53 @@ theorem inducedGraph_deleteEdges_eq_of_not_internal (G : SimpleGraph V)
   exact ⟨fun h => h.1,
     fun h => ⟨h, hD _ (Finset.mem_coe.mp a.2) _ (Finset.mem_coe.mp b.2)⟩⟩
 
+set_option linter.unusedFintypeInType false in
+/-- **Bond-deleted correlation equals isolated induced-subgraph correlation
+(Finset route)**: for a region `S ⊆ W`, deleting the cut edges between `S` and
+its complement leaves an `S`-supported observable with the same correlation in
+the induced subgraph on `S ∪ Sᶜ` of the bond-deleted model as in the induced
+subgraph on `S` of the *original* model. Assembled entirely from the working
+`inducedGraph`/no-cross machinery:
+`correlation_inducedGraph_union_inl_of_no_cross` (the bond-deleted graph has no
+cross edges by `deleteEdges_straddle_no_cross`) composed with
+`correlation_congr_of_eq` of `inducedGraph_deleteEdges_eq_of_not_internal`
+(deleting cut edges leaves the within-`S` induced subgraph unchanged, by
+`straddle_not_mem_of_same_side`). This is the component-factorization bridge for
+the finite-volume coupling step (Issue #2965, Phase A), realized via the Finset
+route that sidesteps the `Equiv.sumCompl` instance pathology (Issue #2980). -/
+theorem correlation_inducedGraph_deleteEdges_union_inl [Fintype V] (G : SimpleGraph V)
+    (S : Finset V)
+    [Fintype (inducedGraph (G.deleteEdges {e : Sym2 V |
+      ¬ Sym2.lift ⟨fun a b => ((a ∈ S) ↔ (b ∈ S)), fun a b => by simp [iff_comm]⟩ e}) S).edgeSet]
+    [Fintype (inducedGraph (G.deleteEdges {e : Sym2 V |
+      ¬ Sym2.lift ⟨fun a b => ((a ∈ S) ↔ (b ∈ S)), fun a b => by simp [iff_comm]⟩ e}) Sᶜ).edgeSet]
+    [Fintype (((inducedGraph (G.deleteEdges {e : Sym2 V |
+        ¬ Sym2.lift ⟨fun a b => ((a ∈ S) ↔ (b ∈ S)), fun a b => by simp [iff_comm]⟩ e}) S).sum
+        (inducedGraph (G.deleteEdges {e : Sym2 V |
+        ¬ Sym2.lift ⟨fun a b => ((a ∈ S) ↔ (b ∈ S)), fun a b => by simp [iff_comm]⟩ e}) Sᶜ)).map
+      (Equiv.Finset.union S Sᶜ disjoint_compl_right).toEmbedding).edgeSet]
+    [Fintype (inducedGraph (G.deleteEdges {e : Sym2 V |
+      ¬ Sym2.lift ⟨fun a b => ((a ∈ S) ↔ (b ∈ S)), fun a b => by simp [iff_comm]⟩ e})
+      (S ∪ Sᶜ)).edgeSet]
+    [Fintype (inducedGraph G S).edgeSet]
+    (params : IsingParams ℝ) (A : Finset (↑S : Type _)) :
+    correlation (inducedGraph (G.deleteEdges {e : Sym2 V |
+        ¬ Sym2.lift ⟨fun a b => ((a ∈ S) ↔ (b ∈ S)), fun a b => by simp [iff_comm]⟩ e})
+        (S ∪ Sᶜ)) params
+        ((A.map ⟨Sum.inl, Sum.inl_injective⟩).map
+          (Equiv.Finset.union S Sᶜ disjoint_compl_right).toEmbedding)
+      = correlation (inducedGraph G S) params A := by
+  have hcross : ∀ a ∈ S, ∀ b ∈ Sᶜ,
+      ¬ (G.deleteEdges {e : Sym2 V |
+        ¬ Sym2.lift ⟨fun a b => ((a ∈ S) ↔ (b ∈ S)), fun a b => by simp [iff_comm]⟩ e}).Adj a b :=
+    fun a ha b hb =>
+      SimpleGraph.deleteEdges_straddle_no_cross G (· ∈ S) ha (Finset.mem_compl.mp hb)
+  have hD : ∀ a ∈ S, ∀ b ∈ S, s(a, b) ∉ {e : Sym2 V |
+      ¬ Sym2.lift ⟨fun a b => ((a ∈ S) ↔ (b ∈ S)), fun a b => by simp [iff_comm]⟩ e} :=
+    fun a ha b hb => SimpleGraph.straddle_not_mem_of_same_side (· ∈ S) (iff_of_true ha hb)
+  exact (correlation_inducedGraph_union_inl_of_no_cross _ disjoint_compl_right hcross
+        params A).trans
+    (correlation_congr_of_eq
+      (inducedGraph_deleteEdges_eq_of_not_internal G _ S hD) params A)
+
 end IsingModel

docs/index.md

@@ -369,6 +369,7 @@ Named specializations at `A = {i}`:
 | `correlation_congr_of_eq` | `G₁ = G₂ ⇒ correlation G₁ p A = correlation G₂ p A` (correlation is invariant under graph equality even across different `Fintype edgeSet` instances; via `edgeFinset = edgeSet` coercion). Bridges propositional graph equalities without `rw`'s motive obstruction | `InducedUnion.lean` | Component split (Issue #2965) |
 | `correlation_inducedGraph_union_inl_of_no_cross` | `Disjoint Λ₁ Λ₂` + no cross edge ⇒ `correlation (inducedGraph (Λ₁ ∪ Λ₂)) p ((A.map inl).map union) = correlation (inducedGraph Λ₁) p A` (the component-factorization bridge directly on `inducedGraph (Λ₁ ∪ Λ₂)`, via `inducedGraph_sum_map_eq_union_of_no_cross` + `correlation_congr_of_eq` + `correlation_inducedGraph_sum_map_inl`) — the form usable for exhaustion stages | `InducedUnion.lean` | Component split (Issue #2965) |
 | `inducedGraph_deleteEdges_eq_of_not_internal` | If no edge of the deleted set `D` has both endpoints in `S`, then `inducedGraph (G.deleteEdges D) S = inducedGraph G S` (deleting cut/cross edges leaves the within-`S` induced subgraph unchanged). Lets the bond-deleted model's induced subgraph on `S` be identified with the original's, so `correlation_inducedGraph_union_inl_of_no_cross` applies to `G.deleteEdges (cross edges)` (whose cut edges are gone, hence no-cross holds) — the Finset route to the bond-deletion → isolated-component bridge (Issue #2965, Phase A) | `InducedUnion.lean` | Component split (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 |
 | `Ambient.card_mul_freeEnergyΛ_le_of_disjoint_union` | `Λ₁.Nonempty, Disjoint Λ₁ Λ₂ ⇒ |Λ₁|·f_{Λ₁} ≤ |Λ₁∪Λ₂|·f_{Λ₁∪Λ₂}` (ferromagnetic) | `AmbientLatticeSum.lean` | `freeEnergyΛ` weighted monotonicity |

tex/proof-guide.tex

@@ -12614,6 +12614,32 @@ \subsection{Super-additivity on Finset disjoint union
 \texttt{correlation\_inducedGraph\_union\_inl\_of\_no\_cross} applies to it.
 \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
+gives, for any $S$-supported observable $A$,
+\[
+  \langle\sigma^{A}\rangle_{\mathrm{inducedGraph}\,(G.\mathrm{deleteEdges}\,\{\text{straddle }S\})\,(S\cup S^{c})}
+    = \langle\sigma^{A}\rangle_{\mathrm{inducedGraph}\,G\,S},
+\]
+i.e.\ the bond-deleted model's correlation of an $S$-internal observable equals
+the correlation in the isolated induced subgraph on $S$ of the \emph{original}
+model.
+\end{theorem}
+
+\begin{proof}
+Compose \texttt{correlation\_inducedGraph\_union\_inl\_of\_no\_cross} (the
+bond-deleted graph has no cross edges, by \texttt{deleteEdges\_straddle\_no\_cross})
+with \texttt{correlation\_congr\_of\_eq} of
+\texttt{inducedGraph\_deleteEdges\_eq\_of\_not\_internal} (deleting the cut leaves
+the within-$S$ induced subgraph unchanged, by
+\texttt{straddle\_not\_mem\_of\_same\_side}). This realizes the component
+factorization via the Finset/\texttt{inducedGraph} route, sidestepping the
+\texttt{Equiv.sumCompl} instance pathology. Combined with the ball-boundary
+bond-deletion increment \texttt{correlation\_sub\_deleteEdges\_le\_derivBound}, it
+yields the per-stage exhaustion increment bound (Issue \#2965, Phase A).
+\end{proof}
+
 \paragraph{Closing Prop 4.6.1.} Combined with the uniform upper
 bound (PR \#122, \#123), Fekete's lemma now yields
 convergence of $f_\Lambda = (\log Z_\Lambda)/|\Lambda|$ along