Skip to content

Commit 4108742

Browse files
phasetrclaude
phasetr
and
claude
authored
Build two-box per-stage increment for cubic exhaustion stages — #2965 (#2992)
* feat: two-box per-stage increment (Part of #2965) * Build two-box per-stage increment for cubic exhaustion stages Add `correlation_pair_two_box_le_derivBound`: for nested finsets T₁ ⊆ T₂ and a pair r,s interior to T₁, the pair correlation on the larger box exceeds the one on the smaller box by at most the ball-boundary `derivBound` over the cut edges of the T₁-slice. This is the form instantiated on cubic exhaustion stages box_k ⊆ box_{k+1} to bound the per-stage difference c_{k+1} − c_k (Issue #2965, Phase A). Supporting declarations: - `nestedFinsetEquiv`: the double-subtype relabeling ↥(T₁.subtype (· ∈ T₂)) ≃ ↥T₁. - `correlation_inducedGraph_nested_finset`: concrete-layer companion of `correlation_inducedGraph_induce_preimage` (#2991) using the `Finset.subtype` slice instead of a `Set`-predicate, so it matches the `S : Finset ↥T₂` region of the single-box increment directly and avoids the ↥S vs {x // x.val ∈ T₁} subtype-type mismatch. Composes the single-box increment `correlation_pair_sub_inducedGraph_le_derivBound` (#2989) on G' = inducedGraph G T₂ with the double-induce identification, recovering inducedGraph G T₁ on the inner box. Docs and proof-guide synced. Part of #2965 Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com> * Update module doc Main declarations list (codex cross-check) Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com> --------- Co-authored-by: Claude Opus 4.7 <noreply@anthropic.com>
1 parent 65daed6 commit 4108742

3 files changed

Lines changed: 181 additions & 2 deletions

File tree

‎IsingModel/AmbientLatticeSum/PerStageIncrement.lean‎

Lines changed: 131 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -14,9 +14,18 @@ subgraph on `S`:
1414
`correlation G p {r,s} − correlation (inducedGraph G S) p {⟨r,_⟩,⟨s,_⟩}
1515
≤ derivBound G (G.edgeFinset.filter straddle) p r s`.
1616
17-
## Main declaration
17+
It then instantiates this on nested finsets `T₁ ⊆ T₂` (via the double-subtype
18+
relabeling `nestedFinsetEquiv` and the double-induce identification
19+
`correlation_inducedGraph_nested_finset`) to obtain the two-box per-stage
20+
increment, the form used on cubic exhaustion stages `box_k ⊆ box_{k+1}` to bound
21+
`c_{k+1} − c_k`.
1822
19-
* `IsingModel.correlation_pair_sub_inducedGraph_le_derivBound`.
23+
## Main declarations
24+
25+
* `IsingModel.correlation_pair_sub_inducedGraph_le_derivBound` (single-box).
26+
* `IsingModel.nestedFinsetEquiv` and
27+
`IsingModel.correlation_inducedGraph_nested_finset` (double-induce identification).
28+
* `IsingModel.correlation_pair_two_box_le_derivBound` (two-box increment).
2029
-/
2130

2231
namespace IsingModel
@@ -112,4 +121,124 @@ theorem correlation_pair_sub_inducedGraph_le_derivBound (G : SimpleGraph V)
112121
(G.edgeFinset.filter (straddlePred S)) hnd (Finset.filter_subset _ _) p hf hh r s hrs hsep
113122
rwa [correlation_deleteEdges_filter_pair_eq G S p hr hs] at h1
114123

124+
/-- The double-subtype relabeling `↥(T₁.subtype (· ∈ T₂)) ≃ ↥T₁` for nested
125+
finsets `T₁ ⊆ T₂`. An element `x : ↥T₂` lies in `T₁.subtype (· ∈ T₂)` exactly when
126+
`x.val ∈ T₁` (`Finset.mem_subtype`), so the inner-subtype's underlying value
127+
recovers a member of `T₁`. This is the concrete-layer companion of
128+
`nestedSubtypeEquiv` used to instantiate the per-stage increment on the cubic
129+
exhaustion stages `box_k ⊆ box_{k+1}` (Issue #2965, Phase A). -/
130+
def nestedFinsetEquiv {T₁ T₂ : Finset V} (hsub : T₁ ⊆ T₂) :
131+
(↑(T₁.subtype (· ∈ T₂)) : Type _) ≃ (↑T₁ : Type _) where
132+
toFun x := ⟨x.val.val, Finset.mem_subtype.mp x.property⟩
133+
invFun y := ⟨⟨y.val, hsub y.property⟩, Finset.mem_subtype.mpr y.property⟩
134+
left_inv _ := by ext; rfl
135+
right_inv _ := by ext; rfl
136+
137+
set_option linter.unusedFintypeInType false in
138+
omit [Fintype V] in
139+
/-- **Double induced subgraph correlation = direct induced subgraph correlation**:
140+
for nested finsets `T₁ ⊆ T₂`, the correlation of the isolated induced subgraph on
141+
the `T₁`-slice `T₁.subtype (· ∈ T₂)` inside `inducedGraph G T₂` equals the
142+
correlation of the direct induced subgraph `inducedGraph G T₁`, after relabeling
143+
the observable along `nestedFinsetEquiv`. Proved by the same technique as
144+
`correlation_inducedGraph_induce_preimage` (#2991): `correlation_map_equiv` is
145+
applied to the *direct* graph `inducedGraph G T₁`, keeping the heavy double-induce
146+
graph only as the map result, then `correlation_congr_all` absorbs the edge-set
147+
`Fintype` instances. Instantiates the per-stage increment on cubic stages
148+
`box_k ⊆ box_{k+1}` (Issue #2965, Phase A). -/
149+
theorem correlation_inducedGraph_nested_finset (G : SimpleGraph V) {T₁ T₂ : Finset V}
150+
(hsub : T₁ ⊆ T₂)
151+
[Fintype (inducedGraph G T₁).edgeSet]
152+
[Fintype ((inducedGraph G T₁).map (nestedFinsetEquiv hsub).symm.toEmbedding).edgeSet]
153+
[Fintype (inducedGraph (inducedGraph G T₂) (T₁.subtype (· ∈ T₂))).edgeSet]
154+
(p : IsingParams ℝ) (A : Finset (↑T₁ : Type _)) :
155+
correlation (inducedGraph (inducedGraph G T₂) (T₁.subtype (· ∈ T₂))) p
156+
(A.map (nestedFinsetEquiv hsub).symm.toEmbedding)
157+
= correlation (inducedGraph G T₁) p A := by
158+
have hmap2 : (inducedGraph G T₁).map (nestedFinsetEquiv hsub).symm.toEmbedding
159+
= inducedGraph (inducedGraph G T₂) (T₁.subtype (· ∈ T₂)) := by
160+
ext a b
161+
simp only [SimpleGraph.map_adj, inducedGraph_apply, SimpleGraph.comap_adj]
162+
constructor
163+
· rintro ⟨x, y, hxy, rfl, rfl⟩
164+
exact hxy
165+
· intro h
166+
refine ⟨nestedFinsetEquiv hsub a, nestedFinsetEquiv hsub b, ?_, by simp, by simp⟩
167+
simpa [nestedFinsetEquiv] using h
168+
have key := correlation_map_equiv (nestedFinsetEquiv hsub).symm (inducedGraph G T₁) p A
169+
rw [correlation_congr_all hmap2 p (A.map (nestedFinsetEquiv hsub).symm.toEmbedding)] at key
170+
exact key
171+
172+
omit [Fintype V] in
173+
/-- The pair `{⟨r,hr₁⟩, ⟨s,hs₁⟩} : Finset ↥T₁` maps under `nestedFinsetEquiv.symm`
174+
to the corresponding pair in the `T₁`-slice `T₁.subtype (· ∈ T₂)` of `↥T₂`. -/
175+
private theorem pair_map_nestedFinsetEquiv_symm {T₁ T₂ : Finset V} (hsub : T₁ ⊆ T₂)
176+
{r s : V} (hr₁ : r ∈ T₁) (hs₁ : s ∈ T₁) :
177+
({⟨r, hr₁⟩, ⟨s, hs₁⟩} : Finset (↑T₁ : Type _)).map
178+
(nestedFinsetEquiv hsub).symm.toEmbedding
179+
= {⟨⟨r, hsub hr₁⟩, Finset.mem_subtype.mpr hr₁⟩,
180+
⟨⟨s, hsub hs₁⟩, Finset.mem_subtype.mpr hs₁⟩} := by
181+
rw [Finset.map_insert, Finset.map_singleton]
182+
rfl
183+
184+
set_option linter.unusedFintypeInType false in
185+
omit [Fintype V] in
186+
/-- **Two-box per-stage correlation increment** (Issue #2965, Phase A): for nested
187+
finsets `T₁ ⊆ T₂` and a pair `r, s` interior to `T₁` (neither endpoint on a cut
188+
edge of the `T₁`-slice), the pair correlation on the larger box exceeds the one on
189+
the smaller box by at most the ball-boundary `derivBound` over the cut edges of the
190+
slice. Composes `correlation_pair_sub_inducedGraph_le_derivBound` (the single-box
191+
increment) on `G' = inducedGraph G T₂` with the double-induce identification
192+
`correlation_inducedGraph_nested_finset`, recovering `inducedGraph G T₁` on the
193+
inner box. This is the form instantiated on cubic exhaustion stages
194+
`box_k ⊆ box_{k+1}` to bound `c_{k+1} − c_k`. -/
195+
theorem correlation_pair_two_box_le_derivBound (G : SimpleGraph V) {T₁ T₂ : Finset V}
196+
(hsub : T₁ ⊆ T₂) (p : IsingParams ℝ) (hf : Ferromagnetic p) (hh : p.h = 0)
197+
{r s : V} (hr₁ : r ∈ T₁) (hs₁ : s ∈ T₁) (hrs : r ≠ s)
198+
[Fintype (inducedGraph G T₂).edgeSet]
199+
(hsep : ∀ e ∈ (inducedGraph G T₂).edgeFinset.filter
200+
(straddlePred (T₁.subtype (· ∈ T₂))),
201+
¬ Sym2.Mem (⟨r, hsub hr₁⟩ : (↑T₂ : Type _)) e ∧
202+
¬ Sym2.Mem (⟨s, hsub hs₁⟩ : (↑T₂ : Type _)) e)
203+
[Fintype ((inducedGraph G T₂).deleteEdges
204+
↑((inducedGraph G T₂).edgeFinset.filter
205+
(straddlePred (T₁.subtype (· ∈ T₂))))).edgeSet]
206+
[Fintype ((inducedGraph G T₂).deleteEdges
207+
{e : Sym2 (↑T₂ : Type _) | straddlePred (T₁.subtype (· ∈ T₂)) e}).edgeSet]
208+
[Fintype (inducedGraph ((inducedGraph G T₂).deleteEdges
209+
{e : Sym2 (↑T₂ : Type _) | straddlePred (T₁.subtype (· ∈ T₂)) e})
210+
(T₁.subtype (· ∈ T₂))).edgeSet]
211+
[Fintype (inducedGraph ((inducedGraph G T₂).deleteEdges
212+
{e : Sym2 (↑T₂ : Type _) | straddlePred (T₁.subtype (· ∈ T₂)) e})
213+
(T₁.subtype (· ∈ T₂))ᶜ).edgeSet]
214+
[Fintype (((inducedGraph ((inducedGraph G T₂).deleteEdges
215+
{e : Sym2 (↑T₂ : Type _) | straddlePred (T₁.subtype (· ∈ T₂)) e})
216+
(T₁.subtype (· ∈ T₂))).sum
217+
(inducedGraph ((inducedGraph G T₂).deleteEdges
218+
{e : Sym2 (↑T₂ : Type _) | straddlePred (T₁.subtype (· ∈ T₂)) e})
219+
(T₁.subtype (· ∈ T₂))ᶜ)).map
220+
(Equiv.Finset.union (T₁.subtype (· ∈ T₂)) (T₁.subtype (· ∈ T₂))ᶜ
221+
disjoint_compl_right).toEmbedding).edgeSet]
222+
[Fintype (inducedGraph ((inducedGraph G T₂).deleteEdges
223+
{e : Sym2 (↑T₂ : Type _) | straddlePred (T₁.subtype (· ∈ T₂)) e})
224+
((T₁.subtype (· ∈ T₂)) ∪ (T₁.subtype (· ∈ T₂))ᶜ)).edgeSet]
225+
[Fintype (((inducedGraph G T₂).deleteEdges
226+
{e : Sym2 (↑T₂ : Type _) | straddlePred (T₁.subtype (· ∈ T₂)) e}).induce
227+
(↑((T₁.subtype (· ∈ T₂)) ∪ (T₁.subtype (· ∈ T₂))ᶜ) : Set (↑T₂ : Type _))).edgeSet]
228+
[Fintype (inducedGraph (inducedGraph G T₂) (T₁.subtype (· ∈ T₂))).edgeSet]
229+
[Fintype (inducedGraph G T₁).edgeSet]
230+
[Fintype ((inducedGraph G T₁).map (nestedFinsetEquiv hsub).symm.toEmbedding).edgeSet] :
231+
correlation (inducedGraph G T₂) p {⟨r, hsub hr₁⟩, ⟨s, hsub hs₁⟩}
232+
- correlation (inducedGraph G T₁) p {⟨r, hr₁⟩, ⟨s, hs₁⟩}
233+
≤ derivBound (inducedGraph G T₂) ((inducedGraph G T₂).edgeFinset.filter
234+
(straddlePred (T₁.subtype (· ∈ T₂)))) p ⟨r, hsub hr₁⟩ ⟨s, hsub hs₁⟩ := by
235+
have hrs' : (⟨r, hsub hr₁⟩ : (↑T₂ : Type _)) ≠ ⟨s, hsub hs₁⟩ := by
236+
simpa [Subtype.ext_iff] using hrs
237+
have h1 := correlation_pair_sub_inducedGraph_le_derivBound (inducedGraph G T₂)
238+
(T₁.subtype (· ∈ T₂)) p hf hh ⟨r, hsub hr₁⟩ ⟨s, hsub hs₁⟩
239+
(Finset.mem_subtype.mpr hr₁) (Finset.mem_subtype.mpr hs₁) hrs' hsep
240+
rw [← pair_map_nestedFinsetEquiv_symm hsub hr₁ hs₁,
241+
correlation_inducedGraph_nested_finset G hsub p {⟨r, hr₁⟩, ⟨s, hs₁⟩}] at h1
242+
exact h1
243+
115244
end IsingModel

‎docs/index.md‎

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -378,6 +378,8 @@ Named specializations at `A = {i}`:
378378
| `correlation_pair_sub_inducedGraph_le_derivBound` | **Numeric per-stage correlation increment (Phase A).** For `r,s ∈ S`, `r ≠ s`, ferromagnetic, `h=0`, and `r,s` not on any cut (straddle) edge: `correlation G p {r,s} − correlation (inducedGraph G S) p {⟨r,_⟩,⟨s,_⟩} ≤ derivBound G (G.edgeFinset.filter straddle) p r s`. Composes the ball-boundary bond-deletion increment `correlation_sub_deleteEdges_le_derivBound` (#2974) with the component-factorization bridge `correlation_deleteEdges_straddle_eq_inducedGraph` (#2986) via `deleteEdges_filter_edgeFinset_eq` (#2987) + `correlation_congr_all` + `triple_map_subtypeUnivEquiv_eq` (#2988). The full-model pair correlation exceeds the isolated induced-subgraph pair correlation by at most the boundary `derivBound` over the cut edges | `PerStageIncrement.lean` | Per-stage increment (Issue #2965) |
379379
| `nestedSubtypeEquiv` / `inducedGraph_induce_preimage_map_eq` | For `S ⊆ T`, `((inducedGraph G T).induce {x : ↥T \| x.val ∈ S}).map nestedSubtypeEquiv = inducedGraph G S` — the nested induced subgraph (induce `box_k` inside `inducedGraph G box_{k+1}`) equals, up to the nested-subtype relabeling `{x : ↥T // x.val ∈ S} ≃ ↥S`, the direct induced subgraph on `S`. Graph-level foundation for instantiating the per-stage increment on cubic exhaustion stages `box_k ⊆ box_{k+1}` | `InducedUnion.lean` | Nested induce (Issue #2965) |
380380
| `correlation_inducedGraph_induce_preimage` | Correlation companion of the above: `correlation ((inducedGraph G T).induce {x \| x.val ∈ S}) p (A.map nestedSubtypeEquiv.symm) = correlation (inducedGraph G S) p A`. Proved by applying `correlation_map_equiv` to the *direct* `inducedGraph G S` with `nestedSubtypeEquiv.symm` (so the heavy nested-subtype graph is only the map *result*, never the graph `correlation_map_equiv` operates on — bypassing the `whnf` wall), then bridging via `correlation_congr_all` + the graph equality. The `c_k`-side identity for the cubic-exhaustion per-stage increment (Issue #2965) | `InducedUnion.lean` | Nested induce (Issue #2965) |
381+
| `nestedFinsetEquiv` / `correlation_inducedGraph_nested_finset` | **Double-induce correlation identification (Finset route).** For `T₁ ⊆ T₂`, `correlation (inducedGraph (inducedGraph G T₂) (T₁.subtype (· ∈ T₂))) p (A.map nestedFinsetEquiv.symm) = correlation (inducedGraph G T₁) p A`, where `nestedFinsetEquiv : ↥(T₁.subtype (· ∈ T₂)) ≃ ↥T₁`. The concrete-layer companion of `correlation_inducedGraph_induce_preimage` (#2991), using the `Finset.subtype` slice instead of a `Set`-predicate so it matches the `S : Finset ↥T₂` of the single-box increment directly (avoiding the `↥S` vs `{x // x.val ∈ T₁}` type mismatch). Same `correlation_map_equiv`-on-the-direct-graph proof scheme | `PerStageIncrement.lean` | Nested induce (Issue #2965) |
382+
| `correlation_pair_two_box_le_derivBound` | **Two-box per-stage correlation increment (Phase A).** For nested finsets `T₁ ⊆ T₂`, `r,s ∈ T₁`, `r ≠ s`, ferromagnetic, `h=0`, and `r,s` not on any cut edge of the `T₁`-slice: `correlation (inducedGraph G T₂) p {⟨r,_⟩,⟨s,_⟩} − correlation (inducedGraph G T₁) p {⟨r,_⟩,⟨s,_⟩} ≤ derivBound (inducedGraph G T₂) (filter straddle) p ⟨r,_⟩ ⟨s,_⟩`. Composes the single-box increment `correlation_pair_sub_inducedGraph_le_derivBound` (#2989) on `G' = inducedGraph G T₂` with the double-induce identification `correlation_inducedGraph_nested_finset`, recovering `inducedGraph G T₁` on the inner box. The form instantiated on cubic exhaustion stages `box_k ⊆ box_{k+1}` to bound `c_{k+1} − c_k` | `PerStageIncrement.lean` | Per-stage increment (Issue #2965) |
381383
| `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) |
382384
| `partitionFunction_ge_one_of_ferromagnetic` / `log_partitionFunction_nonneg_of_ferromagnetic` | `Z_G ≥ 1` (ferromagnetic), log form | `FreeEnergy.lean` | Step 5/Fekete infra |
383385
| `{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: 48 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -12771,6 +12771,54 @@ \subsection{Super-additivity on Finset disjoint union
1277112771
elaboration within the heartbeat budget.
1277212772
\end{proof}
1277312773

12774+
\begin{proposition}[\texttt{IsingModel.correlation\_inducedGraph\_nested\_finset}]
12775+
For nested finsets $T_1\subseteq T_2$ and an observable $A$ on $\uparrow T_1$,
12776+
\[
12777+
\langle\sigma^{A.\mathrm{map}\,e^{-1}}\rangle_{\mathrm{inducedGraph}\,
12778+
(\mathrm{inducedGraph}\,G\,T_2)\,(T_1.\mathrm{subtype}\,(\cdot\in T_2))}
12779+
= \langle\sigma^{A}\rangle_{\mathrm{inducedGraph}\,G\,T_1},
12780+
\]
12781+
where $e=\mathrm{nestedFinsetEquiv}\colon \uparrow(T_1.\mathrm{subtype}\,(\cdot\in
12782+
T_2))\simeq\uparrow T_1$ is the double-subtype relabeling. This is the
12783+
concrete-layer companion of \texttt{correlation\_inducedGraph\_induce\_preimage}:
12784+
it uses the \texttt{Finset.subtype} slice $T_1.\mathrm{subtype}\,(\cdot\in T_2)$
12785+
rather than the $\mathrm{Set}$-predicate $\{x\mid x.\mathrm{val}\in T_1\}$, so it
12786+
matches the $S:\mathrm{Finset}\,\uparrow T_2$ region of the single-box increment
12787+
directly, sidestepping the $\uparrow S$ versus $\{x\mathbin{/\!/}x.\mathrm{val}\in
12788+
T_1\}$ subtype-type mismatch. Same proof scheme: apply
12789+
\texttt{correlation\_map\_equiv} to the \emph{direct} graph
12790+
$\mathrm{inducedGraph}\,G\,T_1$ with $e^{-1}$, then bridge via
12791+
\texttt{correlation\_congr\_all} and the graph equality (an edge survives the
12792+
double induce iff its deep endpoints are $G$-adjacent and both in $T_1$).
12793+
\end{proposition}
12794+
12795+
\begin{theorem}[\texttt{IsingModel.correlation\_pair\_two\_box\_le\_derivBound}
12796+
(two-box per-stage increment, Issue \#2965 Phase A)]
12797+
For nested finsets $T_1\subseteq T_2$, a pair $r,s\in T_1$ with $r\neq s$,
12798+
ferromagnetic parameters at $h=0$, and $r,s$ on no cut edge of the $T_1$-slice,
12799+
\[
12800+
\langle\sigma_r\sigma_s\rangle_{\mathrm{inducedGraph}\,G\,T_2}
12801+
- \langle\sigma_r\sigma_s\rangle_{\mathrm{inducedGraph}\,G\,T_1}
12802+
\le \mathrm{derivBound}\,(\mathrm{inducedGraph}\,G\,T_2)\,
12803+
(\mathrm{filter}\,\mathrm{straddle})\,r\,s,
12804+
\]
12805+
i.e.\ enlarging the box from $T_1$ to $T_2$ increases the pair correlation by at
12806+
most the ball-boundary $\mathrm{derivBound}$ over the cut edges of the slice. This
12807+
is the form instantiated on cubic exhaustion stages $\mathrm{box}_k\subseteq
12808+
\mathrm{box}_{k+1}$ to bound the per-stage difference $c_{k+1}-c_k$.
12809+
\end{theorem}
12810+
12811+
\begin{proof}
12812+
Apply the single-box increment
12813+
\texttt{correlation\_pair\_sub\_inducedGraph\_le\_derivBound} to
12814+
$G'=\mathrm{inducedGraph}\,G\,T_2$ with region
12815+
$S=T_1.\mathrm{subtype}\,(\cdot\in T_2)$ and pair $\langle r,\_\rangle,
12816+
\langle s,\_\rangle$ (in $S$ since their values lie in $T_1$, by
12817+
\texttt{Finset.mem\_subtype}). Then identify the inner-box correlation via
12818+
\texttt{correlation\_inducedGraph\_nested\_finset}, rewriting the pair observable
12819+
along $e^{-1}$ with \texttt{pair\_map\_nestedFinsetEquiv\_symm}.
12820+
\end{proof}
12821+
1277412822
\begin{theorem}[\texttt{IsingModel.correlation\_inducedGraph\_deleteEdges\_union\_inl}
1277512823
(Phase A component-factorization capstone, Finset route)]
1277612824
For a region $S\subseteq W$, deleting the cut edges between $S$ and its complement

0 commit comments

Comments
 (0)