feat: correlation graph-equality congruence + induced-union bridge (union form) — #2965 (#2978)

* feat: correlation graph-equality congruence + inducedGraph-union bridge (Part of #2965)

* feat: correlation graph-equality congruence + induced-union bridge (union form)

Complete Phase A step 1 (the Fintype-instance transport):

- correlation_congr_of_eq: G₁ = G₂ ⇒ correlation G₁ p A = correlation G₂ p A,
  invariant across different Fintype edgeSet instances (edgeFinset coerces to the
  instance-free edgeSet). Bridges propositional graph equalities without rw's
  motive obstruction.
- correlation_inducedGraph_union_inl_of_no_cross: the component-factorization
  bridge stated directly on inducedGraph (Λ₁ ∪ Λ₂):
    correlation (inducedGraph (Λ₁ ∪ Λ₂)) p ((A.map inl).map union)
      = correlation (inducedGraph Λ₁) p A
  for disjoint Λ₁,Λ₂ with no cross edge, via
  inducedGraph_sum_map_eq_union_of_no_cross + correlation_congr_of_eq +
  correlation_inducedGraph_sum_map_inl. This is the form usable for exhaustion
  stages.

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

@@ -248,4 +248,56 @@ theorem correlation_inducedGraph_sum_map_inl (G : SimpleGraph V)
       = correlation (inducedGraph G Λ₁) p A := by
   rw [correlation_map_equiv, correlation_sum_inl]
 
+/-- **Correlation is invariant under graph equality**, regardless of which
+`Fintype edgeSet` instance is used: if `G₁ = G₂` then their correlations agree.
+Correlation depends on the graph only through `edgeFinset` (inside the
+Hamiltonian's interaction energy), and `edgeFinset` is instance-independent
+since it coerces to `edgeSet`. This lets one transport correlations across the
+graph equalities of this file (e.g. `inducedGraph_sum_map_eq_union_of_no_cross`)
+without the `Fintype` motive obstruction that blocks `rw`. -/
+theorem correlation_congr_of_eq {W : Type*} [Fintype W] [DecidableEq W]
+    {G₁ G₂ : SimpleGraph W}
+    [inst₁ : Fintype G₁.edgeSet] [inst₂ : Fintype G₂.edgeSet]
+    (h : G₁ = G₂) (p : IsingParams ℝ) (A : Finset W) :
+    correlation G₁ p A = correlation G₂ p A := by
+  subst h
+  -- After `subst`, both sides are the same graph; the only residual difference is
+  -- the `Fintype G₁.edgeSet` instance the Hamiltonian's interaction energy feeds to
+  -- `edgeFinset`. Since `edgeFinset` coerces to the instance-free `edgeSet`, the two
+  -- edge finsets are equal, which `simp` propagates through `correlation`.
+  have hef : @SimpleGraph.edgeFinset _ G₁ inst₁ = @SimpleGraph.edgeFinset _ G₁ inst₂ := by
+    apply Finset.coe_injective
+    rw [SimpleGraph.coe_edgeFinset, SimpleGraph.coe_edgeFinset]
+  simp only [correlation, gibbsExpectation, partitionFunction, boltzmannWeight,
+    hamiltonian, interactionEnergy, hef]
+
+set_option linter.unusedFintypeInType false in
+/-- **Component factorization of an induced-union correlation (union form)**:
+the bridge of `correlation_inducedGraph_sum_map_inl` transported onto
+`inducedGraph G (Λ₁ ∪ Λ₂)` itself, via `inducedGraph_sum_map_eq_union_of_no_cross`
+and `correlation_congr_of_eq` (which absorbs the `Fintype` instance change). For
+disjoint `Λ₁, Λ₂` with no `G`-edge between them, an observable supported on `Λ₁`
+has the same correlation in the induced subgraph on the union as in the induced
+subgraph on `Λ₁` alone — the component-factorization bridge in the form directly
+usable for exhaustion stages (Issue #2965, Phase A). -/
+theorem correlation_inducedGraph_union_inl_of_no_cross (G : SimpleGraph V)
+    {Λ₁ Λ₂ : Finset V} (hd : Disjoint Λ₁ Λ₂)
+    (hcross : ∀ a ∈ Λ₁, ∀ b ∈ Λ₂, ¬ G.Adj a b)
+    [Fintype (inducedGraph G Λ₁).edgeSet]
+    [Fintype (inducedGraph G Λ₂).edgeSet]
+    [Fintype (((inducedGraph G Λ₁).sum (inducedGraph G Λ₂)).map
+      (Equiv.Finset.union Λ₁ Λ₂ hd).toEmbedding).edgeSet]
+    [Fintype (inducedGraph G (Λ₁ ∪ Λ₂)).edgeSet]
+    (p : IsingParams ℝ) (A : Finset (↑Λ₁ : Type _)) :
+    correlation (inducedGraph G (Λ₁ ∪ Λ₂)) p
+        ((A.map ⟨Sum.inl, Sum.inl_injective⟩).map
+          (Equiv.Finset.union Λ₁ Λ₂ hd).toEmbedding)
+      = correlation (inducedGraph G Λ₁) p A :=
+  Eq.trans
+    (correlation_congr_of_eq
+      (inducedGraph_sum_map_eq_union_of_no_cross G hd hcross).symm p
+      ((A.map ⟨Sum.inl, Sum.inl_injective⟩).map
+        (Equiv.Finset.union Λ₁ Λ₂ hd).toEmbedding))
+    (correlation_inducedGraph_sum_map_inl G hd p A)
+
 end IsingModel

docs/index.md

@@ -364,6 +364,8 @@ Named specializations at `A = {i}`:
 | `Ambient.freeEnergyΛ_weighted_super_additive_of_nonempty` | `|Λ₁|·f_{Λ₁} + |Λ₂|·f_{Λ₂} ≤ |Λ₁∪Λ₂|·f_{Λ₁∪Λ₂}` (disjoint nonempty, ferromagnetic) | `AmbientLatticeSum.lean` | `freeEnergyΛ` wrapper |
 | `inducedGraph_sum_map_eq_union_of_no_cross` | `Disjoint Λ₁ Λ₂` + no `G`-edge between `Λ₁,Λ₂` ⇒ `((inducedGraph Λ₁) ⊕g (inducedGraph Λ₂)).map (union) = inducedGraph (Λ₁ ∪ Λ₂)` (upgrades `inducedGraph_sum_map_le_union` to equality: no cross edges ⇒ every union edge stays within one part) | `InducedUnion.lean` | Component split (Issue #2965) |
 | `correlation_inducedGraph_sum_map_inl` | `correlation ((inducedGraph Λ₁ ⊕g inducedGraph Λ₂).map union) p ((A.map inl).map union) = correlation (inducedGraph Λ₁) p A` (component factorization of an induced-union correlation; by `correlation_map_equiv` + `correlation_sum_inl`) | `InducedUnion.lean` | Component split (Issue #2965) |
+| `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) |
 | `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 |
 | `Ambient.card_mul_freeEnergyΛ_le_of_disjoint_union` | `Λ₁.Nonempty, Disjoint Λ₁ Λ₂ ⇒ |Λ₁|·f_{Λ₁} ≤ |Λ₁∪Λ₂|·f_{Λ₁∪Λ₂}` (ferromagnetic) | `AmbientLatticeSum.lean` | `freeEnergyΛ` weighted monotonicity |

tex/proof-guide.tex

@@ -12537,6 +12537,25 @@ \subsection{Super-additivity on Finset disjoint union
 finite-volume system to the isolated-component correlation.
 \end{proposition}
 
+\begin{proposition}[\texttt{IsingModel.correlation\_inducedGraph\_union\_inl\_of\_no\_cross}]
+Under the no-cross hypothesis, the same factorization holds directly on the
+induced subgraph of the union:
+\[
+  \langle\sigma^{A}\rangle_{\mathrm{inducedGraph}\,G\,(\Lambda_1\cup\Lambda_2)}
+  = \langle\sigma^{A}\rangle_{\mathrm{inducedGraph}\,G\,\Lambda_1}.
+\]
+\end{proposition}
+
+\begin{proof}
+Transport the previous proposition across the graph equality
+\texttt{inducedGraph\_sum\_map\_eq\_union\_of\_no\_cross} using
+\texttt{correlation\_congr\_of\_eq}: correlation is invariant under graph
+equality even across distinct \texttt{Fintype edgeSet} instances, since
+$\mathrm{edgeFinset}$ coerces to the instance-free $\mathrm{edgeSet}$. This
+absorbs the \texttt{Fintype} motive obstruction that blocks a direct
+\texttt{rw}.
+\end{proof}
+
 \paragraph{Closing Prop 4.6.1.} Combined with the uniform upper
 bound (PR \#122, \#123), Fekete's lemma now yields
 convergence of $f_\Lambda = (\log Z_\Lambda)/|\Lambda|$ along