Skip to content

Commit 055ce00

Browse files
phasetrclaude
phasetr
and
claude
authored
feat: bond-deleted raw correlation = isolated induced subgraph (per-stage increment form) — #2965 (#2986)
* feat: bond-deleted raw correlation = isolated induced subgraph (Part of #2965) * feat: bond-deleted raw correlation = isolated induced subgraph (per-stage increment form) Add two lemmas closing the Phase A per-stage-increment assembly: - correlation_congr_all: G₁ = G₂ ⇒ correlation G₁ = correlation G₂ across ALL instances (vertex Fintype + edgeSet Fintype), since Fintype is Subsingleton (Fintype.subsingleton). Strengthens correlation_congr_of_eq; resolves the vertex-Fintype diamond between Finset.Subtype.fintype (inducedGraph) and the Set-induce vertex Fintype. - correlation_deleteEdges_straddle_eq_inducedGraph: the raw bond-deleted graph's correlation of an S-supported observable equals the isolated induced-subgraph correlation: correlation (G.deleteEdges {straddle S}) p (((A.map inl).map union).map subtypeUnivEquiv) = correlation (inducedGraph G S) p A Composes correlation_induce_of_forall_mem (on ↑(S∪Sᶜ)) ∘ correlation_congr_all ∘ correlation_inducedGraph_deleteEdges_union_inl. This is the per-stage-increment form that pairs directly with the ball-boundary bond-deletion increment correlation_sub_deleteEdges_le_derivBound (#2974). Part of #2965 Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com> * docs: soften per-stage increment claim per codex (composition not yet formalized) Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com> --------- Co-authored-by: Claude Opus 4.7 <noreply@anthropic.com>
1 parent c758342 commit 055ce00

3 files changed

Lines changed: 93 additions & 0 deletions

File tree

‎IsingModel/AmbientLatticeSum/InducedUnion.lean‎

Lines changed: 63 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -427,4 +427,67 @@ theorem correlation_induce_of_forall_mem [Fintype V] (G : SimpleGraph V)
427427
exact (correlation_map_equiv (Equiv.subtypeUnivEquiv hs) (G.induce s) params A).symm.trans
428428
(correlation_congr_of_eq hmap params (A.map (Equiv.subtypeUnivEquiv hs).toEmbedding))
429429

430+
/-- **Correlation is invariant under graph equality across *all* instances**:
431+
strengthens `correlation_congr_of_eq` to also absorb differences in the vertex
432+
`Fintype` and `edgeSet Fintype` instances, since `Fintype` is a `Subsingleton`
433+
(mathlib `Fintype.subsingleton`). For propositionally equal graphs `G₁ = G₂` on
434+
the same vertex type, the correlations agree regardless of which `Fintype ι`,
435+
`Fintype Gᵢ.edgeSet` instances are in play. This is the tool that bridges the
436+
`Finset.Subtype.fintype` (used by `inducedGraph`) and the `Set`-induce vertex
437+
`Fintype` in the per-stage-increment assembly (Issue #2965, Phase A). -/
438+
theorem correlation_congr_all {ι : Type*} [DecidableEq ι] {inst₁ inst₂ : Fintype ι}
439+
{G₁ G₂ : SimpleGraph ι} {e₁ : Fintype G₁.edgeSet} {e₂ : Fintype G₂.edgeSet}
440+
(hG : G₁ = G₂) (params : IsingParams ℝ) (A : Finset ι) :
441+
@correlation ι inst₁ _ G₁ e₁ params A = @correlation ι inst₂ _ G₂ e₂ params A := by
442+
subst hG
443+
rw [Subsingleton.elim inst₁ inst₂, Subsingleton.elim e₁ e₂]
444+
445+
set_option linter.unusedFintypeInType false in
446+
/-- **Bond-deleted raw correlation equals isolated induced-subgraph correlation**:
447+
combining the component-factorization capstone
448+
`correlation_inducedGraph_deleteEdges_union_inl` with
449+
`correlation_induce_of_forall_mem` (on the full set `↑(S ∪ Sᶜ)`) and the
450+
all-instance bridge `correlation_congr_all`, an `S`-supported observable has the
451+
same correlation in the *raw* bond-deleted graph `G.deleteEdges {straddle S}` as
452+
in the isolated induced subgraph on `S` of the original model. This is the
453+
per-stage-increment form that pairs directly with the ball-boundary bond-deletion
454+
increment `correlation_sub_deleteEdges_le_derivBound` (Issue #2965, Phase A). -/
455+
theorem correlation_deleteEdges_straddle_eq_inducedGraph [Fintype V] (G : SimpleGraph V)
456+
(S : Finset V)
457+
[Fintype (inducedGraph (G.deleteEdges {e : Sym2 V |
458+
¬ Sym2.lift ⟨fun a b => ((a ∈ S) ↔ (b ∈ S)), fun a b => by simp [iff_comm]⟩ e}) S).edgeSet]
459+
[Fintype (inducedGraph (G.deleteEdges {e : Sym2 V |
460+
¬ Sym2.lift ⟨fun a b => ((a ∈ S) ↔ (b ∈ S)), fun a b => by simp [iff_comm]⟩ e}) Sᶜ).edgeSet]
461+
[Fintype (((inducedGraph (G.deleteEdges {e : Sym2 V |
462+
¬ Sym2.lift ⟨fun a b => ((a ∈ S) ↔ (b ∈ S)), fun a b => by simp [iff_comm]⟩ e}) S).sum
463+
(inducedGraph (G.deleteEdges {e : Sym2 V |
464+
¬ Sym2.lift ⟨fun a b => ((a ∈ S) ↔ (b ∈ S)), fun a b => by simp [iff_comm]⟩ e}) Sᶜ)).map
465+
(Equiv.Finset.union S Sᶜ disjoint_compl_right).toEmbedding).edgeSet]
466+
[Fintype (inducedGraph (G.deleteEdges {e : Sym2 V |
467+
¬ Sym2.lift ⟨fun a b => ((a ∈ S) ↔ (b ∈ S)), fun a b => by simp [iff_comm]⟩ e})
468+
(S ∪ Sᶜ)).edgeSet]
469+
[Fintype ((G.deleteEdges {e : Sym2 V |
470+
¬ Sym2.lift ⟨fun a b => ((a ∈ S) ↔ (b ∈ S)), fun a b => by simp [iff_comm]⟩ e}).induce
471+
(↑(S ∪ Sᶜ) : Set V)).edgeSet]
472+
[Fintype (G.deleteEdges {e : Sym2 V |
473+
¬ Sym2.lift ⟨fun a b => ((a ∈ S) ↔ (b ∈ S)), fun a b => by simp [iff_comm]⟩ e}).edgeSet]
474+
[Fintype (inducedGraph G S).edgeSet]
475+
(params : IsingParams ℝ) (A : Finset (↑S : Type _)) :
476+
correlation (G.deleteEdges {e : Sym2 V |
477+
¬ Sym2.lift ⟨fun a b => ((a ∈ S) ↔ (b ∈ S)), fun a b => by simp [iff_comm]⟩ e}) params
478+
((((A.map ⟨Sum.inl, Sum.inl_injective⟩).map
479+
(Equiv.Finset.union S Sᶜ disjoint_compl_right).toEmbedding).map
480+
(Equiv.subtypeUnivEquiv (p := fun x => x ∈ (↑(S ∪ Sᶜ) : Set V))
481+
(fun x => by
482+
rw [Finset.union_compl, Finset.coe_univ]; exact Set.mem_univ x)).toEmbedding))
483+
= correlation (inducedGraph G S) params A := by
484+
refine (correlation_induce_of_forall_mem _ (↑(S ∪ Sᶜ) : Set V)
485+
(fun x => by rw [Finset.union_compl, Finset.coe_univ]; exact Set.mem_univ x) params
486+
((A.map ⟨Sum.inl, Sum.inl_injective⟩).map
487+
(Equiv.Finset.union S Sᶜ disjoint_compl_right).toEmbedding)).symm.trans
488+
((correlation_congr_all rfl params
489+
((A.map ⟨Sum.inl, Sum.inl_injective⟩).map
490+
(Equiv.Finset.union S Sᶜ disjoint_compl_right).toEmbedding)).trans
491+
(correlation_inducedGraph_deleteEdges_union_inl G S params A))
492+
430493
end IsingModel

‎docs/index.md‎

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -371,6 +371,8 @@ Named specializations at `A = {i}`:
371371
| `inducedGraph_deleteEdges_eq_of_not_internal` | If no edge of the deleted set `D` has both endpoints in `S`, then `inducedGraph (G.deleteEdges D) S = inducedGraph G S` (deleting cut/cross edges leaves the within-`S` induced subgraph unchanged). Lets the bond-deleted model's induced subgraph on `S` be identified with the original's, so `correlation_inducedGraph_union_inl_of_no_cross` applies to `G.deleteEdges (cross edges)` (whose cut edges are gone, hence no-cross holds) — the Finset route to the bond-deletion → isolated-component bridge (Issue #2965, Phase A) | `InducedUnion.lean` | Component split (Issue #2965) |
372372
| `correlation_induce_univ` | `correlation (G.induce Set.univ) p A = correlation G p (A.map (Equiv.Set.univ V))` — since `G.induce Set.univ ≃g G` (mathlib `induceUnivIso`), pushing the observable along the relabeling preserves the correlation. Connects `inducedGraph _ univ` statements (the left side of `correlation_inducedGraph_deleteEdges_union_inl`) back to the raw graph `G` (the form of `correlation_sub_deleteEdges_le_derivBound`) for the per-stage increment assembly (Issue #2965, Phase A) | `InducedUnion.lean` | Component split (Issue #2965) |
373373
| `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) |
374+
| `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) |
375+
| `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) |
374376
| `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) |
375377
| `partitionFunction_ge_one_of_ferromagnetic` / `log_partitionFunction_nonneg_of_ferromagnetic` | `Z_G ≥ 1` (ferromagnetic), log form | `FreeEnergy.lean` | Step 5/Fekete infra |
376378
| `{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‎

Lines changed: 28 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -12646,6 +12646,34 @@ \subsection{Super-additivity on Finset disjoint union
1264612646
\texttt{correlation\_induce\_univ}.
1264712647
\end{proposition}
1264812648

12649+
\begin{proposition}[\texttt{IsingModel.correlation\_congr\_all}]
12650+
If $G_1=G_2$ then
12651+
$\langle\sigma^{A}\rangle_{G_1}=\langle\sigma^{A}\rangle_{G_2}$ regardless of the
12652+
vertex \texttt{Fintype} and \texttt{edgeSet Fintype} instances, since
12653+
\texttt{Fintype} is a \texttt{Subsingleton} (\texttt{Fintype.subsingleton}):
12654+
after \texttt{subst}, \texttt{Subsingleton.elim} equates the residual instances.
12655+
Strengthens \texttt{correlation\_congr\_of\_eq} and bridges the
12656+
\texttt{Finset.Subtype.fintype} (from \texttt{inducedGraph}) against the
12657+
\texttt{Set}-induce vertex \texttt{Fintype}.
12658+
\end{proposition}
12659+
12660+
\begin{theorem}[\texttt{IsingModel.correlation\_deleteEdges\_straddle\_eq\_inducedGraph}
12661+
(per-stage-increment form)]
12662+
For $S\subseteq V$ and an $S$-supported observable $A$,
12663+
\[
12664+
\langle\sigma^{A}\rangle_{G.\mathrm{deleteEdges}\,\{\text{straddle }S\}}
12665+
= \langle\sigma^{A}\rangle_{\mathrm{inducedGraph}\,G\,S},
12666+
\]
12667+
i.e.\ the \emph{raw} bond-deleted graph's correlation of an $S$-internal
12668+
observable equals the isolated induced-subgraph correlation. Composes
12669+
\texttt{correlation\_induce\_of\_forall\_mem} (on the full set
12670+
$\uparrow(S\cup S^{c})$), \texttt{correlation\_congr\_all}, and the
12671+
component-factorization capstone below. It is intended to pair with the
12672+
ball-boundary increment \texttt{correlation\_sub\_deleteEdges\_le\_derivBound}
12673+
toward the per-stage exhaustion increment bound; that composition (finite
12674+
edge-set, observable reduction to the pair $\{r,s\}$) is not yet formalized here.
12675+
\end{theorem}
12676+
1264912677
\begin{theorem}[\texttt{IsingModel.correlation\_inducedGraph\_deleteEdges\_union\_inl}
1265012678
(Phase A component-factorization capstone, Finset route)]
1265112679
For a region $S\subseteq W$, deleting the cut edges between $S$ and its complement

0 commit comments

Comments
 (0)