feat: correlation on induce-univ equals correlation on G — #2965 (#2984)

* feat: correlation on induce-univ equals correlation on G (Part of #2965)

* feat: correlation on induce-univ equals correlation on G

Add 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; proved via the graph equality (G.induce univ).map e = G
composed through correlation_map_equiv and correlation_congr_of_eq.

Connects inducedGraph _ univ statements (the left side of the Phase A capstone
correlation_inducedGraph_deleteEdges_union_inl) back to the raw graph G (the
form of the ball-boundary increment correlation_sub_deleteEdges_le_derivBound),
for the per-stage exhaustion increment assembly.

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

@@ -370,4 +370,32 @@ theorem correlation_inducedGraph_deleteEdges_union_inl [Fintype V] (G : SimpleGr
     (correlation_congr_of_eq
       (inducedGraph_deleteEdges_eq_of_not_internal G _ S hD) params A)
 
+set_option linter.unusedFintypeInType false in
+/-- **Correlation on the full-vertex induced subgraph equals correlation on the
+graph itself**: since `G.induce Set.univ ≃g G` (mathlib `induceUnivIso`, via
+`Equiv.Set.univ`), pushing an observable forward along that relabeling leaves the
+correlation unchanged. This connects `inducedGraph`-based statements (e.g. the
+component-factorization capstone `correlation_inducedGraph_deleteEdges_union_inl`,
+whose left side lives on `inducedGraph _ univ`) back to the raw graph `G` (e.g.
+the ball-boundary increment `correlation_sub_deleteEdges_le_derivBound`)
+(Issue #2965, Phase A). -/
+theorem correlation_induce_univ [Fintype V] (G : SimpleGraph V)
+    [Fintype (G.induce (Set.univ : Set V)).edgeSet] [Fintype G.edgeSet]
+    (params : IsingParams ℝ) (A : Finset ↥(Set.univ : Set V)) :
+    correlation (G.induce (Set.univ : Set V)) params A
+      = correlation G params (A.map (Equiv.Set.univ V).toEmbedding) := by
+  have hmap : (G.induce (Set.univ : Set V)).map (Equiv.Set.univ V).toEmbedding = G := by
+    ext x y
+    rw [SimpleGraph.map_adj]
+    constructor
+    · rintro ⟨a, b, hab, rfl, rfl⟩
+      exact hab
+    · intro h
+      exact ⟨(Equiv.Set.univ V).symm x, (Equiv.Set.univ V).symm y, by simpa using h,
+        by simp, by simp⟩
+  haveI : Fintype ((G.induce (Set.univ : Set V)).map
+      (Equiv.Set.univ V).toEmbedding).edgeSet := hmap.symm ▸ (inferInstance : Fintype G.edgeSet)
+  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))
+
 end IsingModel

docs/index.md

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

@@ -12614,6 +12614,25 @@ \subsection{Super-additivity on Finset disjoint union
 \texttt{correlation\_inducedGraph\_union\_inl\_of\_no\_cross} applies to it.
 \end{proof}
 
+\begin{proposition}[\texttt{IsingModel.correlation\_induce\_univ}]
+Since $G.\mathrm{induce}\,\mathrm{univ}\simeq_g G$ (mathlib \texttt{induceUnivIso},
+via \texttt{Equiv.Set.univ}), pushing an observable along that relabeling
+preserves the correlation:
+\[
+  \langle\sigma^{A}\rangle_{G.\mathrm{induce}\,\mathrm{univ}}
+    = \langle\sigma^{A.\mathrm{map}\,e}\rangle_{G},\qquad e=\texttt{Equiv.Set.univ}.
+\]
+This connects the $\mathrm{inducedGraph}\,\_\,\mathrm{univ}$ left side of the
+capstone below back to the raw graph $G$ (the form of the ball-boundary
+increment), for the per-stage increment assembly.
+\end{proposition}
+
+\begin{proof}
+The graph equality $(G.\mathrm{induce}\,\mathrm{univ}).\mathrm{map}\,e = G$ holds
+by edge extensionality (the iso adjacency); then compose
+\texttt{correlation\_map\_equiv} with \texttt{correlation\_congr\_of\_eq}.
+\end{proof}
+
 \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