feat: nested induced-subgraph graph equality — #2965 (#2990)

* feat: nested induced-subgraph graph equality (Part of #2965)

* feat: nested induced-subgraph graph equality

Add nestedSubtypeEquiv and inducedGraph_induce_preimage_map_eq: for S ⊆ T,
((inducedGraph G T).induce {x : ↥T | x.val ∈ S}).map nestedSubtypeEquiv =
inducedGraph G S — inducing box_k inside inducedGraph G box_{k+1} equals, up to
the nested-subtype relabeling {x : ↥T // x.val ∈ S} ≃ ↥S, the direct induced
subgraph on S. An edge survives iff its deep endpoints are G-adjacent and both
in S.

Graph-level foundation for instantiating the per-stage increment
(correlation_pair_sub_inducedGraph_le_derivBound, #2989) on cubic exhaustion
stages box_k ⊆ box_{k+1}. The correlation-level transport across this iso is a
follow-up (it currently hits a whnf elaboration wall in correlation_map_equiv on
the nested-subtype graph, needing a lighter sum-level encoding).

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

@@ -508,4 +508,31 @@ theorem triple_map_subtypeUnivEquiv_eq [Fintype V] (S : Finset V)
   rw [Finset.map_map, Finset.map_map]
   congr 1
 
+/-- The nested-subtype relabeling `{x : ↥T // x.val ∈ S} ≃ ↥S` for `S ⊆ T`. -/
+def nestedSubtypeEquiv {S T : Finset V} (hST : S ⊆ T) :
+    {x : (↑T : Type _) // x.val ∈ S} ≃ (↑S : Type _) :=
+  Equiv.subtypeSubtypeEquivSubtype (fun {_x} h => hST h)
+
+omit [DecidableEq V] in
+/-- **Nested induced subgraph equals direct induced subgraph (graph form)**: for
+`S ⊆ T`, pushing the induced subgraph of `inducedGraph G T` over the preimage of
+`S` forward along `nestedSubtypeEquiv` recovers the direct induced subgraph
+`inducedGraph G S`. An edge survives iff its (deep) endpoints are `G`-adjacent and
+both in `S`. This is the graph-level foundation for instantiating the per-stage
+increment on cubic exhaustion stages `box_k ⊆ box_{k+1}` (Issue #2965, Phase A);
+the correlation-level transport is a follow-up. -/
+theorem inducedGraph_induce_preimage_map_eq (G : SimpleGraph V) {S T : Finset V}
+    (hST : S ⊆ T) :
+    ((inducedGraph G T).induce {x : (↑T : Type _) | x.val ∈ S}).map
+        (nestedSubtypeEquiv hST).toEmbedding
+      = inducedGraph G S := by
+  ext a b
+  simp only [SimpleGraph.map_adj, inducedGraph_apply, SimpleGraph.induce_adj]
+  constructor
+  · rintro ⟨x, y, hxy, rfl, rfl⟩
+    exact hxy
+  · intro h
+    exact ⟨(nestedSubtypeEquiv hST).symm a, (nestedSubtypeEquiv hST).symm b,
+      by simpa using h, by simp, by simp⟩
+
 end IsingModel

docs/index.md

@@ -376,6 +376,7 @@ Named specializations at `A = {i}`:
 | `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`. Pairs with the ball-boundary increment `correlation_sub_deleteEdges_le_derivBound` (#2974) to give the numeric per-stage increment `correlation_pair_sub_inducedGraph_le_derivBound` (#2989) | `InducedUnion.lean` | Component split (Issue #2965) |
 | `triple_map_subtypeUnivEquiv_eq` | `(((A.map inl).map union).map subtypeUnivEquiv) = A.map ⟨Subtype.val, _⟩` — the triple-mapped `S`-observable (through `Sum.inl`, `Equiv.Finset.union S Sᶜ`, `Equiv.subtypeUnivEquiv`) equals the plain subtype-inclusion image of `A` in `V`. Identifies the observable of `correlation_deleteEdges_straddle_eq_inducedGraph` with the raw `V`-vertex observable (e.g. `{r,s}` for the pair), matching `correlation_sub_deleteEdges_le_derivBound` (Issue #2965, Phase A) | `InducedUnion.lean` | Component split (Issue #2965) |
 | `correlation_pair_sub_inducedGraph_le_derivBound` | **Numeric per-stage correlation increment (Phase A).** For `r,s ∈ S`, `r ≠ s`, ferromagnetic, `h=0`, and `r,s` not on any cut (straddle) edge: `correlation G p {r,s} − correlation (inducedGraph G S) p {⟨r,_⟩,⟨s,_⟩} ≤ derivBound G (G.edgeFinset.filter straddle) p r s`. Composes the ball-boundary bond-deletion increment `correlation_sub_deleteEdges_le_derivBound` (#2974) with the component-factorization bridge `correlation_deleteEdges_straddle_eq_inducedGraph` (#2986) via `deleteEdges_filter_edgeFinset_eq` (#2987) + `correlation_congr_all` + `triple_map_subtypeUnivEquiv_eq` (#2988). The full-model pair correlation exceeds the isolated induced-subgraph pair correlation by at most the boundary `derivBound` over the cut edges | `PerStageIncrement.lean` | Per-stage increment (Issue #2965) |
+| `nestedSubtypeEquiv` / `inducedGraph_induce_preimage_map_eq` | For `S ⊆ T`, `((inducedGraph G T).induce {x : ↥T \| x.val ∈ S}).map nestedSubtypeEquiv = inducedGraph G S` — the nested induced subgraph (induce `box_k` inside `inducedGraph G box_{k+1}`) equals, up to the nested-subtype relabeling `{x : ↥T // x.val ∈ S} ≃ ↥S`, the direct induced subgraph on `S`. Graph-level foundation for instantiating the per-stage increment on cubic exhaustion stages `box_k ⊆ box_{k+1}` (correlation-level transport is the follow-up) | `InducedUnion.lean` | Nested induce (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

@@ -12708,6 +12708,22 @@ \subsection{Super-additivity on Finset disjoint union
 theorem below).
 \end{proposition}
 
+\begin{proposition}[\texttt{IsingModel.inducedGraph\_induce\_preimage\_map\_eq}]
+For $S\subseteq T$, the nested induced subgraph equals the direct one up to the
+nested-subtype relabeling $\{x:\uparrow T\mid x.\mathrm{val}\in S\}\simeq\uparrow S$:
+\[
+  \bigl((\mathrm{inducedGraph}\,G\,T).\mathrm{induce}\,\{x\mid x.\mathrm{val}\in S\}\bigr)
+    .\mathrm{map}\,\mathrm{nestedSubtypeEquiv}
+  = \mathrm{inducedGraph}\,G\,S.
+\]
+An edge survives iff its (deep) endpoints are $G$-adjacent and both in $S$. This
+is the graph-level foundation for instantiating the per-stage increment on cubic
+exhaustion stages $\mathrm{box}_k\subseteq\mathrm{box}_{k+1}$ (Issue \#2965); the
+correlation-level transport across this iso is a follow-up (it currently hits a
+\texttt{whnf} elaboration wall in \texttt{correlation\_map\_equiv} on the
+nested-subtype graph, needing a lighter sum-level encoding).
+\end{proposition}
+
 \begin{theorem}[\texttt{IsingModel.correlation\_pair\_sub\_inducedGraph\_le\_derivBound}
 (numeric per-stage correlation increment, Issue \#2965 Phase A)]
 For $r,s\in S$, $r\neq s$, ferromagnetic parameters at $h=0$, with $r,s$ on no