feat: induced-union splits as disjoint sum under no cross edges — #2965

IsingModel/AmbientLatticeSum/InducedUnion.lean

@@ -190,4 +190,62 @@ theorem partitionFunction_inducedGraph_le_of_disjoint_union
     (partitionFunction_pos _ _)).mp
     (log_partitionFunction_inducedGraph_le_of_disjoint_union G hd p hf)
 
+/-- **Induced union splits as a disjoint sum when there are no cross edges**:
+for disjoint `Λ₁, Λ₂ : Finset V` with no `G`-edge between `Λ₁` and `Λ₂`, the
+induced subgraph on the union equals the transported disjoint sum of the two
+induced subgraphs. Upgrades `inducedGraph_sum_map_le_union` to an equality: the
+`≤` direction is that lemma; the `≥` direction holds because, with no cross
+edges, every edge of `inducedGraph G (Λ₁ ∪ Λ₂)` has both endpoints in the same
+part. This is the structural fact behind the component factorization of a
+bond-deleted (fully separated) finite-volume system (Issue #2965, Phase A). -/
+theorem inducedGraph_sum_map_eq_union_of_no_cross (G : SimpleGraph V)
+    {Λ₁ Λ₂ : Finset V} (hd : Disjoint Λ₁ Λ₂)
+    (hcross : ∀ a ∈ Λ₁, ∀ b ∈ Λ₂, ¬ G.Adj a b) :
+    ((inducedGraph G Λ₁).sum (inducedGraph G Λ₂)).map
+        (Equiv.Finset.union Λ₁ Λ₂ hd).toEmbedding
+      = inducedGraph G (Λ₁ ∪ Λ₂) := by
+  refine le_antisymm (inducedGraph_sum_map_le_union G hd) ?_
+  intro a b hab
+  have hGadj : G.Adj (a : V) (b : V) := hab
+  rw [SimpleGraph.map_adj]
+  rcases Finset.mem_union.mp a.2 with ha | ha <;>
+    rcases Finset.mem_union.mp b.2 with hb | hb
+  · exact ⟨Sum.inl ⟨↑a, ha⟩, Sum.inl ⟨↑b, hb⟩, by
+      simpa [SimpleGraph.sum_adj, inducedGraph, SimpleGraph.induce] using hGadj,
+      by simp, by simp⟩
+  · exact absurd hGadj (hcross _ ha _ hb)
+  · exact absurd hGadj.symm (hcross _ hb _ ha)
+  · exact ⟨Sum.inr ⟨↑a, ha⟩, Sum.inr ⟨↑b, hb⟩, by
+      simpa [SimpleGraph.sum_adj, inducedGraph, SimpleGraph.induce] using hGadj,
+      by simp, by simp⟩
+
+set_option linter.unusedFintypeInType false in
+/-- **Component factorization of an induced-union correlation under no cross
+edges** (stated on the transported disjoint sum): for disjoint `Λ₁, Λ₂` with no
+`G`-edge between them, an observable supported on `Λ₁` has the same correlation
+in the transported disjoint sum (which equals `inducedGraph G (Λ₁ ∪ Λ₂)` by
+`inducedGraph_sum_map_eq_union_of_no_cross`) as in the induced subgraph on `Λ₁`
+alone. Combines `correlation_map_equiv` (iso transport) with
+`correlation_sum_inl` (disjoint-sum factorization).
+
+This is the bridge from a fully separated (bond-deleted) finite-volume system to
+the isolated-component correlation (Issue #2965, Phase A). The result is stated
+on `(... ).map (Equiv.Finset.union ...)` rather than directly on
+`inducedGraph G (Λ₁ ∪ Λ₂)` because rewriting the graph through the equality would
+require transporting the `Fintype edgeSet` instance; the equality lemma above
+records that the two graphs coincide. -/
+theorem correlation_inducedGraph_sum_map_inl (G : SimpleGraph V)
+    {Λ₁ Λ₂ : Finset V} (hd : Disjoint Λ₁ Λ₂)
+    [Fintype (inducedGraph G Λ₁).edgeSet]
+    [Fintype (inducedGraph G Λ₂).edgeSet]
+    [Fintype (((inducedGraph G Λ₁).sum (inducedGraph G Λ₂)).map
+      (Equiv.Finset.union Λ₁ Λ₂ hd).toEmbedding).edgeSet]
+    (p : IsingParams ℝ) (A : Finset (↑Λ₁ : Type _)) :
+    correlation (((inducedGraph G Λ₁).sum (inducedGraph G Λ₂)).map
+        (Equiv.Finset.union Λ₁ Λ₂ hd).toEmbedding) p
+        ((A.map ⟨Sum.inl, Sum.inl_injective⟩).map
+          (Equiv.Finset.union Λ₁ Λ₂ hd).toEmbedding)
+      = correlation (inducedGraph G Λ₁) p A := by
+  rw [correlation_map_equiv, correlation_sum_inl]
+
 end IsingModel

docs/index.md

@@ -362,6 +362,8 @@ Named specializations at `A = {i}`:
 | `spinProduct_map_equiv` / `correlation_map_equiv` | `e : V ≃ W ⇒ correlation (G.map e) p (A.map e) = correlation G p A` (correlation iso invariance, companion to `partitionFunction_map_equiv`) | `PartitionFunctionIso.lean` | Iso invariance (Issue #2965) |
 | `log_partitionFunction_inducedGraph_disjUnion_super_additive` (§4.6 Prop 4.6.1 Step 5 body) | `Disjoint Λ₁ Λ₂ ⇒ log Z_{inducedGraph Λ₁} + log Z_{inducedGraph Λ₂} ≤ log Z_{inducedGraph (Λ₁ ∪ Λ₂)}` (ferromagnetic) | `AmbientLatticeSum.lean` | Step 5 body |
 | `Ambient.freeEnergyΛ_weighted_super_additive_of_nonempty` | `|Λ₁|·f_{Λ₁} + |Λ₂|·f_{Λ₂} ≤ |Λ₁∪Λ₂|·f_{Λ₁∪Λ₂}` (disjoint nonempty, ferromagnetic) | `AmbientLatticeSum.lean` | `freeEnergyΛ` wrapper |
+| `inducedGraph_sum_map_eq_union_of_no_cross` | `Disjoint Λ₁ Λ₂` + no `G`-edge between `Λ₁,Λ₂` ⇒ `((inducedGraph Λ₁) ⊕g (inducedGraph Λ₂)).map (union) = inducedGraph (Λ₁ ∪ Λ₂)` (upgrades `inducedGraph_sum_map_le_union` to equality: no cross edges ⇒ every union edge stays within one part) | `InducedUnion.lean` | Component split (Issue #2965) |
+| `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) |
 | `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

@@ -12502,6 +12502,41 @@ \subsection{Super-additivity on Finset disjoint union
 case it is an edge of $\mathrm{inducedGraph}\,G\,(\Lambda_1 \cup \Lambda_2)$.
 \end{proof}
 
+\paragraph{Exact split with no cross edges (Issue \#2965).}
+When in addition there is no $G$-edge between $\Lambda_1$ and $\Lambda_2$, the
+subgraph relation becomes an equality.
+
+\begin{proposition}[\texttt{IsingModel.inducedGraph\_sum\_map\_eq\_union\_of\_no\_cross}]
+For disjoint $\Lambda_1,\Lambda_2$ with $\neg\,G.\mathrm{Adj}\,a\,b$ for all
+$a\in\Lambda_1,b\in\Lambda_2$,
+\[
+  (\mathrm{inducedGraph}\,\Lambda_1\oplus_g\mathrm{inducedGraph}\,\Lambda_2)
+    \,.\mathrm{map}\,e
+  = \mathrm{inducedGraph}\,G\,(\Lambda_1\cup\Lambda_2).
+\]
+\end{proposition}
+
+\begin{proof}
+The $\le$ direction is \texttt{inducedGraph\_sum\_map\_le\_union}; for $\ge$, an
+edge $a\sim b$ of the induced union gives $G.\mathrm{Adj}\,a\,b$ with
+$a,b\in\Lambda_1\cup\Lambda_2$, and the no-cross hypothesis rules out the split
+cases, so both endpoints lie in the same part and the edge is an
+$\mathrm{inl}$/$\mathrm{inr}$-image.
+\end{proof}
+
+\begin{proposition}[\texttt{IsingModel.correlation\_inducedGraph\_sum\_map\_inl}]
+For an observable $A$ supported on $\Lambda_1$,
+\[
+  \langle\sigma^{A}\rangle_{(\mathrm{inducedGraph}\,\Lambda_1
+    \oplus_g\mathrm{inducedGraph}\,\Lambda_2).\mathrm{map}\,e}
+  = \langle\sigma^{A}\rangle_{\mathrm{inducedGraph}\,\Lambda_1},
+\]
+by \texttt{correlation\_map\_equiv} (iso transport) and
+\texttt{correlation\_sum\_inl} (disjoint-sum factorization). Together with the
+equality above this is the component-factorization bridge from a fully separated
+finite-volume system to the isolated-component correlation.
+\end{proposition}
+
 \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