From c221cb541e742097ae65eed08876d427eb160f89 Mon Sep 17 00:00:00 2001 From: phasetr Date: Wed, 27 May 2026 01:00:48 +0900 Subject: [PATCH 1/2] feat: straddle-set no-cross + not-internal facts (Part of #2965) From 412ce0e834248dab87d14d37ac2af2765ffc5f49 Mon Sep 17 00:00:00 2001 From: phasetr Date: Wed, 27 May 2026 01:02:30 +0900 Subject: [PATCH 2/2] feat: straddle-set no-cross + not-internal facts MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Add two graph-level facts about the straddle (cut) edge set of induce_sum_map_sumCompl_eq_deleteEdges: - straddle_not_mem_of_same_side: p a ↔ p b ⇒ s(a,b) ∉ straddle (the deleted set contains no same-side edge), feeding inducedGraph_deleteEdges_eq_of_not_internal. - deleteEdges_straddle_no_cross: p a, ¬p b ⇒ ¬(G.deleteEdges {straddle}).Adj a b (the bond-deleted graph disconnects the two sides), the no-cross hypothesis for correlation_inducedGraph_union_inl_of_no_cross applied to G.deleteEdges {straddle}. Pure adjacency facts (no Fintype), bridging #2979/#2981/#2978 toward the bond-deletion → isolated-component capstone via the working inducedGraph route. Part of #2965 Co-Authored-By: Claude Opus 4.7 --- IsingModel/SumGraph.lean | 24 ++++++++++++++++++++++++ docs/index.md | 1 + tex/proof-guide.tex | 17 +++++++++++++++++ 3 files changed, 42 insertions(+) diff --git a/IsingModel/SumGraph.lean b/IsingModel/SumGraph.lean index 2f22b713..e5ab9677 100644 --- a/IsingModel/SumGraph.lean +++ b/IsingModel/SumGraph.lean @@ -165,4 +165,28 @@ theorem induce_sum_map_sumCompl_eq_deleteEdges (p : V → Prop) [DecidablePred p · exact ⟨Sum.inl ⟨a, hp⟩, Sum.inl ⟨b, hiff.mp hp⟩, hadj, rfl, rfl⟩ · exact ⟨Sum.inr ⟨a, hp⟩, Sum.inr ⟨b, fun h => hp (hiff.mpr h)⟩, hadj, rfl, rfl⟩ +/-- The "straddle" deleted set (edges with endpoints on different sides of `p`) +of `induce_sum_map_sumCompl_eq_deleteEdges` contains no edge whose endpoints lie +on the *same* side of `p`. Hence removing it never deletes an edge internal to a +side — the hypothesis required by `inducedGraph_deleteEdges_eq_of_not_internal`. -/ +theorem straddle_not_mem_of_same_side (p : V → Prop) {a b : V} (h : p a ↔ p b) : + s(a, b) ∉ {e : Sym2 V | + ¬ Sym2.lift ⟨fun a b => (p a ↔ p b), fun a b => by simp [iff_comm]⟩ e} := by + simp only [Set.mem_setOf_eq, Sym2.lift_mk, not_not] + exact h + +/-- The bond-deleted (straddle-removed) graph has no edge between the two sides of +`p`: deleting the cut edges disconnects `{a | p a}` from `{a | ¬ p a}`. This is +the no-cross hypothesis required by `correlation_inducedGraph_union_inl_of_no_cross` +applied to `G.deleteEdges {straddling edges}`. -/ +theorem deleteEdges_straddle_no_cross (G : SimpleGraph V) (p : V → Prop) + {a b : V} (ha : p a) (hb : ¬ p b) : + ¬ (G.deleteEdges {e : Sym2 V | + ¬ Sym2.lift ⟨fun a b => (p a ↔ p b), fun a b => by simp [iff_comm]⟩ e}).Adj a b := by + rw [SimpleGraph.deleteEdges_adj] + rintro ⟨_, hmem⟩ + refine hmem ?_ + simp only [Set.mem_setOf_eq, Sym2.lift_mk] + exact fun h => hb (h.mp ha) + end SimpleGraph diff --git a/docs/index.md b/docs/index.md index 2052877c..43abe942 100644 --- a/docs/index.md +++ b/docs/index.md @@ -351,6 +351,7 @@ Named specializations at `A = {i}`: | `disjoint_inl_inr_edgeSet` / `disjoint_inl_inr_edgeFinset` | Set / Finset disjointness of the two images | `SumGraph.lean` | Disjoint-sum lemma | | `card_edgeFinset_sum` | `#(G ⊕g H).edgeFinset = #G.edgeFinset + #H.edgeFinset` | `SumGraph.lean` | Disjoint-sum lemma | | `induce_sum_map_sumCompl_eq_deleteEdges` | `((G.induce {p}) ⊕g (G.induce {¬p})).map (Equiv.sumCompl p) = G.deleteEdges {straddling edges}`: deleting every edge whose endpoints lie on different sides of a predicate `p` decomposes `G` into the disjoint sum of the two induced subgraphs. The structural identity behind component factorization of a bond-deleted (cut) system | `SumGraph.lean` | Component split (Issue #2965) | +| `straddle_not_mem_of_same_side` / `deleteEdges_straddle_no_cross` | The straddle set contains no same-side edge (`p a ↔ p b ⇒ s(a,b) ∉ straddle`), so deleting it is non-internal (feeds `inducedGraph_deleteEdges_eq_of_not_internal`); and `G.deleteEdges {straddle}` has no edge between `{p}` and `{¬p}` (`p a, ¬p b ⇒ ¬Adj`), the no-cross hypothesis for `correlation_inducedGraph_union_inl_of_no_cross` applied to the bond-deleted graph | `SumGraph.lean` | Component split (Issue #2965) | | `Config.sumEquiv` | `Config (ι ⊕ ι') ≃ Config ι × Config ι'` | `SumModel.lean` | Ising on sum graph | | `interactionEnergy_sum` / `externalFieldEnergy_sum` | Per-summand additivity of the Hamiltonian's interaction / field contributions on `G ⊕g H` | `SumModel.lean` | Ising on sum graph | | `hamiltonian_sum` (§4.6 super-add. Step 2-3) | `hamiltonian (G ⊕g H) p (Sum.elim σ₁ σ₂) = hamiltonian G p σ₁ + hamiltonian H p σ₂` | `SumModel.lean` | Ising on sum graph | diff --git a/tex/proof-guide.tex b/tex/proof-guide.tex index c65b9fce..d21e2acd 100644 --- a/tex/proof-guide.tex +++ b/tex/proof-guide.tex @@ -12249,6 +12249,23 @@ \subsection{Edge-set decomposition for disjoint sum graphs (\texttt{SumGraph.lea across a partition yields two independent subsystems. \end{proof} +\begin{proposition}[\texttt{straddle\_not\_mem\_of\_same\_side} / +\texttt{deleteEdges\_straddle\_no\_cross}] +The straddle set contains no same-side edge: if $p\,a \leftrightarrow p\,b$ then +$s(a,b)$ is not deleted (feeds +\texttt{inducedGraph\_deleteEdges\_eq\_of\_not\_internal}). Dually, the +bond-deleted graph has no edge between the two sides: if $p\,a$ and $\neg p\,b$ +then $G.\mathrm{deleteEdges}\,\{\text{straddle}\}$ has no $a\sim b$ edge (the +no-cross hypothesis for \texttt{correlation\_inducedGraph\_union\_inl\_of\_no\_cross} +applied to the bond-deleted graph). +\end{proposition} + +\begin{proof} +Both unfold the straddle membership $s(a,b)\in\{e\mid\neg(p\!\leftrightarrow\!p)(e)\} +\Leftrightarrow \neg(p\,a\leftrightarrow p\,b)$ and the deleteEdges adjacency +$\mathrm{Adj}\wedge s(a,b)\notin\{\dots\}$. +\end{proof} + \paragraph{Context.} This file is the combinatorial Step~1 toward the Glimm--Jaffe \S 4.6 super-additivity proof of thermodynamic-limit convergence of the free-energy density. Subsequent steps