feat: bond-deleted raw correlation = isolated induced subgraph (per-stage increment form) — #2965

IsingModel/AmbientLatticeSum/InducedUnion.lean

@@ -427,4 +427,67 @@ theorem correlation_induce_of_forall_mem [Fintype V] (G : SimpleGraph V)
   exact (correlation_map_equiv (Equiv.subtypeUnivEquiv hs) (G.induce s) params A).symm.trans
     (correlation_congr_of_eq hmap params (A.map (Equiv.subtypeUnivEquiv hs).toEmbedding))
 
+/-- **Correlation is invariant under graph equality across *all* instances**:
+strengthens `correlation_congr_of_eq` to also absorb differences in the vertex
+`Fintype` and `edgeSet Fintype` instances, since `Fintype` is a `Subsingleton`
+(mathlib `Fintype.subsingleton`). For propositionally equal graphs `G₁ = G₂` on
+the same vertex type, the correlations agree regardless of which `Fintype ι`,
+`Fintype Gᵢ.edgeSet` instances are in play. This is the tool that bridges the
+`Finset.Subtype.fintype` (used by `inducedGraph`) and the `Set`-induce vertex
+`Fintype` in the per-stage-increment assembly (Issue #2965, Phase A). -/
+theorem correlation_congr_all {ι : Type*} [DecidableEq ι] {inst₁ inst₂ : Fintype ι}
+    {G₁ G₂ : SimpleGraph ι} {e₁ : Fintype G₁.edgeSet} {e₂ : Fintype G₂.edgeSet}
+    (hG : G₁ = G₂) (params : IsingParams ℝ) (A : Finset ι) :
+    @correlation ι inst₁ _ G₁ e₁ params A = @correlation ι inst₂ _ G₂ e₂ params A := by
+  subst hG
+  rw [Subsingleton.elim inst₁ inst₂, Subsingleton.elim e₁ e₂]
+
+set_option linter.unusedFintypeInType false in
+/-- **Bond-deleted raw correlation equals isolated induced-subgraph correlation**:
+combining the component-factorization capstone
+`correlation_inducedGraph_deleteEdges_union_inl` with
+`correlation_induce_of_forall_mem` (on the full set `↑(S ∪ Sᶜ)`) and the
+all-instance bridge `correlation_congr_all`, an `S`-supported observable has the
+same correlation in the *raw* bond-deleted graph `G.deleteEdges {straddle S}` as
+in the isolated induced subgraph on `S` of the original model. This is the
+per-stage-increment form that pairs directly with the ball-boundary bond-deletion
+increment `correlation_sub_deleteEdges_le_derivBound` (Issue #2965, Phase A). -/
+theorem correlation_deleteEdges_straddle_eq_inducedGraph [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 ((G.deleteEdges {e : Sym2 V |
+      ¬ Sym2.lift ⟨fun a b => ((a ∈ S) ↔ (b ∈ S)), fun a b => by simp [iff_comm]⟩ e}).induce
+      (↑(S ∪ Sᶜ) : Set V)).edgeSet]
+    [Fintype (G.deleteEdges {e : Sym2 V |
+      ¬ Sym2.lift ⟨fun a b => ((a ∈ S) ↔ (b ∈ S)), fun a b => by simp [iff_comm]⟩ e}).edgeSet]
+    [Fintype (inducedGraph G S).edgeSet]
+    (params : IsingParams ℝ) (A : Finset (↑S : Type _)) :
+    correlation (G.deleteEdges {e : Sym2 V |
+        ¬ Sym2.lift ⟨fun a b => ((a ∈ S) ↔ (b ∈ S)), fun a b => by simp [iff_comm]⟩ e}) params
+        ((((A.map ⟨Sum.inl, Sum.inl_injective⟩).map
+            (Equiv.Finset.union S Sᶜ disjoint_compl_right).toEmbedding).map
+          (Equiv.subtypeUnivEquiv (p := fun x => x ∈ (↑(S ∪ Sᶜ) : Set V))
+            (fun x => by
+              rw [Finset.union_compl, Finset.coe_univ]; exact Set.mem_univ x)).toEmbedding))
+      = correlation (inducedGraph G S) params A := by
+  refine (correlation_induce_of_forall_mem _ (↑(S ∪ Sᶜ) : Set V)
+    (fun x => by rw [Finset.union_compl, Finset.coe_univ]; exact Set.mem_univ x) params
+    ((A.map ⟨Sum.inl, Sum.inl_injective⟩).map
+      (Equiv.Finset.union S Sᶜ disjoint_compl_right).toEmbedding)).symm.trans
+    ((correlation_congr_all rfl params
+      ((A.map ⟨Sum.inl, Sum.inl_injective⟩).map
+        (Equiv.Finset.union S Sᶜ disjoint_compl_right).toEmbedding)).trans
+      (correlation_inducedGraph_deleteEdges_union_inl G S params A))
+
 end IsingModel

docs/index.md

@@ -371,6 +371,8 @@ Named specializations at `A = {i}`:
 | `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_induce_univ` | `correlation (G.induce Set.univ) p A = correlation G p (A.map (Equiv.Set.univ V))` — since `G.induce Set.univ ≃g G` (mathlib `induceUnivIso`), pushing the observable along the relabeling preserves the correlation. Connects `inducedGraph _ univ` statements (the left side of `correlation_inducedGraph_deleteEdges_union_inl`) back to the raw graph `G` (the form of `correlation_sub_deleteEdges_le_derivBound`) for the per-stage increment assembly (Issue #2965, Phase A) | `InducedUnion.lean` | Component split (Issue #2965) |
 | `correlation_induce_of_forall_mem` | `(∀ x, x ∈ s) ⇒ correlation (G.induce s) p A = correlation G p (A.map (Equiv.subtypeUnivEquiv hs))` — generalizes `correlation_induce_univ` from `Set.univ` to any full set `s` (via `G.induce s ≃g G`). Applies to `s = ↑(S ∪ Sᶜ)` (full by `Finset.union_compl`), letting the capstone's `inducedGraph _ (S ∪ Sᶜ)` left side connect to the raw bond-deleted graph **without** forcing the propositional `S ∪ Sᶜ = univ` at the type level — the clean route through the per-stage-increment type-transport (Issue #2965, Phase A) | `InducedUnion.lean` | Component split (Issue #2965) |
+| `correlation_congr_all` | `G₁ = G₂ ⇒ @correlation _ inst₁ _ G₁ e₁ p A = @correlation _ inst₂ _ G₂ e₂ p A` — strengthens `correlation_congr_of_eq` to absorb differences in the vertex `Fintype` **and** `edgeSet Fintype` instances, since `Fintype` is `Subsingleton` (`Fintype.subsingleton`). Bridges `Finset.Subtype.fintype` (from `inducedGraph`) vs the `Set`-induce vertex `Fintype` | `InducedUnion.lean` | Component split (Issue #2965) |
+| `correlation_deleteEdges_straddle_eq_inducedGraph` | **Per-stage-increment form.** `correlation (G.deleteEdges {straddle S}) p (((A.map inl).map union).map subtypeUnivEquiv) = correlation (inducedGraph G S) p A` — the *raw* bond-deleted graph's correlation of an `S`-supported observable equals the isolated induced-subgraph correlation. Composes `correlation_induce_of_forall_mem` (on `↑(S∪Sᶜ)`) ∘ `correlation_congr_all` ∘ `correlation_inducedGraph_deleteEdges_union_inl`. Intended to pair with the ball-boundary increment `correlation_sub_deleteEdges_le_derivBound` (#2974) toward the per-stage increment (that composition — finite edge-set, observable reduction to `{r,s}` — not yet formalized) | `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 |

tex/proof-guide.tex

@@ -12646,6 +12646,34 @@ \subsection{Super-additivity on Finset disjoint union
 \texttt{correlation\_induce\_univ}.
 \end{proposition}
 
+\begin{proposition}[\texttt{IsingModel.correlation\_congr\_all}]
+If $G_1=G_2$ then
+$\langle\sigma^{A}\rangle_{G_1}=\langle\sigma^{A}\rangle_{G_2}$ regardless of the
+vertex \texttt{Fintype} and \texttt{edgeSet Fintype} instances, since
+\texttt{Fintype} is a \texttt{Subsingleton} (\texttt{Fintype.subsingleton}):
+after \texttt{subst}, \texttt{Subsingleton.elim} equates the residual instances.
+Strengthens \texttt{correlation\_congr\_of\_eq} and bridges the
+\texttt{Finset.Subtype.fintype} (from \texttt{inducedGraph}) against the
+\texttt{Set}-induce vertex \texttt{Fintype}.
+\end{proposition}
+
+\begin{theorem}[\texttt{IsingModel.correlation\_deleteEdges\_straddle\_eq\_inducedGraph}
+(per-stage-increment form)]
+For $S\subseteq V$ and an $S$-supported observable $A$,
+\[
+  \langle\sigma^{A}\rangle_{G.\mathrm{deleteEdges}\,\{\text{straddle }S\}}
+    = \langle\sigma^{A}\rangle_{\mathrm{inducedGraph}\,G\,S},
+\]
+i.e.\ the \emph{raw} bond-deleted graph's correlation of an $S$-internal
+observable equals the isolated induced-subgraph correlation. Composes
+\texttt{correlation\_induce\_of\_forall\_mem} (on the full set
+$\uparrow(S\cup S^{c})$), \texttt{correlation\_congr\_all}, and the
+component-factorization capstone below. It is intended to pair with the
+ball-boundary increment \texttt{correlation\_sub\_deleteEdges\_le\_derivBound}
+toward the per-stage exhaustion increment bound; that composition (finite
+edge-set, observable reduction to the pair $\{r,s\}$) is not yet formalized here.
+\end{theorem}
+
 \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