feat: generalize induce-univ correlation to any full set — #2965 (#2985)

* feat: generalize induce-univ correlation to any full set (Part of #2965)

* feat: generalize induce-univ correlation to any full set

Add correlation_induce_of_forall_mem: if s contains every vertex (∀ x, x ∈ s),
then correlation (G.induce s) p A = correlation G p (A.map (subtypeUnivEquiv hs)),
since G.induce s ≃g G. Generalizes correlation_induce_univ from Set.univ to any
full set.

Applies to s = ↑(S ∪ Sᶜ) (full by Finset.union_compl), letting the Phase A
capstone's inducedGraph _ (S ∪ Sᶜ) left side connect to the raw bond-deleted
graph WITHOUT forcing the propositional Finset equality S ∪ Sᶜ = univ at the
type level — the clean route through the per-stage-increment type-transport.

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/AmbientLatticeSum/InducedUnion.lean

@@ -398,4 +398,33 @@ theorem correlation_induce_univ [Fintype V] (G : SimpleGraph V)
   exact (correlation_map_equiv (Equiv.Set.univ V) (G.induce (Set.univ : Set V)) params A).symm.trans
     (correlation_congr_of_eq hmap params (A.map (Equiv.Set.univ V).toEmbedding))
 
+set_option linter.unusedFintypeInType false in
+/-- **Correlation on an induced subgraph over a full set equals correlation on
+the graph itself**: if `s : Set V` contains every vertex (`hs : ∀ x, x ∈ s`),
+then `G.induce s ≃g G` via `Equiv.subtypeUnivEquiv hs`, so pushing an observable
+along that relabeling preserves the correlation. Generalizes
+`correlation_induce_univ` from `Set.univ` to any full set — in particular to
+`↑(S ∪ Sᶜ)` (full by `Finset.union_compl`), which lets the component-factorization
+capstone's `inducedGraph _ (S ∪ Sᶜ)` left side connect to the raw bond-deleted
+graph without forcing the propositional Finset equality `S ∪ Sᶜ = univ` at the
+type level (Issue #2965, Phase A per-stage increment assembly). -/
+theorem correlation_induce_of_forall_mem [Fintype V] (G : SimpleGraph V)
+    (s : Set V) (hs : ∀ x, x ∈ s) [Fintype s]
+    [Fintype (G.induce s).edgeSet] [Fintype G.edgeSet]
+    (params : IsingParams ℝ) (A : Finset ↥s) :
+    correlation (G.induce s) params A
+      = correlation G params (A.map (Equiv.subtypeUnivEquiv hs).toEmbedding) := by
+  have hmap : (G.induce s).map (Equiv.subtypeUnivEquiv hs).toEmbedding = G := by
+    ext x y
+    rw [SimpleGraph.map_adj]
+    constructor
+    · rintro ⟨a, b, hab, rfl, rfl⟩
+      exact hab
+    · intro h
+      exact ⟨⟨x, hs x⟩, ⟨y, hs y⟩, by simpa using h, rfl, rfl⟩
+  haveI : Fintype ((G.induce s).map (Equiv.subtypeUnivEquiv hs).toEmbedding).edgeSet :=
+    hmap.symm ▸ (inferInstance : Fintype G.edgeSet)
+  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))
+
 end IsingModel

docs/index.md

@@ -370,6 +370,7 @@ Named specializations at `A = {i}`:
 | `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) |
 | `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_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

@@ -12633,6 +12633,19 @@ \subsection{Super-additivity on Finset disjoint union
 \texttt{correlation\_map\_equiv} with \texttt{correlation\_congr\_of\_eq}.
 \end{proof}
 
+\begin{proposition}[\texttt{IsingModel.correlation\_induce\_of\_forall\_mem}]
+If $s$ contains every vertex ($\forall x,\ x\in s$), then
+$\langle\sigma^{A}\rangle_{G.\mathrm{induce}\,s}
+  = \langle\sigma^{A.\mathrm{map}\,e}\rangle_{G}$ with
+$e=\texttt{Equiv.subtypeUnivEquiv}$. Generalizes the previous proposition from
+$\mathrm{univ}$ to any full set, in particular $s=\uparrow(S\cup S^{c})$ (full by
+\texttt{Finset.union\_compl}); this avoids forcing the propositional Finset
+equality $S\cup S^{c}=\mathrm{univ}$ at the type level when connecting the
+capstone's $\mathrm{inducedGraph}\,\_\,(S\cup S^{c})$ side to the raw bond-deleted
+graph in the per-stage-increment assembly. Same proof scheme as
+\texttt{correlation\_induce\_univ}.
+\end{proposition}
+
 \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