feat: triple-mapped S-observable = val-image observable — #2965

IsingModel/AmbientLatticeSum/InducedUnion.lean

@@ -490,4 +490,22 @@ theorem correlation_deleteEdges_straddle_eq_inducedGraph [Fintype V] (G : Simple
         (Equiv.Finset.union S Sᶜ disjoint_compl_right).toEmbedding)).trans
       (correlation_inducedGraph_deleteEdges_union_inl G S params A))
 
+/-- **The triple-mapped `S`-observable is the raw `val`-image observable**: pushing
+a `Finset ↥S` through `Sum.inl`, the `Equiv.Finset.union S Sᶜ` relabeling, and the
+`Equiv.subtypeUnivEquiv` to `V` recovers exactly the image of `A` under the
+subtype inclusion `↥S → V`. This identifies the observable appearing in
+`correlation_deleteEdges_straddle_eq_inducedGraph` with the plain `V`-vertex
+observable — e.g. for `A = {⟨r,_⟩, ⟨s,_⟩}` it is the pair `{r, s}`, matching the
+ball-boundary increment `correlation_sub_deleteEdges_le_derivBound` (Issue #2965,
+Phase A per-stage increment). -/
+theorem triple_map_subtypeUnivEquiv_eq [Fintype V] (S : Finset V)
+    (A : Finset (↑S : Type _)) :
+    ((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
+      = A.map ⟨Subtype.val, Subtype.val_injective⟩ := by
+  rw [Finset.map_map, Finset.map_map]
+  congr 1
+
 end IsingModel

docs/index.md

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

@@ -12690,6 +12690,23 @@ \subsection{Super-additivity on Finset disjoint union
 edge-set, observable reduction to the pair $\{r,s\}$) is not yet formalized here.
 \end{theorem}
 
+\begin{proposition}[\texttt{IsingModel.triple\_map\_subtypeUnivEquiv\_eq}]
+The triple-mapped $S$-observable equals the raw subtype-inclusion image:
+\[
+  ((A.\mathrm{map}\,\mathrm{inl}).\mathrm{map}\,\mathrm{union})
+    .\mathrm{map}\,\mathrm{subtypeUnivEquiv}
+  = A.\mathrm{map}\,\langle\mathrm{Subtype.val},\cdot\rangle.
+\]
+By \texttt{Finset.map\_map} the three embeddings compose to the inclusion
+$\uparrow S\hookrightarrow V$. This identifies the observable of
+\texttt{correlation\_deleteEdges\_straddle\_eq\_inducedGraph} with the plain
+$V$-vertex observable (e.g.\ $\{r,s\}$ for the pair), supplying the observable
+match for the per-stage increment; together with
+\texttt{deleteEdges\_filter\_edgeFinset\_eq} and \texttt{correlation\_congr\_all}
+the remaining gap to the numeric increment is only the discharge of the
+ball-boundary hypotheses for the straddle-edge finset.
+\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