Skip to content

Commit fe9b676

Browse files
phasetrclaude
phasetr
and
claude
authored
feat: induced-union splits as disjoint sum under no cross edges — #2965 (#2977)
* feat: induced-union equality + correlation factorization under no-cross (Part of #2965) * feat: induced-union splits as disjoint sum under no cross edges Add the structural equality and its correlation factorization: - inducedGraph_sum_map_eq_union_of_no_cross: for disjoint Λ₁,Λ₂ with no G-edge between them, ((inducedGraph Λ₁) ⊕g (inducedGraph Λ₂)).map (union) = inducedGraph (Λ₁ ∪ Λ₂). Upgrades inducedGraph_sum_map_le_union to equality: no cross edges ⇒ every union edge stays within one part. - correlation_inducedGraph_sum_map_inl: an observable supported on Λ₁ has the same correlation in the transported disjoint sum as in inducedGraph Λ₁ (correlation_map_equiv + correlation_sum_inl). Component-factorization bridge from a fully separated (bond-deleted) finite-volume system to the isolated-component correlation. Part of #2965 Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com> --------- Co-authored-by: Claude Opus 4.7 <noreply@anthropic.com>
1 parent 61bbbfe commit fe9b676

3 files changed

Lines changed: 95 additions & 0 deletions

File tree

‎IsingModel/AmbientLatticeSum/InducedUnion.lean‎

Lines changed: 58 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -190,4 +190,62 @@ theorem partitionFunction_inducedGraph_le_of_disjoint_union
190190
(partitionFunction_pos _ _)).mp
191191
(log_partitionFunction_inducedGraph_le_of_disjoint_union G hd p hf)
192192

