feat: straddle-set no-cross + not-internal facts — #2965 (#2982)

* feat: straddle-set no-cross + not-internal facts (Part of #2965)

* feat: straddle-set no-cross + not-internal facts

Add two graph-level facts about the straddle (cut) edge set of
induce_sum_map_sumCompl_eq_deleteEdges:

- straddle_not_mem_of_same_side: p a ↔ p b ⇒ s(a,b) ∉ straddle (the deleted set
  contains no same-side edge), feeding inducedGraph_deleteEdges_eq_of_not_internal.
- deleteEdges_straddle_no_cross: p a, ¬p b ⇒ ¬(G.deleteEdges {straddle}).Adj a b
  (the bond-deleted graph disconnects the two sides), the no-cross hypothesis for
  correlation_inducedGraph_union_inl_of_no_cross applied to G.deleteEdges {straddle}.

Pure adjacency facts (no Fintype), bridging #2979/#2981/#2978 toward the
bond-deletion → isolated-component capstone via the working inducedGraph route.

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/SumGraph.lean

@@ -165,4 +165,28 @@ theorem induce_sum_map_sumCompl_eq_deleteEdges (p : V → Prop) [DecidablePred p
     · 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⟩
 
+/-- The "straddle" deleted set (edges with endpoints on different sides of `p`)
+of `induce_sum_map_sumCompl_eq_deleteEdges` contains no edge whose endpoints lie
+on the *same* side of `p`. Hence removing it never deletes an edge internal to a
+side — the hypothesis required by `inducedGraph_deleteEdges_eq_of_not_internal`. -/
+theorem straddle_not_mem_of_same_side (p : V → Prop) {a b : V} (h : p a ↔ p b) :
+    s(a, b) ∉ {e : Sym2 V |
+      ¬ Sym2.lift ⟨fun a b => (p a ↔ p b), fun a b => by simp [iff_comm]⟩ e} := by
+  simp only [Set.mem_setOf_eq, Sym2.lift_mk, not_not]
+  exact h
+
+/-- The bond-deleted (straddle-removed) graph has no edge between the two sides of
+`p`: deleting the cut edges disconnects `{a | p a}` from `{a | ¬ p a}`. This is
+the no-cross hypothesis required by `correlation_inducedGraph_union_inl_of_no_cross`
+applied to `G.deleteEdges {straddling edges}`. -/
+theorem deleteEdges_straddle_no_cross (G : SimpleGraph V) (p : V → Prop)
+    {a b : V} (ha : p a) (hb : ¬ p b) :
+    ¬ (G.deleteEdges {e : Sym2 V |
+        ¬ Sym2.lift ⟨fun a b => (p a ↔ p b), fun a b => by simp [iff_comm]⟩ e}).Adj a b := by
+  rw [SimpleGraph.deleteEdges_adj]
+  rintro ⟨_, hmem⟩
+  refine hmem ?_
+  simp only [Set.mem_setOf_eq, Sym2.lift_mk]
+  exact fun h => hb (h.mp ha)
+
 end SimpleGraph

docs/index.md

@@ -351,6 +351,7 @@ Named specializations at `A = {i}`:
 | `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) |
+| `straddle_not_mem_of_same_side` / `deleteEdges_straddle_no_cross` | The straddle set contains no same-side edge (`p a ↔ p b ⇒ s(a,b) ∉ straddle`), so deleting it is non-internal (feeds `inducedGraph_deleteEdges_eq_of_not_internal`); and `G.deleteEdges {straddle}` has no edge between `{p}` and `{¬p}` (`p a, ¬p b ⇒ ¬Adj`), the no-cross hypothesis for `correlation_inducedGraph_union_inl_of_no_cross` applied to the bond-deleted graph | `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

@@ -12249,6 +12249,23 @@ \subsection{Edge-set decomposition for disjoint sum graphs (\texttt{SumGraph.lea
 across a partition yields two independent subsystems.
 \end{proof}
 
+\begin{proposition}[\texttt{straddle\_not\_mem\_of\_same\_side} /
+\texttt{deleteEdges\_straddle\_no\_cross}]
+The straddle set contains no same-side edge: if $p\,a \leftrightarrow p\,b$ then
+$s(a,b)$ is not deleted (feeds
+\texttt{inducedGraph\_deleteEdges\_eq\_of\_not\_internal}). Dually, the
+bond-deleted graph has no edge between the two sides: if $p\,a$ and $\neg p\,b$
+then $G.\mathrm{deleteEdges}\,\{\text{straddle}\}$ has no $a\sim b$ edge (the
+no-cross hypothesis for \texttt{correlation\_inducedGraph\_union\_inl\_of\_no\_cross}
+applied to the bond-deleted graph).
+\end{proposition}
+
+\begin{proof}
+Both unfold the straddle membership $s(a,b)\in\{e\mid\neg(p\!\leftrightarrow\!p)(e)\}
+\Leftrightarrow \neg(p\,a\leftrightarrow p\,b)$ and the deleteEdges adjacency
+$\mathrm{Adj}\wedge s(a,b)\notin\{\dots\}$.
+\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