feat: deleteEdges-straddling = induce sumCompl disjoint sum — #2965

IsingModel/SumGraph.lean

@@ -1,5 +1,7 @@
 import Mathlib.Combinatorics.SimpleGraph.Sum
 import Mathlib.Combinatorics.SimpleGraph.Finite
+import Mathlib.Combinatorics.SimpleGraph.DeleteEdges
+import Mathlib.Logic.Equiv.Sum
 
 /-!
 # Edge-set decomposition for the disjoint sum graph
@@ -135,4 +137,32 @@ theorem card_edgeFinset_sum [Fintype G.edgeSet] [Fintype H.edgeSet] :
       Finset.card_union_of_disjoint (disjoint_inl_inr_edgeFinset G H),
       Finset.card_map, Finset.card_map]
 
+/-- **Deleting the edges that straddle a predicate `p` decomposes `G` into a
+disjoint sum of the two induced subgraphs.** Up to the relabeling
+`Equiv.sumCompl p : {a // p a} ⊕ {a // ¬p a} ≃ V`, the graph obtained by removing
+every edge whose endpoints lie on different sides of `p` equals the disjoint sum
+`G.induce {a | p a} ⊕g G.induce {a | ¬p a}`.
+
+This is the structural identity behind the component factorization of a fully
+separated (bond-deleted) finite-volume Ising system: deleting the bonds across a
+cut yields two independent subsystems (Issue #2965, Phase A). -/
+theorem induce_sum_map_sumCompl_eq_deleteEdges (p : V → Prop) [DecidablePred p] :
+    ((G.induce {a | p a}).sum (G.induce {a | ¬ p a})).map (Equiv.sumCompl p).toEmbedding
+      = G.deleteEdges {e : Sym2 V |
+          ¬ Sym2.lift ⟨fun a b => (p a ↔ p b), fun a b => by simp [iff_comm]⟩ e} := by
+  ext a b
+  rw [SimpleGraph.map_adj, SimpleGraph.deleteEdges_adj]
+  simp only [Set.mem_setOf_eq, Sym2.lift_mk, not_not]
+  constructor
+  · rintro ⟨x, y, hxy, rfl, rfl⟩
+    rcases x with ⟨x, hx⟩ | ⟨x, hx⟩ <;> rcases y with ⟨y, hy⟩ | ⟨y, hy⟩
+    · exact ⟨hxy, iff_of_true hx hy⟩
+    · exact Bool.noConfusion hxy
+    · exact Bool.noConfusion hxy
+    · exact ⟨hxy, iff_of_false hx hy⟩
+  · rintro ⟨hadj, hiff⟩
+    by_cases hp : p a
+    · exact ⟨Sum.inl ⟨a, hp⟩, Sum.inl ⟨b, hiff.mp hp⟩, hadj, rfl, rfl⟩
+    · exact ⟨Sum.inr ⟨a, hp⟩, Sum.inr ⟨b, fun h => hp (hiff.mpr h)⟩, hadj, rfl, rfl⟩
+
 end SimpleGraph

docs/index.md

@@ -350,6 +350,7 @@ Named specializations at `A = {i}`:
 | `edgeSet_sum` | Edge-set decomposition of `G ⊕g H` | `SumGraph.lean` | Disjoint-sum lemma |
 | `disjoint_inl_inr_edgeSet` / `disjoint_inl_inr_edgeFinset` | Set / Finset disjointness of the two images | `SumGraph.lean` | Disjoint-sum lemma |
 | `card_edgeFinset_sum` | `#(G ⊕g H).edgeFinset = #G.edgeFinset + #H.edgeFinset` | `SumGraph.lean` | Disjoint-sum lemma |
+| `induce_sum_map_sumCompl_eq_deleteEdges` | `((G.induce {p}) ⊕g (G.induce {¬p})).map (Equiv.sumCompl p) = G.deleteEdges {straddling edges}`: deleting every edge whose endpoints lie on different sides of a predicate `p` decomposes `G` into the disjoint sum of the two induced subgraphs. The structural identity behind component factorization of a bond-deleted (cut) system | `SumGraph.lean` | Component split (Issue #2965) |
 | `Config.sumEquiv` | `Config (ι ⊕ ι') ≃ Config ι × Config ι'` | `SumModel.lean` | Ising on sum graph |
 | `interactionEnergy_sum` / `externalFieldEnergy_sum` | Per-summand additivity of the Hamiltonian's interaction / field contributions on `G ⊕g H` | `SumModel.lean` | Ising on sum graph |
 | `hamiltonian_sum` (§4.6 super-add. Step 2-3) | `hamiltonian (G ⊕g H) p (Sum.elim σ₁ σ₂) = hamiltonian G p σ₁ + hamiltonian H p σ₂` | `SumModel.lean` | Ising on sum graph |

tex/proof-guide.tex

@@ -12226,6 +12226,29 @@ \subsection{Edge-set decomposition for disjoint sum graphs (\texttt{SumGraph.lea
 $\mathrm{Embedding.sym2Map}$.
 \end{proof}
 
+\begin{proposition}[\texttt{SimpleGraph.induce\_sum\_map\_sumCompl\_eq\_deleteEdges} (Issue \#2965)]
+For a predicate $p$ on the vertices, deleting every edge whose endpoints lie on
+different sides of $p$ decomposes $G$ into the disjoint sum of the two induced
+subgraphs, up to the relabeling $\mathrm{Equiv.sumCompl}\,p
+: \{a\mid p\,a\}\oplus\{a\mid\neg p\,a\}\simeq V$:
+\[
+  \bigl((G\,\mathrm{induce}\,\{a\mid p\,a\})
+    \oplus_g (G\,\mathrm{induce}\,\{a\mid\neg p\,a\})\bigr)
+    .\mathrm{map}\,(\mathrm{Equiv.sumCompl}\,p)
+  = G.\mathrm{deleteEdges}\,\{e\mid e\text{ straddles }p\}.
+\]
+\end{proposition}
+
+\begin{proof}
+By edge extensionality: an edge $a\sim b$ survives the deletion iff
+$G.\mathrm{Adj}\,a\,b$ and $a,b$ are on the same side of $p$, which is exactly
+the adjacency of the transported disjoint sum (the $\mathrm{inl}$/$\mathrm{inr}$
+arms of \texttt{SimpleGraph.sum} for same-side pairs, and $\bot$ for straddling
+pairs). This is the structural identity behind the component factorization of a
+fully separated (bond-deleted) finite-volume Ising system: cutting all bonds
+across a partition yields two independent subsystems.
+\end{proof}
+
 \paragraph{Context.} This file is the combinatorial Step~1 toward the
 Glimm--Jaffe \S 4.6 super-additivity proof of thermodynamic-limit
 convergence of the free-energy density. Subsequent steps