193+
/-- **Induced union splits as a disjoint sum when there are no cross edges**:
194+
for disjoint `Λ₁, Λ₂ : Finset V` with no `G`-edge between `Λ₁` and `Λ₂`, the
195+
induced subgraph on the union equals the transported disjoint sum of the two
196+
induced subgraphs. Upgrades `inducedGraph_sum_map_le_union` to an equality: the
197+
`≤` direction is that lemma; the `≥` direction holds because, with no cross
198+
edges, every edge of `inducedGraph G (Λ₁ ∪ Λ₂)` has both endpoints in the same
199+
part. This is the structural fact behind the component factorization of a
200+
bond-deleted (fully separated) finite-volume system (Issue #2965, Phase A). -/
201+
theorem inducedGraph_sum_map_eq_union_of_no_cross (G : SimpleGraph V)
202+
{Λ₁ Λ₂ : Finset V} (hd : Disjoint Λ₁ Λ₂)
203+
(hcross : ∀ a ∈ Λ₁, ∀ b ∈ Λ₂, ¬ G.Adj a b) :
204+
((inducedGraph G Λ₁).sum (inducedGraph G Λ₂)).map
205+
(Equiv.Finset.union Λ₁ Λ₂ hd).toEmbedding
206+
= inducedGraph G (Λ₁ ∪ Λ₂) := by
207+
refine le_antisymm (inducedGraph_sum_map_le_union G hd) ?_
208+
intro a b hab
209+
have hGadj : G.Adj (a : V) (b : V) := hab
210+
rw [SimpleGraph.map_adj]
211+
rcases Finset.mem_union.mp a.2 with ha | ha <;>
212+
rcases Finset.mem_union.mp b.2 with hb | hb
213+
· exact ⟨Sum.inl ⟨↑a, ha⟩, Sum.inl ⟨↑b, hb⟩, by
214+
simpa [SimpleGraph.sum_adj, inducedGraph, SimpleGraph.induce] using hGadj,
215+
by simp, by simp⟩
216+
· exact absurd hGadj (hcross _ ha _ hb)
217+
· exact absurd hGadj.symm (hcross _ hb _ ha)
218+
· exact ⟨Sum.inr ⟨↑a, ha⟩, Sum.inr ⟨↑b, hb⟩, by
219+
simpa [SimpleGraph.sum_adj, inducedGraph, SimpleGraph.induce] using hGadj,
220+
by simp, by simp⟩
221+
222+
set_option linter.unusedFintypeInType false in
223+
/-- **Component factorization of an induced-union correlation under no cross
224+
edges** (stated on the transported disjoint sum): for disjoint `Λ₁, Λ₂` with no
225+
`G`-edge between them, an observable supported on `Λ₁` has the same correlation
226+
in the transported disjoint sum (which equals `inducedGraph G (Λ₁ ∪ Λ₂)` by
227+
`inducedGraph_sum_map_eq_union_of_no_cross`) as in the induced subgraph on `Λ₁`
228+
alone. Combines `correlation_map_equiv` (iso transport) with
229+
`correlation_sum_inl` (disjoint-sum factorization).
230+
231+
This is the bridge from a fully separated (bond-deleted) finite-volume system to
232+
the isolated-component correlation (Issue #2965, Phase A). The result is stated
233+
on `(... ).map (Equiv.Finset.union ...)` rather than directly on
234+
`inducedGraph G (Λ₁ ∪ Λ₂)` because rewriting the graph through the equality would
235+
require transporting the `Fintype edgeSet` instance; the equality lemma above
236+
records that the two graphs coincide. -/
237+
theorem correlation_inducedGraph_sum_map_inl (G : SimpleGraph V)
238+
{Λ₁ Λ₂ : Finset V} (hd : Disjoint Λ₁ Λ₂)
239+
[Fintype (inducedGraph G Λ₁).edgeSet]
240+
[Fintype (inducedGraph G Λ₂).edgeSet]
241+
[Fintype (((inducedGraph G Λ₁).sum (inducedGraph G Λ₂)).map
242+
(Equiv.Finset.union Λ₁ Λ₂ hd).toEmbedding).edgeSet]
243+
(p : IsingParams ℝ) (A : Finset (↑Λ₁ : Type _)) :
244+
correlation (((inducedGraph G Λ₁).sum (inducedGraph G Λ₂)).map
245+
(Equiv.Finset.union Λ₁ Λ₂ hd).toEmbedding) p
246+
((A.map ⟨Sum.inl, Sum.inl_injective⟩).map
247+
(Equiv.Finset.union Λ₁ Λ₂ hd).toEmbedding)
248+
= correlation (inducedGraph G Λ₁) p A := by
249+
rw [correlation_map_equiv, correlation_sum_inl]
250+
193251
end IsingModel

‎docs/index.md‎

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -362,6 +362,8 @@ Named specializations at `A = {i}`:
362362
| `spinProduct_map_equiv` / `correlation_map_equiv` | `e : V ≃ W ⇒ correlation (G.map e) p (A.map e) = correlation G p A` (correlation iso invariance, companion to `partitionFunction_map_equiv`) | `PartitionFunctionIso.lean` | Iso invariance (Issue #2965) |
363363
| `log_partitionFunction_inducedGraph_disjUnion_super_additive` (§4.6 Prop 4.6.1 Step 5 body) | `Disjoint Λ₁ Λ₂ ⇒ log Z_{inducedGraph Λ₁} + log Z_{inducedGraph Λ₂} ≤ log Z_{inducedGraph (Λ₁ ∪ Λ₂)}` (ferromagnetic) | `AmbientLatticeSum.lean` | Step 5 body |
364364
| `Ambient.freeEnergyΛ_weighted_super_additive_of_nonempty` | `|Λ₁|·f_{Λ₁} + |Λ₂|·f_{Λ₂} ≤ |Λ₁∪Λ₂|·f_{Λ₁∪Λ₂}` (disjoint nonempty, ferromagnetic) | `AmbientLatticeSum.lean` | `freeEnergyΛ` wrapper |
365+
| `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) |
366+
| `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) |
365367
| `partitionFunction_ge_one_of_ferromagnetic` / `log_partitionFunction_nonneg_of_ferromagnetic` | `Z_G ≥ 1` (ferromagnetic), log form | `FreeEnergy.lean` | Step 5/Fekete infra |
366368
| `{log_,}partitionFunction{,Λ}_inducedGraph_le_of_disjoint_union` | `Disjoint Λ₁ Λ₂ ⇒ Z_{Λ₁} ≤ Z_{Λ₁∪Λ₂}` (ferromagnetic), log / multiplicative and generic / `Λ`-wrapped forms | `AmbientLatticeSum.lean` | Monotonicity step toward Fekete |
367369
| `Ambient.card_mul_freeEnergyΛ_le_of_disjoint_union` | `Λ₁.Nonempty, Disjoint Λ₁ Λ₂ ⇒ |Λ₁|·f_{Λ₁} ≤ |Λ₁∪Λ₂|·f_{Λ₁∪Λ₂}` (ferromagnetic) | `AmbientLatticeSum.lean` | `freeEnergyΛ` weighted monotonicity |

‎tex/proof-guide.tex‎

Lines changed: 35 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -12502,6 +12502,41 @@ \subsection{Super-additivity on Finset disjoint union
1250212502
case it is an edge of $\mathrm{inducedGraph}\,G\,(\Lambda_1 \cup \Lambda_2)$.
1250312503
\end{proof}
1250412504

12505+
\paragraph{Exact split with no cross edges (Issue \#2965).}
12506+
When in addition there is no $G$-edge between $\Lambda_1$ and $\Lambda_2$, the
12507+
subgraph relation becomes an equality.
12508+
12509+
\begin{proposition}[\texttt{IsingModel.inducedGraph\_sum\_map\_eq\_union\_of\_no\_cross}]
12510+
For disjoint $\Lambda_1,\Lambda_2$ with $\neg\,G.\mathrm{Adj}\,a\,b$ for all
12511+
$a\in\Lambda_1,b\in\Lambda_2$,
12512+
\[
12513+
(\mathrm{inducedGraph}\,\Lambda_1\oplus_g\mathrm{inducedGraph}\,\Lambda_2)
12514+
\,.\mathrm{map}\,e
12515+
= \mathrm{inducedGraph}\,G\,(\Lambda_1\cup\Lambda_2).
12516+
\]
12517+
\end{proposition}
12518+
12519+
\begin{proof}
12520+
The $\le$ direction is \texttt{inducedGraph\_sum\_map\_le\_union}; for $\ge$, an
12521+
edge $a\sim b$ of the induced union gives $G.\mathrm{Adj}\,a\,b$ with
12522+
$a,b\in\Lambda_1\cup\Lambda_2$, and the no-cross hypothesis rules out the split
12523+
cases, so both endpoints lie in the same part and the edge is an
12524+
$\mathrm{inl}$/$\mathrm{inr}$-image.
12525+
\end{proof}
12526+
12527+
\begin{proposition}[\texttt{IsingModel.correlation\_inducedGraph\_sum\_map\_inl}]
12528+
For an observable $A$ supported on $\Lambda_1$,
12529+
\[
12530+
\langle\sigma^{A}\rangle_{(\mathrm{inducedGraph}\,\Lambda_1
12531+
\oplus_g\mathrm{inducedGraph}\,\Lambda_2).\mathrm{map}\,e}
12532+
= \langle\sigma^{A}\rangle_{\mathrm{inducedGraph}\,\Lambda_1},
12533+
\]
12534+
by \texttt{correlation\_map\_equiv} (iso transport) and
12535+
\texttt{correlation\_sum\_inl} (disjoint-sum factorization). Together with the
12536+
equality above this is the component-factorization bridge from a fully separated
12537+
finite-volume system to the isolated-component correlation.
12538+
\end{proposition}
12539+
1250512540
\paragraph{Closing Prop 4.6.1.} Combined with the uniform upper
1250612541
bound (PR \#122, \#123), Fekete's lemma now yields
1250712542
convergence of $f_\Lambda = (\log Z_\Lambda)/|\Lambda|$ along

0 commit comments

Comments
 (0)