feat: inducedGraph unaffected by deleting non-internal edges — #2965

IsingModel/AmbientLatticeSum/InducedUnion.lean

@@ -300,4 +300,25 @@ theorem correlation_inducedGraph_union_inl_of_no_cross (G : SimpleGraph V)
         (Equiv.Finset.union Λ₁ Λ₂ hd).toEmbedding))
     (correlation_inducedGraph_sum_map_inl G hd p A)
 
+omit [DecidableEq V] in
+/-- **Deleting non-internal edges leaves the induced subgraph unchanged**: if no
+edge in the deleted set `D` has both endpoints in `S`, then
+`inducedGraph (G.deleteEdges D) S = inducedGraph G S`. An edge of the induced
+subgraph on `S` joins two vertices of `S`, so it lies inside `S` and is never
+among the deleted edges `D`.
+
+For the finite-volume coupling step (Issue #2965, Phase A): deleting the cut
+(cross) edges between a region `S` and its complement does not alter the
+correlations *inside* `S`, so the induced subgraph on `S` of the bond-deleted
+model coincides with the induced subgraph on `S` of the original model. -/
+theorem inducedGraph_deleteEdges_eq_of_not_internal (G : SimpleGraph V)
+    (D : Set (Sym2 V)) (S : Finset V)
+    (hD : ∀ a ∈ S, ∀ b ∈ S, s(a, b) ∉ D) :
+    inducedGraph (G.deleteEdges D) S = inducedGraph G S := by
+  ext a b
+  rw [inducedGraph_apply, inducedGraph_apply, SimpleGraph.induce_adj,
+      SimpleGraph.induce_adj, SimpleGraph.deleteEdges_adj]
+  exact ⟨fun h => h.1,
+    fun h => ⟨h, hD _ (Finset.mem_coe.mp a.2) _ (Finset.mem_coe.mp b.2)⟩⟩
+
 end IsingModel

docs/index.md

@@ -367,6 +367,7 @@ Named specializations at `A = {i}`:
 | `correlation_inducedGraph_sum_map_inl` | `correlation ((inducedGraph Λ₁ ⊕g inducedGraph Λ₂).map union) p ((A.map inl).map union) = correlation (inducedGraph Λ₁) p A` (component factorization of an induced-union correlation; by `correlation_map_equiv` + `correlation_sum_inl`) | `InducedUnion.lean` | Component split (Issue #2965) |
 | `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) |
 | `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

@@ -12579,6 +12579,24 @@ \subsection{Super-additivity on Finset disjoint union
 \texttt{rw}.
 \end{proof}
 
+\begin{proposition}[\texttt{IsingModel.inducedGraph\_deleteEdges\_eq\_of\_not\_internal}]
+If no edge of the deleted set $D$ has both endpoints in $S$, then
+\[
+  \mathrm{inducedGraph}\,(G.\mathrm{deleteEdges}\,D)\,S
+    = \mathrm{inducedGraph}\,G\,S.
+\]
+\end{proposition}
+
+\begin{proof}
+An edge of the induced subgraph on $S$ joins two vertices of $S$, hence lies
+inside $S$ and is never among $D$ (by hypothesis); so the induce-adjacency is
+unchanged by the deletion. This is the Finset route to the bond-deletion
+$\to$ isolated-component bridge: deleting the cut edges between $S$ and its
+complement leaves the within-$S$ induced subgraph (hence its correlations)
+intact, and the bond-deleted graph then has no cross edges, so
+\texttt{correlation\_inducedGraph\_union\_inl\_of\_no\_cross} applies to it.
+\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