From 820c4bb371aa891970418e5462ecf29a2443f682 Mon Sep 17 00:00:00 2001 From: phasetr Date: Mon, 4 May 2026 23:10:18 +0900 Subject: [PATCH 1/2] =?UTF-8?q?wip:=20=C2=A718.5=20vdPolymerFamilies=5Fsum?= =?UTF-8?q?=20generic-t=20bound=20family=204-layer=20wraps?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit From 51ecc18a113bd360667451bb9c9d38386eee5770 Mon Sep 17 00:00:00 2001 From: phasetr Date: Mon, 4 May 2026 23:14:47 +0900 Subject: [PATCH 2/2] =?UTF-8?q?feat:=20=C2=A718.5=20vdPolymerFamilies=5Fsu?= =?UTF-8?q?m=20generic-t=20bound=20family=204-layer=20wraps?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Lifts the four abstract generic-t bound family theorems (which had no wrappers prior) to all 4 volume layers: - `vdPolymerFamilies_sum_ge_one_of_nonneg` (`1 ≤ vdSum` under `0 ≤ t`, generalises `one_le_vdPolymerFamilies_sum` from tanh) - `vdPolymerFamilies_sum_le_one_plus_pow_of_nonneg` (`vdSum ≤ (1+t)^|E|` under `0 ≤ t`) - `vdPolymerFamilies_sum_pos_of_nonneg` (`0 < vdSum` under `0 ≤ t`, ensures `Real.log (vdSum)` well-defined) - `vdPolymerFamilies_sum_eq_one_add` (`vdSum = 1 + ε(t)` decomposition for the `log(1+ε)` Mayer expansion) Bundle contents: 16 new theorems (4 abstracts × 4 layers). `docs/index.md` §18.5 row + `tex/proof-guide.tex` updated. `lake build` clean (zero linter warnings); `grep -rn "sorry" IsingModel/` = 0; `lake exe GKSTest` passes. Part of #1344. Co-Authored-By: Claude Opus 4.7 (1M context) --- IsingModel/AmbientLattice/Analyticity.lean | 42 +++++++ IsingModel/AmbientLattice/SpecialCases.lean | 46 ++++++++ .../Concrete/LatticeGraphCorrelation.lean | 104 ++++++++++++++++++ docs/index.md | 2 +- tex/proof-guide.tex | 16 +++ 5 files changed, 209 insertions(+), 1 deletion(-) diff --git a/IsingModel/AmbientLattice/Analyticity.lean b/IsingModel/AmbientLattice/Analyticity.lean index 2f922d2d4..12986e243 100644 --- a/IsingModel/AmbientLattice/Analyticity.lean +++ b/IsingModel/AmbientLattice/Analyticity.lean @@ -1480,5 +1480,47 @@ theorem one_le_vdPolymerFamilies_sum_Λ ∏ P ∈ Γ, Real.tanh (β * J) ^ P.card := IsingModel.one_le_vdPolymerFamilies_sum (inducedGraph G Λ) hβJ +/-! ### §18.5 vdPolymerFamilies_sum generic-t bounds Λ-layer -/ + +/-- **Λ-layer: 1 ≤ vdSum** under `0 ≤ t`. -/ +theorem vdPolymerFamilies_sum_Λ_ge_one_of_nonneg + (G : SimpleGraph V) (Λ : Finset V) + [Fintype (inducedGraph G Λ).edgeSet] + {t : ℝ} (ht : 0 ≤ t) : + 1 ≤ ∑ Γ ∈ IsingModel.vdCompatiblePolymerFamilies (inducedGraph G Λ), + ∏ P ∈ Γ, t ^ P.card := + IsingModel.vdPolymerFamilies_sum_ge_one_of_nonneg (inducedGraph G Λ) ht + +/-- **Λ-layer: vdSum ≤ (1+t)^|E|** under `0 ≤ t`. -/ +theorem vdPolymerFamilies_sum_Λ_le_one_plus_pow_of_nonneg + (G : SimpleGraph V) (Λ : Finset V) + [Fintype (inducedGraph G Λ).edgeSet] + {t : ℝ} (ht : 0 ≤ t) : + (∑ Γ ∈ IsingModel.vdCompatiblePolymerFamilies (inducedGraph G Λ), + ∏ P ∈ Γ, t ^ P.card) + ≤ (1 + t) ^ (inducedGraph G Λ).edgeFinset.card := + IsingModel.vdPolymerFamilies_sum_le_one_plus_pow_of_nonneg + (inducedGraph G Λ) ht + +/-- **Λ-layer: 0 < vdSum** under `0 ≤ t`. -/ +theorem vdPolymerFamilies_sum_Λ_pos_of_nonneg + (G : SimpleGraph V) (Λ : Finset V) + [Fintype (inducedGraph G Λ).edgeSet] + {t : ℝ} (ht : 0 ≤ t) : + 0 < ∑ Γ ∈ IsingModel.vdCompatiblePolymerFamilies (inducedGraph G Λ), + ∏ P ∈ Γ, t ^ P.card := + IsingModel.vdPolymerFamilies_sum_pos_of_nonneg (inducedGraph G Λ) ht + +/-- **Λ-layer: vdSum = 1 + ε(t)** decomposition. -/ +theorem vdPolymerFamilies_sum_Λ_eq_one_add + (G : SimpleGraph V) (Λ : Finset V) + [Fintype (inducedGraph G Λ).edgeSet] (t : ℝ) : + (∑ Γ ∈ IsingModel.vdCompatiblePolymerFamilies (inducedGraph G Λ), + ∏ P ∈ Γ, t ^ P.card) = + 1 + ∑ Γ ∈ (IsingModel.vdCompatiblePolymerFamilies + (inducedGraph G Λ)).erase ∅, + ∏ P ∈ Γ, t ^ P.card := + IsingModel.vdPolymerFamilies_sum_eq_one_add (inducedGraph G Λ) t + end Ambient end IsingModel diff --git a/IsingModel/AmbientLattice/SpecialCases.lean b/IsingModel/AmbientLattice/SpecialCases.lean index fd3300f7a..4b350566a 100644 --- a/IsingModel/AmbientLattice/SpecialCases.lean +++ b/IsingModel/AmbientLattice/SpecialCases.lean @@ -4010,5 +4010,51 @@ theorem one_le_vdPolymerFamilies_sumAlongExhaustion ∏ P ∈ Γ, Real.tanh (β * J) ^ P.card := one_le_vdPolymerFamilies_sum_Λ G (Λ.volume n) hβJ +/-! ### §18.5 vdPolymerFamilies_sum generic-t bounds along-ex -/ + +/-- **Along-ex: 1 ≤ vdSum** under `0 ≤ t`. -/ +theorem vdPolymerFamilies_sumAlongExhaustion_ge_one_of_nonneg + (G : SimpleGraph V) (Λ : Exhaustion V) + [∀ n, Fintype (inducedGraph G (Λ.volume n)).edgeSet] + {t : ℝ} (ht : 0 ≤ t) (n : ℕ) : + 1 ≤ ∑ Γ ∈ IsingModel.vdCompatiblePolymerFamilies + (inducedGraph G (Λ.volume n)), + ∏ P ∈ Γ, t ^ P.card := + vdPolymerFamilies_sum_Λ_ge_one_of_nonneg G (Λ.volume n) ht + +/-- **Along-ex: vdSum ≤ (1+t)^|E|** under `0 ≤ t`. -/ +theorem vdPolymerFamilies_sumAlongExhaustion_le_one_plus_pow_of_nonneg + (G : SimpleGraph V) (Λ : Exhaustion V) + [∀ n, Fintype (inducedGraph G (Λ.volume n)).edgeSet] + {t : ℝ} (ht : 0 ≤ t) (n : ℕ) : + (∑ Γ ∈ IsingModel.vdCompatiblePolymerFamilies + (inducedGraph G (Λ.volume n)), + ∏ P ∈ Γ, t ^ P.card) + ≤ (1 + t) ^ (inducedGraph G (Λ.volume n)).edgeFinset.card := + vdPolymerFamilies_sum_Λ_le_one_plus_pow_of_nonneg G (Λ.volume n) ht + +/-- **Along-ex: 0 < vdSum** under `0 ≤ t`. -/ +theorem vdPolymerFamilies_sumAlongExhaustion_pos_of_nonneg + (G : SimpleGraph V) (Λ : Exhaustion V) + [∀ n, Fintype (inducedGraph G (Λ.volume n)).edgeSet] + {t : ℝ} (ht : 0 ≤ t) (n : ℕ) : + 0 < ∑ Γ ∈ IsingModel.vdCompatiblePolymerFamilies + (inducedGraph G (Λ.volume n)), + ∏ P ∈ Γ, t ^ P.card := + vdPolymerFamilies_sum_Λ_pos_of_nonneg G (Λ.volume n) ht + +/-- **Along-ex: vdSum = 1 + ε(t)** decomposition. -/ +theorem vdPolymerFamilies_sumAlongExhaustion_eq_one_add + (G : SimpleGraph V) (Λ : Exhaustion V) + [∀ n, Fintype (inducedGraph G (Λ.volume n)).edgeSet] + (t : ℝ) (n : ℕ) : + (∑ Γ ∈ IsingModel.vdCompatiblePolymerFamilies + (inducedGraph G (Λ.volume n)), + ∏ P ∈ Γ, t ^ P.card) = + 1 + ∑ Γ ∈ (IsingModel.vdCompatiblePolymerFamilies + (inducedGraph G (Λ.volume n))).erase ∅, + ∏ P ∈ Γ, t ^ P.card := + vdPolymerFamilies_sum_Λ_eq_one_add G (Λ.volume n) t + end Ambient end IsingModel diff --git a/IsingModel/Concrete/LatticeGraphCorrelation.lean b/IsingModel/Concrete/LatticeGraphCorrelation.lean index 8f9def266..0f833c646 100644 --- a/IsingModel/Concrete/LatticeGraphCorrelation.lean +++ b/IsingModel/Concrete/LatticeGraphCorrelation.lean @@ -10581,6 +10581,110 @@ theorem one_le_vdPolymerFamilies_sumAlongExhaustion_latticeGraph Ambient.one_le_vdPolymerFamilies_sumAlongExhaustion (IsingModel.latticeGraph d) Λ hβJ n +/-! ### §18.5 vdPolymerFamilies_sum generic-t bounds ℤ^d wraps -/ + +/-- **ℤ^d Λ: 1 ≤ vdSum** under `0 ≤ t`. -/ +theorem vdPolymerFamilies_sum_Λ_latticeGraph_ge_one_of_nonneg + (d : ℕ) (Λ : Finset (Fin d → ℤ)) + [Fintype (inducedGraph (IsingModel.latticeGraph d) Λ).edgeSet] + {t : ℝ} (ht : 0 ≤ t) : + 1 ≤ ∑ Γ ∈ IsingModel.vdCompatiblePolymerFamilies + (inducedGraph (IsingModel.latticeGraph d) Λ), + ∏ P ∈ Γ, t ^ P.card := + Ambient.vdPolymerFamilies_sum_Λ_ge_one_of_nonneg + (IsingModel.latticeGraph d) Λ ht + +/-- **ℤ^d Λ: vdSum ≤ (1+t)^|E|** under `0 ≤ t`. -/ +theorem vdPolymerFamilies_sum_Λ_latticeGraph_le_one_plus_pow_of_nonneg + (d : ℕ) (Λ : Finset (Fin d → ℤ)) + [Fintype (inducedGraph (IsingModel.latticeGraph d) Λ).edgeSet] + {t : ℝ} (ht : 0 ≤ t) : + (∑ Γ ∈ IsingModel.vdCompatiblePolymerFamilies + (inducedGraph (IsingModel.latticeGraph d) Λ), + ∏ P ∈ Γ, t ^ P.card) + ≤ (1 + t) ^ + (inducedGraph (IsingModel.latticeGraph d) Λ).edgeFinset.card := + Ambient.vdPolymerFamilies_sum_Λ_le_one_plus_pow_of_nonneg + (IsingModel.latticeGraph d) Λ ht + +/-- **ℤ^d Λ: 0 < vdSum** under `0 ≤ t`. -/ +theorem vdPolymerFamilies_sum_Λ_latticeGraph_pos_of_nonneg + (d : ℕ) (Λ : Finset (Fin d → ℤ)) + [Fintype (inducedGraph (IsingModel.latticeGraph d) Λ).edgeSet] + {t : ℝ} (ht : 0 ≤ t) : + 0 < ∑ Γ ∈ IsingModel.vdCompatiblePolymerFamilies + (inducedGraph (IsingModel.latticeGraph d) Λ), + ∏ P ∈ Γ, t ^ P.card := + Ambient.vdPolymerFamilies_sum_Λ_pos_of_nonneg + (IsingModel.latticeGraph d) Λ ht + +/-- **ℤ^d Λ: vdSum = 1 + ε(t)** decomposition. -/ +theorem vdPolymerFamilies_sum_Λ_latticeGraph_eq_one_add + (d : ℕ) (Λ : Finset (Fin d → ℤ)) + [Fintype (inducedGraph (IsingModel.latticeGraph d) Λ).edgeSet] + (t : ℝ) : + (∑ Γ ∈ IsingModel.vdCompatiblePolymerFamilies + (inducedGraph (IsingModel.latticeGraph d) Λ), + ∏ P ∈ Γ, t ^ P.card) = + 1 + ∑ Γ ∈ (IsingModel.vdCompatiblePolymerFamilies + (inducedGraph (IsingModel.latticeGraph d) Λ)).erase ∅, + ∏ P ∈ Γ, t ^ P.card := + Ambient.vdPolymerFamilies_sum_Λ_eq_one_add + (IsingModel.latticeGraph d) Λ t + +/-- **ℤ^d along-ex: 1 ≤ vdSum** under `0 ≤ t`. -/ +theorem +vdPolymerFamilies_sumAlongExhaustion_latticeGraph_ge_one_of_nonneg + (d : ℕ) (Λ : Ambient.Exhaustion (Fin d → ℤ)) + [∀ n, Fintype (inducedGraph (IsingModel.latticeGraph d) + (Λ.volume n)).edgeSet] {t : ℝ} (ht : 0 ≤ t) (n : ℕ) : + 1 ≤ ∑ Γ ∈ IsingModel.vdCompatiblePolymerFamilies + (inducedGraph (IsingModel.latticeGraph d) (Λ.volume n)), + ∏ P ∈ Γ, t ^ P.card := + Ambient.vdPolymerFamilies_sumAlongExhaustion_ge_one_of_nonneg + (IsingModel.latticeGraph d) Λ ht n + +/-- **ℤ^d along-ex: vdSum ≤ (1+t)^|E|** under `0 ≤ t`. -/ +theorem +vdPolymerFamilies_sumAlongExhaustion_latticeGraph_le_one_plus_pow_of_nonneg + (d : ℕ) (Λ : Ambient.Exhaustion (Fin d → ℤ)) + [∀ n, Fintype (inducedGraph (IsingModel.latticeGraph d) + (Λ.volume n)).edgeSet] {t : ℝ} (ht : 0 ≤ t) (n : ℕ) : + (∑ Γ ∈ IsingModel.vdCompatiblePolymerFamilies + (inducedGraph (IsingModel.latticeGraph d) (Λ.volume n)), + ∏ P ∈ Γ, t ^ P.card) + ≤ (1 + t) ^ + (inducedGraph (IsingModel.latticeGraph d) + (Λ.volume n)).edgeFinset.card := + Ambient.vdPolymerFamilies_sumAlongExhaustion_le_one_plus_pow_of_nonneg + (IsingModel.latticeGraph d) Λ ht n + +/-- **ℤ^d along-ex: 0 < vdSum** under `0 ≤ t`. -/ +theorem vdPolymerFamilies_sumAlongExhaustion_latticeGraph_pos_of_nonneg + (d : ℕ) (Λ : Ambient.Exhaustion (Fin d → ℤ)) + [∀ n, Fintype (inducedGraph (IsingModel.latticeGraph d) + (Λ.volume n)).edgeSet] {t : ℝ} (ht : 0 ≤ t) (n : ℕ) : + 0 < ∑ Γ ∈ IsingModel.vdCompatiblePolymerFamilies + (inducedGraph (IsingModel.latticeGraph d) (Λ.volume n)), + ∏ P ∈ Γ, t ^ P.card := + Ambient.vdPolymerFamilies_sumAlongExhaustion_pos_of_nonneg + (IsingModel.latticeGraph d) Λ ht n + +/-- **ℤ^d along-ex: vdSum = 1 + ε(t)** decomposition. -/ +theorem vdPolymerFamilies_sumAlongExhaustion_latticeGraph_eq_one_add + (d : ℕ) (Λ : Ambient.Exhaustion (Fin d → ℤ)) + [∀ n, Fintype (inducedGraph (IsingModel.latticeGraph d) + (Λ.volume n)).edgeSet] (t : ℝ) (n : ℕ) : + (∑ Γ ∈ IsingModel.vdCompatiblePolymerFamilies + (inducedGraph (IsingModel.latticeGraph d) (Λ.volume n)), + ∏ P ∈ Γ, t ^ P.card) = + 1 + ∑ Γ ∈ (IsingModel.vdCompatiblePolymerFamilies + (inducedGraph (IsingModel.latticeGraph d) + (Λ.volume n))).erase ∅, + ∏ P ∈ Γ, t ^ P.card := + Ambient.vdPolymerFamilies_sumAlongExhaustion_eq_one_add + (IsingModel.latticeGraph d) Λ t n + end Ambient end IsingModel diff --git a/docs/index.md b/docs/index.md index 88e383fcd..acd4d2053 100644 --- a/docs/index.md +++ b/docs/index.md @@ -641,7 +641,7 @@ inventory (2026-04-17). | §18.2 | `exp(α·edgeSpin) = cosh α + sinh α · edgeSpin` | **Done** | `exp_edgeSpin_decomp` (`Inequalities/NonnegCorrelations.lean`). | | §18.3 | Clustering and analyticity (lattice high-temp expansion) | **Done (lattice + Λ-layer + ℤ^d)** | `partitionFunction_high_temp_expansion` (`Conditioning.lean`): `Z = (cosh βJ)^{\|E\|} · ∑_σ ∏_e (1 + tanh(βJ) σ_iσ_j) · exp(βh ∑ σ_i)`. Λ-layer + along-exhaustion + ℤ^d wrappers `partitionFunctionΛ_high_temp_expansion`, `partitionFunctionAlongExhaustion_high_temp_expansion`, etc. Zero-field corollary `partitionFunction_high_temp_expansion_h_zero` (Λ-layer + ℤ^d + along-exhaustion wrappers). **General-h subset expansion** `partitionFunction_high_temp_expansion_subset_form`: `Z = (cosh βJ)^{\|E\|} · ∑_{X ⊆ E} tanh(βJ)^{\|X\|} · ∑_σ (∏_{e ∈ X} σ_iσ_j) exp(βh ∑ σ_i)` — intermediate between Step 281 (full product) and Step 283 (h=0 closed form), with the residual σ-sum carrying field dependence. Λ-layer + ℤ^d wrappers `partitionFunctionΛ_high_temp_expansion_subset_form`, `partitionFunctionΛ_latticeGraph_high_temp_expansion_subset_form`. Along-exhaustion + ℤ^d wrappers `partitionFunctionAlongExhaustion_{,latticeGraph_}high_temp_expansion_subset_form`. **Closed form** `partitionFunction_high_temp_expansion_h_zero_closed`: `Z(J,0,β) = 2^{\|ι\|} · (cosh βJ)^{\|E\|} · ∑_{X ⊆ E, even-degree} tanh(βJ)^{\|X\|}` (FV §3.7.3 eq. (3.45)). Λ-layer + ℤ^d + along-exhaustion + ℤ^d-along-exhaustion wrappers. **J = 0 consistency check** `partitionFunction_high_temp_expansion_h_zero_closed_at_J_zero`: at `J = 0` the FV (3.45) closed form correctly reduces to `Z = 2^{\|ι\|}`, matching `partitionFunction_J_zero`. **β = 0 consistency check** `partitionFunction_high_temp_expansion_h_zero_closed_at_beta_zero`: dual at `β = 0`. Λ-layer + ℤ^d wrappers. Along-exhaustion + ℤ^d-along-exhaustion wrappers `partitionFunctionAlongExhaustion_{,latticeGraph_}high_temp_expansion_h_zero_closed_at_{J,beta}_zero`. Λ-layer + ℤ^d wrappers `partitionFunctionΛ_{,latticeGraph_}high_temp_expansion_h_zero_closed_at_J_zero`. **log Z decomposition** `log_partitionFunction_high_temp_expansion_h_zero_closed`: under `0 ≤ βJ`, `log Z = \|ι\| log 2 + \|E\| log cosh(βJ) + log(∑_{X even} tanh^{\|X\|})`. Λ-layer + ℤ^d + along-exhaustion wrappers. **Upper bound** `partitionFunction_high_temp_expansion_h_zero_upper_bound`: under `0 ≤ βJ`, `Z(J,0,β) ≤ 2^{\|ι\|+\|E\|} · (cosh βJ)^{\|E\|}` (from Step 319 sum-bound). Λ-layer + ℤ^d + along-exhaustion wrappers. **Sandwich** `partitionFunction_high_temp_expansion_h_zero_sandwich` and `freeEnergy_high_temp_h_zero_sandwich`: combined lower+upper bounds. Λ-layer + along-exhaustion wrappers `partitionFunction{Λ,AlongExhaustion}_high_temp_expansion_h_zero_sandwich`, `freeEnergy{Λ,AlongExhaustion}_high_temp_h_zero_sandwich`. ℤ^d wrappers `partitionFunctionΛ_latticeGraph_*`, `freeEnergyΛ_latticeGraph_*`. **Lower bound** `partitionFunction_high_temp_expansion_h_zero_lower_bound`: under `0 ≤ βJ`, `Z(J,0,β) ≥ 2^{\|ι\|} · (cosh βJ)^{\|E\|}` (empty-X term ≥ 1 in (3.45)). Λ-layer + ℤ^d wrappers `partitionFunctionΛ_high_temp_expansion_h_zero_lower_bound`, `partitionFunctionΛ_latticeGraph_high_temp_expansion_h_zero_lower_bound`. Core inequality `one_le_sum_pow_tanh_even_subgraph`: under `0 ≤ βJ`, `∑_{X even} tanh(βJ)^{\|X\|} ≥ 1`. Λ-layer + ℤ^d wrappers `one_le_sum_pow_tanh_even_subgraph_Λ`, `one_le_sum_pow_tanh_even_subgraph_latticeGraph`. Along-exhaustion + ℤ^d wrappers `one_le_sum_pow_tanh_even_subgraph_alongExhaustion{,_latticeGraph}`. **Upper bound** `sum_pow_tanh_even_subgraph_le_two_pow`: under `0 ≤ βJ`, `∑_{X even} tanh^{\|X\|} ≤ 2^{\|E\|}` (each term `≤ 1`, count `≤ 2^{\|E\|}`). **Free-energy decomposition** `freeEnergy_high_temp_expansion_h_zero_closed`: under `0 < \|ι\|` and `0 ≤ βJ`, `f = log 2 + (\|E\|/\|ι\|) log cosh(βJ) + log(∑_{X even} tanh^{\|X\|}) / \|ι\|`. Λ-layer + ℤ^d + along-exhaustion wrappers. **Free-energy upper bound** `freeEnergy_high_temp_h_zero_upper_bound`: under `0 < \|ι\|` and `0 ≤ βJ`, `f ≤ log 2 + (\|E\|/\|ι\|) · log(2·cosh(βJ))`. Pair to Step 288 lower bound. Λ-layer + ℤ^d + along-exhaustion wrappers. **Free-energy lower bound** `freeEnergy_high_temp_h_zero_lower_bound`: graph-aware `f(J,0,β) ≥ log 2 + (\|E\|/\|ι\|) · log(cosh βJ)` (Step 286 ÷ \|ι\|). Λ-layer + ℤ^d wrappers `freeEnergyΛ_high_temp_h_zero_lower_bound`, `freeEnergyΛ_latticeGraph_high_temp_h_zero_lower_bound`. Along-exhaustion wrappers `partitionFunctionAlongExhaustion_high_temp_expansion_h_zero_lower_bound`, `freeEnergyAlongExhaustion_high_temp_h_zero_lower_bound` (`AmbientLattice/SpecialCases.lean`) and ℤ^d versions in `Concrete/LatticeGraphCorrelation.lean`. **Z₂ symmetry from FV (3.46)**: `sum_high_temp_numerator_h_zero_odd_card_eq_zero` — for odd `\|A\|`, the FV (3.46) numerator vanishes via the handshake-based filter-empty result (Step 297) — independent of `correlation_odd_vanish`. Λ-layer + ℤ^d wrappers `sum_high_temp_numerator_h_zero_odd_card_eq_zero_Λ`, `sum_high_temp_numerator_h_zero_odd_card_eq_zero_latticeGraph`. **Direct handshake-based filter-empty**: `high_temp_numerator_filter_eq_empty_of_odd_card` — the FV (3.46) numerator filter is *literally empty* for odd `\|A\|`, via the edge-vertex handshake `∑_v deg_X v = 2\|X\|` plus `Finset.even_sum_iff_even_card_odd`. Independent of the spin-flip argument. Direct corollary `correlation_high_temp_h_zero_odd_card_eq_zero`: combinatorial proof of Z₂ symmetry from the closed form alone (no `correlation_odd_vanish`). Λ-layer + ℤ^d wrappers `high_temp_numerator_filter_eq_empty_of_odd_card_{Λ,latticeGraph}`, `correlationΛ_{,latticeGraph_}high_temp_h_zero_odd_card_eq_zero`. Along-exhaustion + ℤ^d wrappers `correlationAlongExhaustion_{,latticeGraph_}high_temp_h_zero_odd_card_eq_zero`, `high_temp_numerator_filter_eq_empty_of_odd_card_alongExhaustion{,_latticeGraph}`. **Correlation nonnegativity from FV (3.46)**: `correlation_high_temp_h_zero_nonneg` — alternate derivation of GKS-I at `h = 0` from the closed form (numerator/denominator both ≥ 0 when `tanh(βJ) ≥ 0`). Λ-layer + ℤ^d wrappers `correlationΛ_high_temp_h_zero_nonneg`, `correlationΛ_latticeGraph_high_temp_h_zero_nonneg`. Along-exhaustion + ℤ^d wrappers `correlationAlongExhaustion_{,latticeGraph_}high_temp_h_zero_nonneg`. **A = ∅ consistency check** `correlation_high_temp_h_zero_at_empty_A`: at `A = ∅` the FV (3.46) closed form correctly reduces to `1`, matching `correlation_empty`. Requires `0 ≤ β·J` for denominator positivity. Λ-layer + ℤ^d wrappers `correlationΛ_{,latticeGraph_}high_temp_h_zero_at_empty_A`. Along-exhaustion + ℤ^d wrappers `correlationAlongExhaustion_{,latticeGraph_}high_temp_h_zero_at_empty_A`. **Correlation closed form** `correlation_high_temp_expansion_h_zero_closed`: `⟨σ_A⟩_{β,0} = (∑_{X : ∂X=A} tanh^{\|X\|}) / (∑_{X : ∂X=∅} tanh^{\|X\|})` (FV §3.7.3 eq. (3.46)). Λ-layer + ℤ^d wrappers in `AmbientLattice/Defs.lean` and `Concrete/LatticeGraphCorrelation.lean`. Along-exhaustion + ℤ^d wrappers `correlationAlongExhaustion_{,latticeGraph_}high_temp_expansion_h_zero_closed`. **Pair+singleton bundle** `correlation_high_temp_h_zero_at_pair_singleton_bundle`: under `0 ≤ β·J`, packages `⟨σ_i⟩ = 0`, `0 ≤ ⟨σ_iσ_j⟩`, `⟨σ_iσ_j⟩ ≤ 1` into a single triple. Full 5-layer wrap with Λ / along-ex / ℤ^d / ℤ^d-along-ex companions. **Ferromagnetic bundle** `correlation_high_temp_h_zero_at_pair_singleton_bundle_ferromagnetic`: under `0 ≤ J, 0 < β`, the same triple from `mul_nonneg hβ.le hJ`. Full 5-layer wrap with Λ / along-ex / ℤ^d / ℤ^d-along-ex companions in the same PR. **Trivial-slices full bundle** `correlation_high_temp_h_zero_at_pair_singleton_trivial_slices_bundle` (and pair-only / singleton-only variants): packages the four `J=0` and `β=0` consistency vanishings (singleton at J=0, singleton at β=0, pair at J=0, pair at β=0) into one statement. Full 5-layer wrap. **Complete-summary bundle** `correlation_high_temp_h_zero_at_pair_singleton_complete_summary`: under `0 ≤ β·J`, single statement bundling pair upper bound, pair sandwich lower, singleton vanishing, and pair vanishing at `J=0` / `β=0` trivial slices. Useful as a single import for downstream applications. Full 5-layer wrap. **Z complete-summary bundle** `partitionFunction_high_temp_expansion_h_zero_complete_summary`: under `0 ≤ β·J`, single statement bundling Z lower bound, upper bound, and trivial-slice values `Z⟨0,0,β⟩ = Z⟨J,0,0⟩ = 2^|ι|`. Λ / along-ex / ℤ^d Λ / ℤ^d along-ex companions in same PR. **freeEnergy complete-summary bundle** `freeEnergy_high_temp_h_zero_complete_summary`: under `0 < |ι|` and `0 ≤ β·J`, single statement bundling free-energy lower bound, upper bound, and trivial-slice values `f⟨0,0,β⟩ = f⟨J,0,0⟩ = log 2`. Λ / along-ex / ℤ^d Λ / ℤ^d along-ex companions in same PR. **Single-edge tanh lower bound** `correlation_high_temp_h_zero_at_pair_ge_tanh_div_two_pow_edges`: under `0 ≤ β·J` and an edge `s(i, j) ∈ G.edgeSet`, `⟨σ_iσ_j⟩^{⟨J,0,β⟩} ≥ tanh(β·J) / 2^|E|`. The single edge `e = s(i,j)` contributes `tanh(β·J)` to the FV (3.46) numerator (key lemma `singleton_edge_mem_high_temp_pair_filter`); denominator ≤ `2^|E|`. First quantitative non-trivial lower bound on the pair correlation between adjacent sites. Λ / along-ex / ℤ^d Λ / ℤ^d along-ex companions wrap the bound to the corresponding subtype. **Strict positivity under edge** `correlation_high_temp_h_zero_at_pair_pos_of_edge`: under `0 < β·J` and an edge `s(i, j) ∈ G.edgeSet`, `0 < ⟨σ_iσ_j⟩`. Direct from the lower bound + `Real.tanh_pos`. Strengthens GKS-I in this specific setting. Full 5-layer wrap. **Ferromagnetic single-edge bounds** `correlation_high_temp_h_zero_at_pair_ge_tanh_div_two_pow_edges_ferromagnetic` (under `0 ≤ J, 0 < β`) and `_pair_pos_of_edge_ferromagnetic` (under `0 < J, 0 < β`): bridge the `Ferromagnetic`-style hypotheses with the abstract bounds via `mul_nonneg` / `mul_pos`. Full 5-layer wrap. **ℤ^d lattice-adjacency variants** `correlationΛ_latticeGraph_high_temp_h_zero_at_pair_ge_tanh_div_two_pow_edges_of_latticeAdj` and `_pair_pos_of_latticeAdj` (Λ + along-ex): take ambient `(latticeGraph d).Adj ↑i ↑j` directly, deriving `i ≠ j` from `Adj.ne` and `s(i, j) ∈ edgeSet` via `SimpleGraph.induce_adj`. **highTempParam API** `highTempParam_nonneg` (under `0 ≤ β·J`), `highTempParam_pos` (under `0 < β·J`), `@[simp] highTempParam_at_beta_zero`, `@[simp] highTempParam_at_J_zero`, plus the `highTempParam`-form pair lower bound `correlation_high_temp_h_zero_at_pair_ge_highTempParam_div_two_pow_edges`. **Sharper sum bound** `sum_pow_tanh_even_subgraph_le_one_plus_tanh_pow`: under `0 ≤ β·J`, `∑_{X even} tanh^|X| ≤ (1+tanh(β·J))^|E|`, tightening the `≤ 2^|E|` bound. Proof: `Finset.prod_one_add` + filter ⊆ powerset + nonneg terms. **Sharper Z upper bound** `partitionFunction_high_temp_expansion_h_zero_upper_bound_exp`: under `0 ≤ β·J`, `Z(J,0,β) ≤ 2^|ι| · exp(β·J·|E|)`. Globally tighter than `Z ≤ 2^(|ι|+|E|)·cosh^|E|`. Uses Step 392 + `Real.cosh_add_sinh` to collapse `cosh × (1+tanh) = exp`. **Sharper f upper bound** `freeEnergy_high_temp_h_zero_upper_bound_exp`: under `0 < |ι|` and `0 ≤ β·J`, `f(J,0,β) ≤ log 2 + β·J·|E|/|ι|`. Direct corollary of Step 393 by taking logs. Globally tighter than the cosh-based bound. Λ / along-ex / ℤ^d Λ / ℤ^d along-ex companions for both Z and f sharper upper bounds. **Uniform sharper f bound under BoundedEdgeDensity** `freeEnergyAlongExhaustion_high_temp_h_zero_upper_bound_exp_uniform`: under `0 ≤ β·J` + edge density `|E_n| ≤ c·|Λ_n|`, at every nonempty stage `n`, `f_n(⟨J, 0, β⟩) ≤ log 2 + β·J·c`. **∞-vol sharper f upper bound** `freeEnergyInfinite_high_temp_h_zero_upper_bound_exp_uniform`: under ferromagnetic `0 ≤ J, 0 < β` + edge density witness `c`, `freeEnergyInfinite G Λ ⟨J, 0, β⟩ ≤ log 2 + β·J·c`. **ℤ^d concrete** `freeEnergyInfinite_latticeGraph_cubicExhaustion_high_temp_h_zero_upper_bound_exp`: on the cubic exhaustion with `c = d` (via `inducedLatticeGraph_card_edgeFinset_le`), `freeEnergyInfinite ⟨J, 0, β⟩ ≤ log 2 + β·J·d`. **∞-vol sharper f sandwich** `freeEnergyInfinite_high_temp_h_zero_sandwich_exp_uniform`: under ferromagnetic + edge density witness `c`, `log 2 ≤ freeEnergyInfinite G Λ ⟨J, 0, β⟩ ≤ log 2 + β·J·c`. **ℤ^d concrete sandwich** `freeEnergyInfinite_latticeGraph_cubicExhaustion_high_temp_h_zero_sandwich_exp`: on the cubic exhaustion (`c = d`), `log 2 ≤ freeEnergyInfinite (latticeGraph d) (cubicExhaustion d) ⟨J, 0, β⟩ ≤ log 2 + β·J·d`. **∞-vol f complete-summary bundle** `freeEnergyInfinite_high_temp_h_zero_complete_summary_exp`: under ferromagnetic + edge density `c`, single statement bundling sandwich bounds (`log 2 ≤ f_∞ ≤ log 2 + β·J·c`) with trivial-slice values (`f_∞⟨0,0,β⟩ = f_∞⟨J,0,0⟩ = log 2`). **ℤ^d concrete complete-summary** `freeEnergyInfinite_latticeGraph_cubicExhaustion_high_temp_h_zero_complete_summary_exp`: with `c = d`, single ℤ^d concrete statement bundling all sandwich + trivial-slice values on the cubic exhaustion. **Sharper log Z bound + sandwich** `log_partitionFunction_high_temp_expansion_h_zero_upper_bound_exp` (`log Z ≤ |ι|·log 2 + β·J·|E|`) and `..._sandwich_exp` (`|ι|·log 2 + |E|·log cosh(β·J) ≤ log Z ≤ |ι|·log 2 + β·J·|E|`). Λ / along-ex / ℤ^d Λ / ℤ^d along-ex companions for both. **Ferromagnetic Z/logZ/f sharper upper bounds** `partitionFunction_high_temp_expansion_h_zero_upper_bound_exp_ferromagnetic` / `log_partitionFunction_..._upper_bound_exp_ferromagnetic` / `freeEnergy_high_temp_h_zero_upper_bound_exp_ferromagnetic`: under `0 ≤ J, 0 < β`, the same exp bounds via `mul_nonneg hβ.le hJ`. Λ / along-ex / ℤ^d Λ / ℤ^d along-ex companions for all three quantities. **Sharper Z/f sandwiches** `partitionFunction_high_temp_expansion_h_zero_sandwich_exp` (`2^|ι|·cosh^|E| ≤ Z ≤ 2^|ι|·exp(β·J·|E|)`) and `freeEnergy_high_temp_h_zero_sandwich_exp` (`log 2 + (|E|/|ι|)·log cosh(β·J) ≤ f ≤ log 2 + β·J·|E|/|ι|`): combine the existing lower bounds with the new sharper exp upper bounds. Λ / along-ex / ℤ^d Λ / ℤ^d along-ex companions for both. **Ferromagnetic Z/f sharper sandwiches** `partitionFunction_high_temp_expansion_h_zero_sandwich_exp_ferromagnetic` and `freeEnergy_high_temp_h_zero_sandwich_exp_ferromagnetic`: under `0 ≤ J, 0 < β`, the same sandwiches via `mul_nonneg hβ.le hJ`. Λ / along-ex / ℤ^d Λ / ℤ^d along-ex companions for both. **Sharper f complete-summary bundle** `freeEnergy_high_temp_h_zero_complete_summary_exp`: under `0 < |ι|`, `0 ≤ β·J`, single statement bundling sharper sandwich + trivial-slice values `f⟨0,0,β⟩ = f⟨J,0,0⟩ = log 2`. **Sharper Z complete-summary bundle** `partitionFunction_high_temp_expansion_h_zero_complete_summary_exp`: under `0 ≤ β·J`, single statement bundling sharper sandwich + trivial-slice values `Z⟨0,0,β⟩ = Z⟨J,0,0⟩ = 2^|ι|`. **Sharper log Z complete-summary bundle** `log_partitionFunction_high_temp_expansion_h_zero_complete_summary_exp`: under `0 ≤ β·J`, single statement bundling sharper sandwich + trivial-slice values `log Z⟨0,0,β⟩ = log Z⟨J,0,0⟩ = |ι|·log 2`. **Sharper f complete-summary exp wraps** `freeEnergyΛ_high_temp_h_zero_complete_summary_exp` + along-ex + ℤ^d Λ + ℤ^d along-ex companions. **Sharper Z + log Z complete-summary exp wraps** `partitionFunctionΛ_high_temp_expansion_h_zero_complete_summary_exp`, `log_partitionFunctionΛ_high_temp_expansion_h_zero_complete_summary_exp` plus along-ex / ℤ^d / ℤ^d along-ex companions. **Ferromagnetic complete-summary exp bundles** `partitionFunction_..._complete_summary_exp_ferromagnetic`, `log_partitionFunction_..._complete_summary_exp_ferromagnetic`, `freeEnergy_..._complete_summary_exp_ferromagnetic`: under `0 ≤ J, 0 < β`. Λ / along-ex / ℤ^d Λ / ℤ^d along-ex companions for all three. **∞-vol f deviation bound** `freeEnergyInfinite_high_temp_h_zero_deviation_bound_exp`: under ferromagnetic + edge density `c`, `freeEnergyInfinite G Λ ⟨J, 0, β⟩ - log 2 ≤ β·J·c`. Quantitative high-temperature deviation estimate. ℤ^d concrete `freeEnergyInfinite_latticeGraph_cubicExhaustion_high_temp_h_zero_deviation_bound_exp` with `c = d`. **Finite-volume f deviation bounds** `freeEnergy_..._deviation_bound_exp` (abstract) + Λ / along-ex / ℤ^d Λ / ℤ^d along-ex companions: under `0 ≤ β·J`, `f - log 2 ≤ β·J·|E|/|ι|`. **Ferromagnetic f deviation bounds** `freeEnergy_..._deviation_bound_exp_ferromagnetic`: under `0 ≤ J, 0 < β`, the same bound. Full 5-layer wrap. **f quantitative continuity at J=0** `freeEnergy_high_temp_h_zero_continuity_at_J_zero`: under `0 ≤ β·J` and `0 < |ι|`, `|f(J,0,β) - f(0,0,β)| ≤ β·J·|E|/|ι|`. Right-continuity at J=0 with explicit linear modulus. **∞-vol** `freeEnergyInfinite_high_temp_h_zero_continuity_at_J_zero`: under ferromagnetic + edge density `c`, `|freeEnergyInfinite G Λ ⟨J, 0, β⟩ - freeEnergyInfinite G Λ ⟨0, 0, β⟩| ≤ β·J·c`. **ℤ^d concrete** `freeEnergyInfinite_latticeGraph_cubicExhaustion_high_temp_h_zero_continuity_at_J_zero` with `c = d`. **f continuity at β=0** `freeEnergy_high_temp_h_zero_continuity_at_beta_zero`: under `0 ≤ β·J` and `0 < |ι|`, `|f(J,0,β) - f(J,0,0)| ≤ β·J·|E|/|ι|`. **∞-vol** `freeEnergyInfinite_high_temp_h_zero_continuity_at_beta_zero`: under ferromagnetic + edge density `c`, same bound at the ∞-volume level. **ℤ^d concrete** `freeEnergyInfinite_latticeGraph_cubicExhaustion_high_temp_h_zero_continuity_at_beta_zero` with `c = d`. **f continuity bundles** `freeEnergy_high_temp_h_zero_continuity_bundle` and `freeEnergyInfinite_high_temp_h_zero_continuity_bundle`: bundle both J=0 and β=0 continuity into single statements. **Ferromagnetic f continuity** `freeEnergy_high_temp_h_zero_continuity_at_J_zero_ferromagnetic`, `_continuity_at_beta_zero_ferromagnetic`, `_continuity_bundle_ferromagnetic`: under `0 ≤ J, 0 < β`, the same bounds. **ℤ^d ∞-vol concrete continuity bundle** `freeEnergyInfinite_latticeGraph_cubicExhaustion_high_temp_h_zero_continuity_bundle`: bundles J=0 and β=0 continuity at ℤ^d cubic ∞-volume. **f continuity Λ/along-ex/ℤ^d wraps**: `freeEnergyΛ_high_temp_h_zero_continuity_at_J_zero` / `_at_beta_zero` / `_bundle` plus along-ex / ℤ^d Λ / ℤ^d along-ex companions. **Ferromagnetic continuity bundle wraps** `_continuity_bundle_ferromagnetic` at all 4 layers. **f deviation sandwich** `freeEnergy_high_temp_h_zero_deviation_sandwich`: under `0 ≤ β·J` and `0 < |ι|`, `0 ≤ f - log 2 ≤ β·J·|E|/|ι|`. **∞-vol** `freeEnergyInfinite_high_temp_h_zero_deviation_sandwich_exp`: under ferromagnetic + edge density `c`, `0 ≤ f_∞ - log 2 ≤ β·J·c`. **ℤ^d concrete** `freeEnergyInfinite_latticeGraph_cubicExhaustion_high_temp_h_zero_deviation_sandwich_exp` with `c = d`. **f deviation sandwich Λ/along-ex/ℤ^d wraps**: `freeEnergyΛ_..._deviation_sandwich` + along-ex + ℤ^d Λ + ℤ^d along-ex companions. **Ferromagnetic f deviation sandwich** `_deviation_sandwich_ferromagnetic` at all 5 layers (under `0 ≤ J, 0 < β`). **log Z deviation sandwich** `log_partitionFunction_high_temp_expansion_h_zero_deviation_sandwich`: under `0 ≤ β·J`, `0 ≤ log Z - |ι|·log 2 ≤ β·J·|E|`. Λ / along-ex / ℤ^d Λ / ℤ^d along-ex companions. **Ferromagnetic log Z deviation sandwich** `_deviation_sandwich_ferromagnetic` at all 5 layers (under `0 ≤ J, 0 < β`). **Z relative-deviation sandwich** `partitionFunction_high_temp_expansion_h_zero_relative_sandwich`: under `0 ≤ β·J`, `cosh(β·J)^|E| ≤ Z / 2^|ι| ≤ exp(β·J·|E|)`. Normalized form. Λ / along-ex / ℤ^d Λ / ℤ^d along-ex companions. **Ferromagnetic Z relative-deviation sandwich** `_relative_sandwich_ferromagnetic` at all 5 layers (under `0 ≤ J, 0 < β`). **f strict deviation** `freeEnergy_high_temp_h_zero_deviation_pos`: under `0 < β·J`, `0 < |ι|`, `0 < |E|`, `0 < f - log 2`. **Ferromagnetic** `freeEnergy_high_temp_h_zero_deviation_pos_ferromagnetic`: under `0 < J, 0 < β`, the same. **f strict deviation Λ/along-ex/ℤ^d wraps** `freeEnergyΛ_..._deviation_pos` etc. **Ferromagnetic f strict deviation** wraps `_deviation_pos_ferromagnetic` at all 5 layers. **log Z strict deviation** `log_partitionFunction_high_temp_expansion_h_zero_deviation_pos`: under `0 < β·J` and `0 < |E|`, `0 < log Z - |ι|·log 2`. **Z strict deviation** `partitionFunction_high_temp_expansion_h_zero_pow_two_lt`: under `0 < β·J` and `0 < |E|`, `2^|ι| < Z`. **Ferromagnetic strict deviations** `_pow_two_lt_ferromagnetic` and `log_..._deviation_pos_ferromagnetic`: under `0 < J, 0 < β`, the same. **Z + log Z strict deviation Λ/along-ex/ℤ^d wraps**: `partitionFunctionΛ_..._pow_two_lt`, `log_partitionFunctionΛ_..._deviation_pos` plus along-ex / ℤ^d Λ / ℤ^d along-ex companions. **Ferromagnetic Z + log Z strict deviation Λ/along-ex/ℤ^d wraps** `_pow_two_lt_ferromagnetic` and `_deviation_pos_ferromagnetic` at all 4 layers. **Z ratio bounds** `partitionFunction_high_temp_expansion_h_zero_ratio_bound` (J=0 trivial slice) and `_ratio_bound_beta_zero`: under `0 ≤ β·J`, both ratios `Z⟨J,0,β⟩ / Z⟨0,0,β⟩` and `Z⟨J,0,β⟩ / Z⟨J,0,0⟩ ≤ exp(β·J·|E|)`. **Z ratio sandwiches** `partitionFunction_high_temp_expansion_h_zero_ratio_sandwich` (J=0) and `_ratio_sandwich_beta_zero`: `cosh(β·J)^|E| ≤ Z⟨J,0,β⟩/Z⟨trivial,0,β⟩ ≤ exp(β·J·|E|)`. **Z ratio sandwich bundle** `_ratio_sandwich_bundle`: bundles both J=0 and β=0 slices. **Ferromagnetic Z ratio sandwiches** `_ratio_sandwich_ferromagnetic`, `_ratio_sandwich_beta_zero_ferromagnetic`, `_ratio_sandwich_bundle_ferromagnetic`. **Z ratio sandwich Λ/along-ex/ℤ^d Λ wraps** `partitionFunctionΛ_high_temp_expansion_h_zero_ratio_sandwich` and along-ex / ℤ^d companions (J=0 slice). **Z ratio sandwich at β=0 wraps** `_ratio_sandwich_beta_zero` Λ / along-ex / ℤ^d Λ companions. **Λ-level Z ratio sandwich bundle** `partitionFunctionΛ_high_temp_expansion_h_zero_ratio_sandwich_bundle`. **along-ex / ℤ^d Λ / ℤ^d along-ex** Z ratio sandwich bundle wraps. **Ferromagnetic Z ratio sandwich bundle** Λ + along-ex + ℤ^d Λ + ℤ^d along-ex wraps `_ratio_sandwich_bundle_ferromagnetic`. **Λ-level Z ratio bound** `partitionFunctionΛ_high_temp_expansion_h_zero_ratio_bound` and `_ratio_bound_beta_zero` (upper-only forms). **along-ex / ℤ^d Λ / ℤ^d along-ex** Z ratio upper bound wraps. **Ferromagnetic Z ratio upper bounds** `_ratio_bound_ferromagnetic` and `_ratio_bound_beta_zero_ferromagnetic` at all 5 layers (abstract / Λ / along-ex / ℤ^d Λ / ℤ^d along-ex). **Z ratio upper bound bundle** `_ratio_bound_bundle`: bundles J=0 and β=0 ratio upper bounds. **Λ-level Z ratio upper bound bundle** wrap. **along-ex / ℤ^d Λ / ℤ^d along-ex Z ratio bound bundle** wraps. **Ferromagnetic Z ratio upper bound bundle** at all 5 layers `_ratio_bound_bundle_ferromagnetic`. **f ratio bounds** `freeEnergy_high_temp_h_zero_ratio_bound` (J=0) and `_beta_zero`: `f⟨J,0,β⟩ - f⟨trivial,0,β⟩ ≤ β·J·|E|/|ι|`. **f ratio bound bundle** `_ratio_bound_bundle`: bundles both J=0 and β=0 ratio bounds. **Ferromagnetic f ratio bounds** `freeEnergy_high_temp_h_zero_ratio_bound_ferromagnetic`, `_beta_zero_ferromagnetic`, `_bundle_ferromagnetic`. **Λ-level f ratio bound** `freeEnergyΛ_high_temp_h_zero_ratio_bound`, `_beta_zero`, `_bundle`. **f ratio bound bundle along-ex/ℤ^d Λ/ℤ^d along-ex** wraps. **Ferromagnetic f ratio bound bundle** at all 5 layers. **∞-vol f ratio bounds** `freeEnergyInfinite_high_temp_h_zero_ratio_bound`, `_beta_zero`, `_bundle`: under ferromagnetic + edge density `c`, `f_∞⟨J,0,β⟩ - f_∞⟨trivial,0,β⟩ ≤ β·J·c`. **ℤ^d concrete ∞-vol f ratio bound bundle on cubicExhaustion** with `c = d`. **along-ex f deviation bound** `_deviation_bound_exp_of_nonempty` accepts `(Λ.volume n).Nonempty` directly. **along-ex strict deviation API** `_deviation_pos_of_nonempty` for f and `_pow_two_lt_of_nonempty` for Z. **ℤ^d along-ex deviation under nonempty wraps** for f. **along-ex / ℤ^d Λ f ratio bound (J=0/β=0 individually)** wraps. **ℤ^d along-ex f ratio bound** individually at J=0/β=0. **Λ-level ferromagnetic f ratio bound** individual J=0/β=0. **Along-ex / ℤ^d Λ / ℤ^d along-ex ferromagnetic individual** f ratio bounds J=0/β=0. **Z + log Z + f strict deviation bundle** `partitionFunction_high_temp_expansion_h_zero_strict_deviation_bundle`: under `0 < β·J`, `0 < |E|`, `0 < |ι|`, single statement bundling `2^|ι| < Z`, `0 < log Z - |ι|·log 2`, `0 < f - log 2`. **Λ / along-ex / ℤ^d Λ / ℤ^d along-ex** strict deviation bundle wraps and ferromagnetic variants at all 5 layers. **log Z ratio bounds** `log_partitionFunction_high_temp_expansion_h_zero_ratio_bound` (J=0) and `_beta_zero`: under `0 ≤ β·J`, `log Z⟨J,0,β⟩ - log Z⟨trivial,0,β⟩ ≤ β·J·|E|`. **log Z ratio bound bundle** + ferromagnetic variants. **Λ / along-ex / ℤ^d Λ / ℤ^d along-ex** log Z ratio bound bundle wraps + ferromagnetic. **log Z ratio sandwich** `log_partitionFunction_high_temp_expansion_h_zero_ratio_sandwich` (J=0) and `_beta_zero`: under `0 ≤ β·J`, `|E|·log cosh(β·J) ≤ log Z⟨J,0,β⟩ - log Z⟨trivial,0,β⟩ ≤ β·J·|E|`. **log Z ratio sandwich bundle** + ferromagnetic. **Λ / along-ex / ℤ^d Λ / ℤ^d along-ex** log Z ratio sandwich bundle wraps + ferromagnetic. **f ratio sandwich** `freeEnergy_high_temp_h_zero_ratio_sandwich` (J=0) and `_beta_zero`: under `0 ≤ β·J` and `0 < |ι|`, `(|E|/|ι|)·log cosh(β·J) ≤ f⟨J,0,β⟩ - f⟨trivial,0,β⟩ ≤ β·J·|E|/|ι|`. **f ratio sandwich bundle** + ferromagnetic. **Λ / along-ex / ℤ^d Λ / ℤ^d along-ex** f ratio sandwich bundle wraps + ferromagnetic. **Triple (Z + log Z + f) ratio bound bundle** `partitionFunction_high_temp_expansion_h_zero_triple_ratio_bound_bundle` (J=0) and `_beta_zero`: under `0 ≤ β·J` and `0 < |ι|`, single statement bundling all three quantities' ratio bounds + ferromagnetic variants. **Λ / along-ex / ℤ^d Λ / ℤ^d along-ex** triple ratio bound bundle wraps + ferromagnetic. **Triple (Z + log Z + f) ratio sandwich bundle** `partitionFunction_high_temp_expansion_h_zero_triple_ratio_sandwich_bundle` (J=0) and `_beta_zero`: under `0 ≤ β·J` and `0 < |ι|`, single statement bundling all three quantities' ratio sandwiches + ferromagnetic. **Λ / along-ex / ℤ^d Λ / ℤ^d along-ex** triple ratio sandwich bundle wraps + ferromagnetic. **Triple ratio sandwich bundle β=0** at abstract / Λ / along-ex / ℤ^d Λ / ℤ^d along-ex layers, plus ferromagnetic at all 5 layers. (PRs #1118–#1343.) | | §18.4 | Cluster expansion machinery (lattice version) | **Done (foundations + main bijection + Z identity)** | `IsEvenSubgraph`, `IsPolymer`, `polymerSupport`, `IsPolymerVertexDisjoint`, `IsCompatiblePolymerFamilyVertexDisjoint`, `edgeComponent`, `polymerDecomposition` (`ClusterExpansion.lean`); the bijection `evenSubgraphs G ↔ vdCompatiblePolymerFamilies G` is established in both directions. Capstone `partitionFunction_high_temp_expansion_h_zero_polymer_family`: `Z(J,0,β) = 2^|ι|·cosh(β·J)^|E|·∑_{Γ ∈ vdCompatiblePolymerFamilies G} ∏_{P ∈ Γ} tanh(β·J)^|P|`. **Mayer expansion foundation** (Step 576): `PolymersIncompatible P Q := ¬ Disjoint (polymerSupport P) (polymerSupport Q)` with `Decidable` instance, `symm`, `iff_not_isPolymerVertexDisjoint`, `iff_exists_shared_vertex`, and `self_of_isPolymer` (a non-empty polymer is incompatible with itself, reflecting the multi-set convention for clusters). **Incompatibility graph** (Step 577): `incompatibilityGraph : SimpleGraph (Finset (Sym2 ι))` defined via `SimpleGraph.fromRel PolymersIncompatible`, with `incompatibilityGraph_adj` characterising adjacency as `P ≠ Q ∧ PolymersIncompatible P Q` (the disjunction in `fromRel` collapses by symmetry of `PolymersIncompatible`) and `DecidableRel` instance. **Cluster polymer set** (Step 578): `IsClusterPolymerSet G Γ := Γ.Nonempty ∧ (∀ P ∈ Γ, IsPolymer G P) ∧ ((incompatibilityGraph).induce ↑Γ).Connected` — the set-level notion of cluster (no multiplicity yet). `IsClusterPolymerSet.singleton`: any singleton `{P}` of a polymer is a cluster set (vacuous Preconnected on a single vertex). **Polymer-sequence incompatibility graph** (Step 579): `polymerSeqIncompatibilityGraph (ω : α → Finset (Sym2 ι)) : SimpleGraph α` parameterised by an arbitrary index type `α`, with adjacency `i ~ j ↔ i ≠ j ∧ PolymersIncompatible (ω i) (ω j)` and `DecidableRel` instance. The identity-indexed sequence on the polymer space recovers Step 577 (`polymerSeqIncompatibilityGraph_id`). **Cluster polymer sequence** (Step 580): `IsClusterPolymerSequence G hn ω` for `ω : Fin n → polymers` with `n ≥ 1` — every entry is a polymer of `G` and the index-side incompatibility graph on `Fin n` is `Connected`. Sequence-level analogue of `IsClusterPolymerSet` allowing multiplicities (the same polymer may appear at multiple indices), as required by the Mayer-expansion sum. `IsClusterPolymerSequence.singleton`: any one-element sequence whose entry is a polymer is a cluster sequence. **Cluster-sequence activity** (Step 581): `clusterSeqActivity t ω := ∏ i, t ^ (ω i).card` — the activity factor multiplying the Ursell coefficient in the Mayer expansion `log Ξ = ∑_n (1/n!) ∑_ω ϕ^T(ω) · z(ω)`. API: singleton (`n=1`), non-negativity for `0 ≤ t`, empty sequence (`n=0`) equals `1`. **Connected spanning edge subsets** (Step 582): `connectedSpanningEdgeSubsets G : Finset (Finset (Sym2 V))` for finite-vertex `G` — edge subsets `S ⊆ G.edgeFinset` such that the spanning subgraph `SimpleGraph.fromEdgeSet ↑S` (with the same vertex set `V`) is `Connected`. API: `mem_connectedSpanningEdgeSubsets` (membership characterisation). **Ursell coefficient** (Step 583): `ursellCoefficient (ω : Fin n → polymers) : ℝ := (∑_{S ∈ connectedSpanningEdgeSubsets G(ω)} (-1)^{\|S\|}) / n!` — the combinatorial weight in the Mayer expansion `log Ξ = ∑_{n ≥ 1} ∑_ω ϕ^T(ω) · z(ω)`. Singleton case `ursellCoefficient_singleton`: `ϕ^T(ω) = 1` for `n = 1` (graph on `Fin 1` has no edges, only edge subset is `∅`, spanning is connected). **Vanishing for disconnected sequences** (Step 584): `ursellCoefficient_eq_zero_of_disconnected`: `ϕ^T(ω) = 0` whenever `G(ω)` is not `Connected`. The Mayer-expansion sum effectively restricts to cluster sequences (Step 580). Proof: any connected spanning subgraph `fromEdgeSet ↑S` of `G(ω)` implies `G(ω)` itself is `Connected` (via `Reachable.mono`), so disconnected `G(ω)` forces `connectedSpanningEdgeSubsets = ∅`. **Pair Ursell coefficient (incompatible)** (Step 585): `ursellCoefficient_pair_incompatible`: for `ω : Fin 2 → polymers` with `PolymersIncompatible (ω 0) (ω 1)`, `ϕ^T(ω) = -1/2`. **Pair Ursell coefficient (compatible)** (Step 586): `ursellCoefficient_pair_compatible`: for compatible pairs, `ϕ^T(ω) = 0` (Step 584 applies — Fin 2 graph with no edge is disconnected). **Unified** `ursellCoefficient_pair`: case-conditional formula `ϕ^T(ω) = if PolymersIncompatible (ω 0) (ω 1) then -1/2 else 0`. **Mayer expansion n-th term** (Step 587): `mayerExpansionTerm G n t := ∑_{ω ∈ piFinset (allPolymers G)} ϕ^T(ω) · z(t, ω)` — the contribution of `n`-element polymer sequences to `log Ξ`; the `1/n!` factor is already absorbed into `ursellCoefficient` (Step 583). `mayerExpansionTerm_zero`: `= 0` (empty sequence's Ursell vanishes by disconnectedness). `mayerExpansionTerm_one`: `= ∑_{P ∈ allPolymers G} t^|P|` (singleton ϕ^T = 1, z = t^|P|, reindex via `ω ↦ ω 0`). **Continuity in `t`** (Step 588): `clusterSeqActivity_continuous` (finite product of monomials) and `mayerExpansionTerm_continuous` (finite sum of constants times continuous functions). **Differentiability in `t`** (Step 589): `clusterSeqActivity_differentiable` and `mayerExpansionTerm_differentiable` strengthen continuity to `Differentiable ℝ` on all of `ℝ`, since each term is a polynomial. **Real-analyticity in `t`** (Step 590): `clusterSeqActivity_analyticAt`, `mayerExpansionTerm_analyticAt`, and global `mayerExpansionTerm_analyticOnNhd` over `Set.univ`. Each Mayer term is a polynomial in `t`, hence real-analytic at every point. **Mayer partial sum** (Step 591): `mayerPartialSum G N t := ∑_{n = 0..N} mayerExpansionTerm G n t` — finite truncation through cluster size `N`. Inherits `Continuous`, `Differentiable ℝ`, `AnalyticAt ℝ` (at every `t`), and global `AnalyticOnNhd ℝ _ Set.univ`. **Base cases** (Step 592): `mayerPartialSum_zero`: `= 0` at N=0. `mayerPartialSum_one`: `= ∑_{P ∈ allPolymers G} t^|P|` at N=1 (leading non-trivial truncation = total polymer activity). **n=2 explicit pair sum** (Step 593): `mayerExpansionTerm G 2 t = ∑_{(P, Q) ∈ allPolymers²} (if PolymersIncompatible P Q then -1/2 else 0) · t^|P| · t^|Q|`. Reindex via `Finset.sum_bij` between `piFinset` and `allPolymers ×ˢ allPolymers` (sending `ω ↦ (ω 0, ω 1)`); apply pair Ursell formula. **Lift to β/J via tanh chain** (Step 594): `mayerExpansionTerm_tanh_continuous_beta` / `_J` and `mayerPartialSum_tanh_continuous_beta` / `_J` — continuous in β (resp. J) with the other fixed, by composition with `Real.tanh (β·J)`. **Differentiable lift** (Step 595): `mayerExpansionTerm_tanh_differentiable_beta` / `_J` and `mayerPartialSum_tanh_differentiable_beta` / `_J` — same chain via `differentiable_real_tanh`. **AnalyticAt + AnalyticOnNhd lift** (Step 596): `mayerExpansionTerm_tanh_analyticAt_beta` / `_J`, `mayerPartialSum_tanh_analyticAt_beta` / `_J`, plus global `mayerPartialSum_tanh_analyticOnNhd_beta` / `_J` over `Set.univ`. Chain through `analyticAt_real_tanh` and analytic linear factor `β·J`. The Mayer truncation `mayerPartialSum G N` is now a real-analytic function of β/J on all of ℝ, mirroring `freeEnergy_analyticOnNhd` from §18.6. **n=2 filter form** (Step 597): `mayerExpansionTerm_two_filter`: `mayerExpansionTerm G 2 t = -1/2 · ∑_{(P, Q) ∈ allPolymers², PolymersIncompatible P Q} t^|P| · t^|Q|` — restricted to incompatible pairs. **Vanishing at t=0** (Step 598): `mayerExpansionTerm_at_zero` and `mayerPartialSum_at_zero` (`= 0` for all n / N). For n=0 via Step 587; for n ≥ 1 since every polymer has |P| ≥ 1, so `0 ^ |P| = 0` and `clusterSeqActivity 0 ω = 0`. **vdPolymerFamilies_sum at t=0** (Step 599): `vdPolymerFamilies_sum_at_zero`: `∑_{Γ ∈ vdCompatiblePolymerFamilies G} ∏_{P ∈ Γ} 0^|P| = 1` (only empty family `Γ = ∅` contributes via empty product; non-empty families contribute 0). **Mayer identity at t=0** (Step 600 milestone): `mayer_identity_at_zero`: `Real.log (vdPolymerFamilies_sum G 0) = mayerPartialSum G N 0` for any `N` (both sides = 0). First verified instance of the Mayer expansion identity `log Ξ = ∑_{n ≥ 0} mayerExpansionTerm G n t`; the general-`t` identity requires substantial Mayer/Ursell power-series manipulations (deferred). **Ursell absolute bound** (Step 601): `|ϕ^T(ω)| ≤ |connectedSpanningEdgeSubsets G(ω)| / n!` via triangle inequality on the alternating sum (each `(-1)^|S|` has `|·| = 1`). **`connectedSpanningEdgeSubsets` cardinality** (Step 602): `|connectedSpanningEdgeSubsets G| ≤ 2^|G.edgeFinset|` (filter ⊆ powerset). **Uniform Ursell bound** (Step 603): `ursellCoefficient_abs_le_pow_div_factorial`: `|ϕ^T(ω)| ≤ 2^|E(G(ω))| / n!` — classical Mayer-expansion uniform bound combining Steps 601, 602. **Mayer term triangle bound** (Step 604): `mayerExpansionTerm_abs_le`: `|mayerExpansionTerm G n t| ≤ ∑_ω |ϕ^T(ω)| · |z(t,ω)|` via `Finset.abs_sum_le_sum_abs` + `abs_mul`. **Generic positivity** (Step 605): `vdPolymerFamilies_sum_ge_one_of_nonneg`: `1 ≤ ∑ Γ ∏ t^|P|` for any `t ≥ 0` (empty family contributes 1, others non-negative); `vdPolymerFamilies_sum_pos_of_nonneg`: `> 0`. Strengthens Step 549 from the tanh form to a generic non-negative activity. **`log` analyticity** (Step 606): `log_vdPolymerFamilies_sum_analyticAt`: `Real.log (vdPolymerFamilies_sum G t)` is `AnalyticAt ℝ` at every `t ≥ 0`, via `AnalyticAt.log` of the analytic polymer-family sum (positive). **Global form** (Step 607): `log_vdPolymerFamilies_sum_analyticOnNhd_Ici_zero`: `AnalyticOnNhd ℝ _ (Set.Ici 0)` lifting Step 606. **`log` analyticity in β / J** (Step 608): `log_vdPolymerFamilies_sum_tanh_analyticAt_beta` / `_J` under `0 ≤ β·J` — `Real.log (∑_Γ ∏ tanh(β·J)^|P|)` is `AnalyticAt ℝ` in β (resp. J). Combines Step 562 (vdSum analytic in β/J via tanh) with positivity at `tanh(β·J) ≥ 0`. **Mayer identity at β·J=0** (Step 609): `mayer_identity_at_betaJ_zero` (general), `mayer_identity_at_beta_zero` (β=0), `mayer_identity_at_J_zero` (J=0) — extend Step 600 to β/J directions via `tanh 0 = 0`. **Polymer free energy** (Step 610): `polymerFreeEnergy G t := Real.log (∑_Γ ∏ t^|P|)` — named wrapper for the LHS of the Mayer identity. `polymerFreeEnergy_at_zero = 0`, `polymerFreeEnergy_analyticAt` for `t ≥ 0`, `polymerFreeEnergy_analyticOnNhd_Ici_zero` (global form over `Set.Ici 0`). **Continuity / differentiability + restated identity** (Step 611): `polymerFreeEnergy_continuousAt` and `_differentiableAt` (consequences of analyticAt); `polymerFreeEnergy_eq_mayerPartialSum_at_zero` (Mayer identity at t=0 in named-wrapper form). **freeEnergy decomposition** (Step 612): `freeEnergy_eq_polymerFreeEnergy`: under `0 < |ι|` and `0 ≤ β·J`, `freeEnergy G ⟨J, 0, β⟩ = log 2 + (|E|/|ι|) · log cosh(β·J) + polymerFreeEnergy G (tanh(β·J)) / |ι|`. Restatement of Step 317 in polymer-family form (via Step 547 bijection), connecting the actual Ising free energy to the polymer free energy. **β/J analyticity wrappers** (Step 613): `polymerFreeEnergy_tanh_analyticAt_beta` / `_J` (named-wrapper restatement of Step 608) and `_analyticOnNhd_beta_Ici_zero` / `_J_Ici_zero` (under `J ≥ 0` / `β ≥ 0` gives global form on `[0, ∞)`). **N=2 explicit Mayer truncation** (Step 614): `mayerPartialSum_two`: `mayerPartialSum G 2 t = ∑_P t^|P| - (1/2) ∑_{(P, Q) incompat} t^|P|·t^|Q|` — leading two-term Mayer truncation in fully explicit polymer-sum form. **Uniform Ursell bound** (Step 615): `ursellCoefficient_abs_le_choose_pow_div_factorial`: `|ϕ^T(ω)| ≤ 2^(n choose 2) / n!` — independent of `ω` (combines Step 603 with `SimpleGraph.card_edgeFinset_le_card_choose_two`). **Explicit convergence radius via `log` `HasSum`** (PR #1517): `polymerFreeEnergy_hasSum_via_log_of_pow_lt_two` — under `(1+t)^|E| < 2`, `polymerFreeEnergy G t = ∑_n …` as a `HasSum` of explicit terms; named convergence radius for the polymer expansion. **Mayer Phase B base cases via `decide`** (PRs #1518, #1519, #1542-#1546, #1553): explicit alternating connected-subgraph sums `alternatingConnectedSubgraphSum_K3 = 2`, `_K4 = -6` (PRs #1518/#1519, `set_option maxRecDepth 2000`), `pathGraph` for `n = 3..8` with alternating signs `1, -1, 1, -1, 1, -1` (PRs #1542-#1544; `pathGraph 8` requires `maxRecDepth 8000` + `maxHeartbeats 1000000`), `cycleGraph` for `n = 3..7` with values `2, -3, 4, -5, 6` (PRs #1545, #1546, #1553). General `K_n` formula `(-1)^(n-1)·(n-1)!` and `n ≥ 9` cases require chromatic-polynomial / matrix-tree theorem machinery not yet in Mathlib (deferred). **Filter forms** (PRs #1521, #1522): `mayerExpansionTerm_filter_connected` and `mayerPartialSum_filter_connected` — restrict the Mayer sums to connected polymer-sequence supports without changing the value. **`polymerFreeEnergy` upper bounds** (PRs #1523, #1524, #1525): `polymerFreeEnergy_le_eps_of_nonneg`, `_le_pow_sub_one_of_nonneg`, `_lt_log_two_of_pow_lt_two`, plus tanh-substituted forms. **High-temperature sandwich** (PR #1526): `polymerFreeEnergy_high_temp_sandwich` (5-tuple) and **`freeEnergy_lt_log_two_plus_high_temp_correction`** (PR #1527). **Strict / iff characterisations** (PRs #1547-#1550, #1554-#1560): `polymerFreeEnergy_lt_eps_of_eps_pos` (strict; PR #1547), `_eq_zero_iff_eps_eq_zero` and `_pos_iff_eps_pos` (PR #1548), `_lt_eps_iff_eps_pos` (PR #1549), tanh-substituted strict / iff forms (PR #1550), `polymerFreeEnergy_lt_pow_sub_one_of_eps_pos` and tanh form (PRs #1554, #1555), `mayerExpansionTerm_eq_zero_of_no_polymers` (PR #1556), `vdPolymerFamilies_sum_eq_one_iff_eps_eq_zero` and `_gt_one_iff_eps_pos` (PR #1557), bundle of ε > 0 / = 0 iff polymers + tanh forms (10 thm; PR #1558), strict-mono bundle (4 thm; PR #1559), strict-pos bundle + `StrictMonoOn (Set.Ioi 0)` (8 thm; PR #1560). **Pair connectivity / filter** (PRs #1551, #1552): `polymerSeqIncompatibilityGraph_two_connected_iff_incompatible` and `mayerExpansionTerm_two_filter_connected_eq_incompat`. **`mayerPartialSum` strict-pos / sign / N=0** (PR #1562; 3 thm). **Λ-layer wrappers** (PRs #1563, #1564): 10 + 8 theorems in `AmbientLattice/Analyticity.lean` lifting the abstract API to the Λ layer. **Ferromagnetic forms** (PR #1565; 9 thm) — `0 ≤ J, 0 < β` versions of the strict / iff bundle via `mul_nonneg`. **tanh-monotonicity in β / J** (PR #1566; 5 thm + local helper `real_tanh_strictMono`) — `polymerFreeEnergy (tanh(β·J))` is monotone (resp. strictly monotone) in β and J under the appropriate ferromagnetic sign assumptions. (Steps 503-548, 576-615; PRs #1517-#1566; Issue #1344.) | -| §18.5 | Convergence of the cluster expansion | **Done at `h = 0` (polymer-family sum sandwich + explicit log-Taylor convergence radius at all volume layers, including the polymer-family sum sandwich at every volume layer)** | `vdPolymerFamilies_sum_sandwich` (`1 ≤ ∑_Γ ∏ tanh(β·J)^|P| ≤ 2^|E|`) and `vdPolymerFamilies_sum_sandwich_sharp` (`≤ (1+tanh(β·J))^|E|`) under `0 ≤ β·J` (`ClusterExpansion.lean`). **Λ + along-ex + ℤ^d wraps for both sandwich variants** (PR #1572): `vdPolymerFamilies_sum_Λ_sandwich(_sharp)` (`AmbientLattice/Analyticity.lean`), `vdPolymerFamilies_sumAlongExhaustion_sandwich(_sharp)` (`AmbientLattice/SpecialCases.lean`), `vdPolymerFamilies_sum_Λ_latticeGraph_sandwich(_sharp)` and `vdPolymerFamilies_sumAlongExhaustion_latticeGraph_sandwich(_sharp)` (`Concrete/LatticeGraphCorrelation.lean`). **Ferromagnetic versions of both sandwich variants at all 5 layers** (PR #1574, under `0 ≤ J, 0 < β`): abstract `vdPolymerFamilies_sum_sandwich_ferromagnetic` and `_sandwich_sharp_ferromagnetic`, plus 4 layer wraps for each. The two ℤ^d sharp variants use the abbreviated `_ferro` suffix; other ferromagnetic wrappers retain `_ferromagnetic`. **Strict `freeEnergy` upper bound in convergence regime, all 5 layers** (PR #1575): abstract `freeEnergy_lt_log_two_plus_high_temp_correction` (PR #1527) plus ferromagnetic version, lifted to Λ-direct, along-exhaustion, ℤ^d Λ-direct, and ℤ^d along-exhaustion as `freeEnergyΛ_lt_log_two_plus_high_temp_correction(_ferromagnetic)`, `freeEnergyAlongExhaustion_lt_log_two_plus_high_temp_correction(_ferromagnetic)`, and the corresponding `latticeGraph` versions (with the two ℤ^d ferromagnetic variants using the abbreviated `_ferro` suffix). **`polymerFreeEnergy` regularity at all 4 layers** (PR #1576): `polymerFreeEnergy_{Λ,AlongExhaustion}_{continuousAt,differentiableAt,continuousOn_Ici_zero,differentiableOn_Ici_zero}` (`AmbientLattice/Analyticity.lean`, `AmbientLattice/SpecialCases.lean`) plus their `latticeGraph` ℤ^d variants (`Concrete/LatticeGraphCorrelation.lean`). 16 thin per-point / per-set wrappers of the abstract `polymerFreeEnergy_continuousAt` / `_differentiableAt` (Step 611) and `_continuousOn_Ici_zero` / `_differentiableOn_Ici_zero`. **`polymerFreeEnergy` β / J real-analyticity at all 4 layers** (PR #1577): `polymerFreeEnergy_{Λ,AlongExhaustion}_tanh_{analyticAt_beta,analyticAt_J,analyticOnNhd_beta_Ici_zero,analyticOnNhd_J_Ici_zero}` plus `latticeGraph` ℤ^d variants. 16 thin wrappers of the abstract `polymerFreeEnergy_tanh_analyticAt_{beta,J}` (Step 613) and `_analyticOnNhd_{beta,J}_Ici_zero` over `Set.Ici 0`. **`polymerFreeEnergy` bound family at all 4 layers** (PR #1578): `polymerFreeEnergy_{Λ,AlongExhaustion}_{nonneg_of_nonneg,le_card_log_one_plus_of_nonneg,le_card_mul_of_nonneg,monotoneOn_Ici_zero}` plus `latticeGraph` ℤ^d variants. 16 thin wrappers of the abstract `polymerFreeEnergy_nonneg_of_nonneg`, `_le_card_log_one_plus_of_nonneg`, `_le_card_mul_of_nonneg`, and `_monotoneOn_Ici_zero` bound API. **`polymerFreeEnergy` edge-cases + comparison family at all 4 layers** (PR #1579): `polymerFreeEnergy_{Λ,AlongExhaustion}_{eq_zero_of_no_polymers,eq_zero_of_edgeFinset_empty,le_of_le_of_nonneg,le_of_le_strict_form}` plus `latticeGraph` ℤ^d variants. 16 thin wrappers covering `polymerFreeEnergy = 0` on no-polymer / edgeless induced graphs (Steps 621, 623) and order preservation on `[0, ∞)` (Steps 649, 650). **`polymerFreeEnergy` tanh-bound family at all 4 layers** (PR #1580): `polymerFreeEnergy_{Λ,AlongExhaustion}_{tanh_sandwich,le_card_log_two_of_le_one,tanh_le_card_log_two,tanh_double_bound}` plus `latticeGraph` ℤ^d variants. 16 thin wrappers covering the tanh-form sandwich (Step 632), `≤ |E| · log 2` for `0 ≤ t ≤ 1` (Step 642), the tanh form thereof (Step 643), and the combined double bound (Step 645). **`mayerPartialSum` regularity at all 4 layers** (PR #1581): `mayerPartialSum_{Λ,AlongExhaustion}_{continuous,differentiable,analyticAt,continuousOn,differentiableOn}` plus `latticeGraph` ℤ^d variants. 20 thin wrappers of `mayerPartialSum_continuous` / `_differentiable` / `_analyticAt` (Step 591) and `_continuousOn` / `_differentiableOn` (Step 628). **`mayerExpansionTerm` regularity at all 4 layers** (PR #1582): `mayerExpansionTerm_{Λ,AlongExhaustion}_{continuous,differentiable,analyticAt,analyticOnNhd}` plus `latticeGraph` ℤ^d variants. 16 thin wrappers of the four abstract regularity statements (Steps 588, 589, 590). **`mayerPartialSum` tanh β/J regularity at all 4 layers** (PR #1583): `mayerPartialSum_{Λ,AlongExhaustion}_tanh_{continuous_beta,continuous_J,differentiable_beta,differentiable_J,analyticAt_beta,analyticAt_J,analyticOnNhd_beta,analyticOnNhd_J}` plus `latticeGraph` ℤ^d variants. 32 thin wrappers of the abstract `mayerPartialSum_tanh_*_{beta,J}` (Steps 594, 595, 596). **`mayerExpansionTerm` tanh β/J regularity at all 4 layers** (PR #1584): `mayerExpansionTerm_{Λ,AlongExhaustion}_tanh_{continuous_beta,continuous_J,differentiable_beta,differentiable_J,analyticAt_beta,analyticAt_J}` plus `latticeGraph` ℤ^d variants. 24 thin wrappers of the abstract `mayerExpansionTerm_tanh_*_{beta,J}` (Steps 594, 595, 596). **`vdPolymerFamilies_sum` regularity in `t` at all 4 layers** (PR #1585): `vdPolymerFamilies_sum_{Λ,AlongExhaustion}_{continuous,differentiable,analyticAt,hasDerivAt}` plus `latticeGraph` ℤ^d variants. 16 thin wrappers of the abstract `vdPolymerFamilies_sum_continuous` (Step 555), `_differentiable` (Step 558), `_analyticAt` (Step 561), and `_hasDerivAt` with explicit polynomial derivative formula (Step 575). **`vdPolymerFamilies_sum` tanh β/J regularity at all 4 layers** (PR #1586): `vdPolymerFamilies_sum_{Λ,AlongExhaustion}_tanh_{continuous_beta,continuous_J,differentiable_beta,differentiable_J,analyticAt_beta,analyticAt_J}` plus `latticeGraph` ℤ^d variants. 24 thin wrappers of the abstract `vdPolymerFamilies_sum_tanh_*_{beta,J}` (Steps 556, 559, 562). **`log_vdPolymerFamilies_sum` analyticity at all 4 layers** (PR #1587): `log_vdPolymerFamilies_sum_{Λ,AlongExhaustion}_{analyticAt,analyticOnNhd_Ici_zero,tanh_analyticAt_beta,tanh_analyticAt_J}` plus `latticeGraph` ℤ^d variants. 16 thin wrappers of the abstract `log_vdPolymerFamilies_sum_analyticAt` (Step 606), `_analyticOnNhd_Ici_zero` (Step 607), `_tanh_analyticAt_beta` / `_J` (Step 608). **Mayer identity at edge-case parameter slices, all 4 layers** (PR #1588): `mayer_identity_at_{zero,betaJ_zero,beta_zero,J_zero}_{Λ,AlongExhaustion}` plus `latticeGraph` ℤ^d variants. 16 thin wrappers of the abstract `mayer_identity_at_zero` (Step 600) and the β/J specialisations (Step 609). **`polymerFreeEnergy_eq_mayerPartialSum` at edge-case parameter slices, all 4 layers** (PR #1589): named-wrapper restatements `polymerFreeEnergy_{Λ,AlongExhaustion}_eq_mayerPartialSum_at_{zero,betaJ_zero,beta_zero,J_zero}` plus `latticeGraph` ℤ^d variants. 16 thin wrappers of the abstract `polymerFreeEnergy_eq_mayerPartialSum_at_*` family (Steps 611, 617). **Mayer identity polymer_free_energy variants at all 4 layers** (PR #1590): `mayer_identity_at_{J_zero,beta_zero,either_zero}_polymer_free_energy_{Λ,AlongExhaustion}` plus `latticeGraph` ℤ^d variants. 12 thin wrappers of the abstract `mayer_identity_at_J_zero_polymer_free_energy` (Step 652), `_at_beta_zero_polymer_free_energy` (Step 652), `_at_either_zero_polymer_free_energy` (Step 653). **`mayerPartialSum 0 ≤ polymerFreeEnergy` family at all 4 layers** (PR #1591): `mayerPartialSum_zero_{Λ,AlongExhaustion}_{le_polymerFreeEnergy,tanh_le_polymerFreeEnergy,tanh_le_polymerFreeEnergy_ferromagnetic}` plus `latticeGraph` ℤ^d variants. 12 thin wrappers of the three abstract inequalities (Steps 654, 655, 656), establishing `mayerPartialSum G 0 ≤ polymerFreeEnergy G` at every parameter where `polymerFreeEnergy ≥ 0` is known. **Mayer identity edge-cases (no polymers / trivial / edgeless) at all 4 layers** (PR #1592): `mayer_identity_of_{no_polymers,no_polymers_tanh,trivial,edgeFinset_empty,edgeFinset_empty_tanh}_{Λ,AlongExhaustion}` plus `latticeGraph` ℤ^d variants. 20 thin wrappers of the abstract `mayer_identity_of_no_polymers` (Step 618), `_no_polymers_tanh` (Step 619), `_of_trivial` (Step 651), `_of_edgeFinset_empty` (Step 620), `_of_edgeFinset_empty_tanh` (Step 622). **Basic identities (at_zero / at_one) at all 4 layers** (PR #1593): `vdPolymerFamilies_sum_{Λ,AlongExhaustion}_{at_zero,at_one}`, `mayerPartialSum_{Λ,AlongExhaustion}_{zero,one,at_zero}`, `mayerExpansionTerm_{Λ,AlongExhaustion}_{zero,one,at_zero}` plus `latticeGraph` ℤ^d variants. 32 thin wrappers of the eight abstract base-case identities (Steps 587, 592, 598, 599, 639). **`vdPolymerFamilies_sum` iff characterizations at all 4 layers** (PR #1594): adds `vdPolymerFamilies_sum_*_tanh_{gt_one_iff,eq_one_iff}` to all 4 layers (the non-tanh `_eq_one_iff_eps_zero` and `_gt_one_iff_eps_pos` variants extend the existing Λ-layer-only versions to along-ex + ℤ^d). 14 new thin wrappers across the four iff characterizations under `0 ≤ β·J`. **`vdPolymerFamilies_sum` bound family completion at all 4 layers** (PR #1595): adds `vdPolymerFamilies_sum_*_le_two_pow`, `_le_one_plus_tanh_pow`, and `one_le_vdPolymerFamilies_sum_*` to all 4 layers (none of these had wrappers prior). 12 new thin wrappers (3 abstracts × 4 layers). **Ferromagnetic versions of `polymerFreeEnergy` sandwich + hasSum at all 5 layers** (PR #1573, under `0 ≤ J, 0 < β`): abstract `polymerFreeEnergy_tanh_high_temp_sandwich_ferromagnetic` and `polymerFreeEnergy_tanh_hasSum_via_log_of_pow_lt_two_ferromagnetic`, plus 4 layer wraps each (Λ-direct, along-ex, ℤ^d Λ-direct, ℤ^d along-ex). The four ℤ^d wrappers use the abbreviated `_ferro` suffix in place of `_ferromagnetic` to keep each declaration line within the 100-character linter budget. **Convergence-radius regime (PRs #1517, #1526, #1569)**: under `0 ≤ t` and `(1+t)^|E| < 2`, `polymerFreeEnergy_high_temp_sandwich` packages the 5-statement sandwich `0 ≤ polymerFreeEnergy G t ≤ ε(t) ≤ (1+t)^|E| - 1 < 1` plus `polymerFreeEnergy G t < log 2`; `polymerFreeEnergy_hasSum_via_log_of_pow_lt_two` gives the explicit log-Taylor `HasSum (fun n => (-1)^n · ε(t)^(n+1) / (n+1)) (polymerFreeEnergy G t)` in the same regime. **Tanh forms** (β·J substituted): `polymerFreeEnergy_tanh_high_temp_sandwich` and `polymerFreeEnergy_tanh_hasSum_via_log_of_pow_lt_two` under `0 ≤ β·J` and `(1 + tanh(β·J))^|E| < 2`. **Λ-layer wraps** (`AmbientLattice/Analyticity.lean`): `polymerFreeEnergy_Λ_high_temp_sandwich`, `polymerFreeEnergy_Λ_hasSum_via_log_of_pow_lt_two`, plus tanh variants `polymerFreeEnergy_Λ_tanh_{high_temp_sandwich,hasSum_via_log_of_pow_lt_two}`. **Along-exhaustion wraps** (`AmbientLattice/SpecialCases.lean`): `polymerFreeEnergyAlongExhaustion_{,tanh_}{high_temp_sandwich,hasSum_via_log_of_pow_lt_two}` (4 theorems, per-stage `n`). **ℤ^d concrete wraps** (`Concrete/LatticeGraphCorrelation.lean`): `polymerFreeEnergy_Λ_latticeGraph_{,tanh_}{high_temp_sandwich,hasSum_via_log_of_pow_lt_two}` (4 theorems on `latticeGraph d × Finset (Fin d → ℤ)`) plus `polymerFreeEnergyAlongExhaustion_latticeGraph_{,tanh_}{high_temp_sandwich,hasSum_via_log_of_pow_lt_two}` (4 theorems on `latticeGraph d × Exhaustion (Fin d → ℤ)`). Sharper polymer-density / Kotecky-Preiss / radius-of-convergence-in-degree estimates are deferred (require chromatic-polynomial / matrix-tree machinery not in Mathlib). (Steps 549-554; PRs #1517, #1526, #1569; Issue #1344.) | +| §18.5 | Convergence of the cluster expansion | **Done at `h = 0` (polymer-family sum sandwich + explicit log-Taylor convergence radius at all volume layers, including the polymer-family sum sandwich at every volume layer)** | `vdPolymerFamilies_sum_sandwich` (`1 ≤ ∑_Γ ∏ tanh(β·J)^|P| ≤ 2^|E|`) and `vdPolymerFamilies_sum_sandwich_sharp` (`≤ (1+tanh(β·J))^|E|`) under `0 ≤ β·J` (`ClusterExpansion.lean`). **Λ + along-ex + ℤ^d wraps for both sandwich variants** (PR #1572): `vdPolymerFamilies_sum_Λ_sandwich(_sharp)` (`AmbientLattice/Analyticity.lean`), `vdPolymerFamilies_sumAlongExhaustion_sandwich(_sharp)` (`AmbientLattice/SpecialCases.lean`), `vdPolymerFamilies_sum_Λ_latticeGraph_sandwich(_sharp)` and `vdPolymerFamilies_sumAlongExhaustion_latticeGraph_sandwich(_sharp)` (`Concrete/LatticeGraphCorrelation.lean`). **Ferromagnetic versions of both sandwich variants at all 5 layers** (PR #1574, under `0 ≤ J, 0 < β`): abstract `vdPolymerFamilies_sum_sandwich_ferromagnetic` and `_sandwich_sharp_ferromagnetic`, plus 4 layer wraps for each. The two ℤ^d sharp variants use the abbreviated `_ferro` suffix; other ferromagnetic wrappers retain `_ferromagnetic`. **Strict `freeEnergy` upper bound in convergence regime, all 5 layers** (PR #1575): abstract `freeEnergy_lt_log_two_plus_high_temp_correction` (PR #1527) plus ferromagnetic version, lifted to Λ-direct, along-exhaustion, ℤ^d Λ-direct, and ℤ^d along-exhaustion as `freeEnergyΛ_lt_log_two_plus_high_temp_correction(_ferromagnetic)`, `freeEnergyAlongExhaustion_lt_log_two_plus_high_temp_correction(_ferromagnetic)`, and the corresponding `latticeGraph` versions (with the two ℤ^d ferromagnetic variants using the abbreviated `_ferro` suffix). **`polymerFreeEnergy` regularity at all 4 layers** (PR #1576): `polymerFreeEnergy_{Λ,AlongExhaustion}_{continuousAt,differentiableAt,continuousOn_Ici_zero,differentiableOn_Ici_zero}` (`AmbientLattice/Analyticity.lean`, `AmbientLattice/SpecialCases.lean`) plus their `latticeGraph` ℤ^d variants (`Concrete/LatticeGraphCorrelation.lean`). 16 thin per-point / per-set wrappers of the abstract `polymerFreeEnergy_continuousAt` / `_differentiableAt` (Step 611) and `_continuousOn_Ici_zero` / `_differentiableOn_Ici_zero`. **`polymerFreeEnergy` β / J real-analyticity at all 4 layers** (PR #1577): `polymerFreeEnergy_{Λ,AlongExhaustion}_tanh_{analyticAt_beta,analyticAt_J,analyticOnNhd_beta_Ici_zero,analyticOnNhd_J_Ici_zero}` plus `latticeGraph` ℤ^d variants. 16 thin wrappers of the abstract `polymerFreeEnergy_tanh_analyticAt_{beta,J}` (Step 613) and `_analyticOnNhd_{beta,J}_Ici_zero` over `Set.Ici 0`. **`polymerFreeEnergy` bound family at all 4 layers** (PR #1578): `polymerFreeEnergy_{Λ,AlongExhaustion}_{nonneg_of_nonneg,le_card_log_one_plus_of_nonneg,le_card_mul_of_nonneg,monotoneOn_Ici_zero}` plus `latticeGraph` ℤ^d variants. 16 thin wrappers of the abstract `polymerFreeEnergy_nonneg_of_nonneg`, `_le_card_log_one_plus_of_nonneg`, `_le_card_mul_of_nonneg`, and `_monotoneOn_Ici_zero` bound API. **`polymerFreeEnergy` edge-cases + comparison family at all 4 layers** (PR #1579): `polymerFreeEnergy_{Λ,AlongExhaustion}_{eq_zero_of_no_polymers,eq_zero_of_edgeFinset_empty,le_of_le_of_nonneg,le_of_le_strict_form}` plus `latticeGraph` ℤ^d variants. 16 thin wrappers covering `polymerFreeEnergy = 0` on no-polymer / edgeless induced graphs (Steps 621, 623) and order preservation on `[0, ∞)` (Steps 649, 650). **`polymerFreeEnergy` tanh-bound family at all 4 layers** (PR #1580): `polymerFreeEnergy_{Λ,AlongExhaustion}_{tanh_sandwich,le_card_log_two_of_le_one,tanh_le_card_log_two,tanh_double_bound}` plus `latticeGraph` ℤ^d variants. 16 thin wrappers covering the tanh-form sandwich (Step 632), `≤ |E| · log 2` for `0 ≤ t ≤ 1` (Step 642), the tanh form thereof (Step 643), and the combined double bound (Step 645). **`mayerPartialSum` regularity at all 4 layers** (PR #1581): `mayerPartialSum_{Λ,AlongExhaustion}_{continuous,differentiable,analyticAt,continuousOn,differentiableOn}` plus `latticeGraph` ℤ^d variants. 20 thin wrappers of `mayerPartialSum_continuous` / `_differentiable` / `_analyticAt` (Step 591) and `_continuousOn` / `_differentiableOn` (Step 628). **`mayerExpansionTerm` regularity at all 4 layers** (PR #1582): `mayerExpansionTerm_{Λ,AlongExhaustion}_{continuous,differentiable,analyticAt,analyticOnNhd}` plus `latticeGraph` ℤ^d variants. 16 thin wrappers of the four abstract regularity statements (Steps 588, 589, 590). **`mayerPartialSum` tanh β/J regularity at all 4 layers** (PR #1583): `mayerPartialSum_{Λ,AlongExhaustion}_tanh_{continuous_beta,continuous_J,differentiable_beta,differentiable_J,analyticAt_beta,analyticAt_J,analyticOnNhd_beta,analyticOnNhd_J}` plus `latticeGraph` ℤ^d variants. 32 thin wrappers of the abstract `mayerPartialSum_tanh_*_{beta,J}` (Steps 594, 595, 596). **`mayerExpansionTerm` tanh β/J regularity at all 4 layers** (PR #1584): `mayerExpansionTerm_{Λ,AlongExhaustion}_tanh_{continuous_beta,continuous_J,differentiable_beta,differentiable_J,analyticAt_beta,analyticAt_J}` plus `latticeGraph` ℤ^d variants. 24 thin wrappers of the abstract `mayerExpansionTerm_tanh_*_{beta,J}` (Steps 594, 595, 596). **`vdPolymerFamilies_sum` regularity in `t` at all 4 layers** (PR #1585): `vdPolymerFamilies_sum_{Λ,AlongExhaustion}_{continuous,differentiable,analyticAt,hasDerivAt}` plus `latticeGraph` ℤ^d variants. 16 thin wrappers of the abstract `vdPolymerFamilies_sum_continuous` (Step 555), `_differentiable` (Step 558), `_analyticAt` (Step 561), and `_hasDerivAt` with explicit polynomial derivative formula (Step 575). **`vdPolymerFamilies_sum` tanh β/J regularity at all 4 layers** (PR #1586): `vdPolymerFamilies_sum_{Λ,AlongExhaustion}_tanh_{continuous_beta,continuous_J,differentiable_beta,differentiable_J,analyticAt_beta,analyticAt_J}` plus `latticeGraph` ℤ^d variants. 24 thin wrappers of the abstract `vdPolymerFamilies_sum_tanh_*_{beta,J}` (Steps 556, 559, 562). **`log_vdPolymerFamilies_sum` analyticity at all 4 layers** (PR #1587): `log_vdPolymerFamilies_sum_{Λ,AlongExhaustion}_{analyticAt,analyticOnNhd_Ici_zero,tanh_analyticAt_beta,tanh_analyticAt_J}` plus `latticeGraph` ℤ^d variants. 16 thin wrappers of the abstract `log_vdPolymerFamilies_sum_analyticAt` (Step 606), `_analyticOnNhd_Ici_zero` (Step 607), `_tanh_analyticAt_beta` / `_J` (Step 608). **Mayer identity at edge-case parameter slices, all 4 layers** (PR #1588): `mayer_identity_at_{zero,betaJ_zero,beta_zero,J_zero}_{Λ,AlongExhaustion}` plus `latticeGraph` ℤ^d variants. 16 thin wrappers of the abstract `mayer_identity_at_zero` (Step 600) and the β/J specialisations (Step 609). **`polymerFreeEnergy_eq_mayerPartialSum` at edge-case parameter slices, all 4 layers** (PR #1589): named-wrapper restatements `polymerFreeEnergy_{Λ,AlongExhaustion}_eq_mayerPartialSum_at_{zero,betaJ_zero,beta_zero,J_zero}` plus `latticeGraph` ℤ^d variants. 16 thin wrappers of the abstract `polymerFreeEnergy_eq_mayerPartialSum_at_*` family (Steps 611, 617). **Mayer identity polymer_free_energy variants at all 4 layers** (PR #1590): `mayer_identity_at_{J_zero,beta_zero,either_zero}_polymer_free_energy_{Λ,AlongExhaustion}` plus `latticeGraph` ℤ^d variants. 12 thin wrappers of the abstract `mayer_identity_at_J_zero_polymer_free_energy` (Step 652), `_at_beta_zero_polymer_free_energy` (Step 652), `_at_either_zero_polymer_free_energy` (Step 653). **`mayerPartialSum 0 ≤ polymerFreeEnergy` family at all 4 layers** (PR #1591): `mayerPartialSum_zero_{Λ,AlongExhaustion}_{le_polymerFreeEnergy,tanh_le_polymerFreeEnergy,tanh_le_polymerFreeEnergy_ferromagnetic}` plus `latticeGraph` ℤ^d variants. 12 thin wrappers of the three abstract inequalities (Steps 654, 655, 656), establishing `mayerPartialSum G 0 ≤ polymerFreeEnergy G` at every parameter where `polymerFreeEnergy ≥ 0` is known. **Mayer identity edge-cases (no polymers / trivial / edgeless) at all 4 layers** (PR #1592): `mayer_identity_of_{no_polymers,no_polymers_tanh,trivial,edgeFinset_empty,edgeFinset_empty_tanh}_{Λ,AlongExhaustion}` plus `latticeGraph` ℤ^d variants. 20 thin wrappers of the abstract `mayer_identity_of_no_polymers` (Step 618), `_no_polymers_tanh` (Step 619), `_of_trivial` (Step 651), `_of_edgeFinset_empty` (Step 620), `_of_edgeFinset_empty_tanh` (Step 622). **Basic identities (at_zero / at_one) at all 4 layers** (PR #1593): `vdPolymerFamilies_sum_{Λ,AlongExhaustion}_{at_zero,at_one}`, `mayerPartialSum_{Λ,AlongExhaustion}_{zero,one,at_zero}`, `mayerExpansionTerm_{Λ,AlongExhaustion}_{zero,one,at_zero}` plus `latticeGraph` ℤ^d variants. 32 thin wrappers of the eight abstract base-case identities (Steps 587, 592, 598, 599, 639). **`vdPolymerFamilies_sum` iff characterizations at all 4 layers** (PR #1594): adds `vdPolymerFamilies_sum_*_tanh_{gt_one_iff,eq_one_iff}` to all 4 layers (the non-tanh `_eq_one_iff_eps_zero` and `_gt_one_iff_eps_pos` variants extend the existing Λ-layer-only versions to along-ex + ℤ^d). 14 new thin wrappers across the four iff characterizations under `0 ≤ β·J`. **`vdPolymerFamilies_sum` bound family completion at all 4 layers** (PR #1595): adds `vdPolymerFamilies_sum_*_le_two_pow`, `_le_one_plus_tanh_pow`, and `one_le_vdPolymerFamilies_sum_*` to all 4 layers (none of these had wrappers prior). 12 new thin wrappers (3 abstracts × 4 layers). **`vdPolymerFamilies_sum` generic-`t` bound family + `_eq_one_add` decomposition at all 4 layers** (PR #1596): adds `vdPolymerFamilies_sum_*_{ge_one_of_nonneg,le_one_plus_pow_of_nonneg,pos_of_nonneg,eq_one_add}` to all 4 layers (none of these had wrappers prior). 16 new thin wrappers (4 abstracts × 4 layers) covering the generic-`t` bound family (`1 ≤ vdSum`, `vdSum ≤ (1+t)^|E|`, `0 < vdSum` under `0 ≤ t`) plus the `1 + ε(t)` decomposition. **Ferromagnetic versions of `polymerFreeEnergy` sandwich + hasSum at all 5 layers** (PR #1573, under `0 ≤ J, 0 < β`): abstract `polymerFreeEnergy_tanh_high_temp_sandwich_ferromagnetic` and `polymerFreeEnergy_tanh_hasSum_via_log_of_pow_lt_two_ferromagnetic`, plus 4 layer wraps each (Λ-direct, along-ex, ℤ^d Λ-direct, ℤ^d along-ex). The four ℤ^d wrappers use the abbreviated `_ferro` suffix in place of `_ferromagnetic` to keep each declaration line within the 100-character linter budget. **Convergence-radius regime (PRs #1517, #1526, #1569)**: under `0 ≤ t` and `(1+t)^|E| < 2`, `polymerFreeEnergy_high_temp_sandwich` packages the 5-statement sandwich `0 ≤ polymerFreeEnergy G t ≤ ε(t) ≤ (1+t)^|E| - 1 < 1` plus `polymerFreeEnergy G t < log 2`; `polymerFreeEnergy_hasSum_via_log_of_pow_lt_two` gives the explicit log-Taylor `HasSum (fun n => (-1)^n · ε(t)^(n+1) / (n+1)) (polymerFreeEnergy G t)` in the same regime. **Tanh forms** (β·J substituted): `polymerFreeEnergy_tanh_high_temp_sandwich` and `polymerFreeEnergy_tanh_hasSum_via_log_of_pow_lt_two` under `0 ≤ β·J` and `(1 + tanh(β·J))^|E| < 2`. **Λ-layer wraps** (`AmbientLattice/Analyticity.lean`): `polymerFreeEnergy_Λ_high_temp_sandwich`, `polymerFreeEnergy_Λ_hasSum_via_log_of_pow_lt_two`, plus tanh variants `polymerFreeEnergy_Λ_tanh_{high_temp_sandwich,hasSum_via_log_of_pow_lt_two}`. **Along-exhaustion wraps** (`AmbientLattice/SpecialCases.lean`): `polymerFreeEnergyAlongExhaustion_{,tanh_}{high_temp_sandwich,hasSum_via_log_of_pow_lt_two}` (4 theorems, per-stage `n`). **ℤ^d concrete wraps** (`Concrete/LatticeGraphCorrelation.lean`): `polymerFreeEnergy_Λ_latticeGraph_{,tanh_}{high_temp_sandwich,hasSum_via_log_of_pow_lt_two}` (4 theorems on `latticeGraph d × Finset (Fin d → ℤ)`) plus `polymerFreeEnergyAlongExhaustion_latticeGraph_{,tanh_}{high_temp_sandwich,hasSum_via_log_of_pow_lt_two}` (4 theorems on `latticeGraph d × Exhaustion (Fin d → ℤ)`). Sharper polymer-density / Kotecky-Preiss / radius-of-convergence-in-degree estimates are deferred (require chromatic-polynomial / matrix-tree machinery not in Mathlib). (Steps 549-554; PRs #1517, #1526, #1569; Issue #1344.) | | §18.6 | Analyticity of log Z in the activity | **Done (polymer-family sum, `Z`, and `freeEnergy` are `AnalyticAt ℝ` in `β`/`J` at `h = 0` via polymer expansion)** | `vdPolymerFamilies_sum_continuous` / `_differentiable` / `_analyticAt`: `Continuous`, `Differentiable ℝ`, and `AnalyticAt ℝ` (at every `t`) for `fun t => ∑_Γ ∏ t^|P|` (`ClusterExpansion.lean`). The polymer-family sum is a polynomial in `t = tanh(β·J)`; the analyticity proof goes by `Finset.induction` via the helper `analyticAt_prod_pow` (`AnalyticAt ℝ (fun s => ∏ P ∈ Γ, s^P.card) t`). Project-local `continuous_real_tanh` / `differentiable_real_tanh` / `analyticAt_real_tanh` (mathlib does not yet export `Real.continuous_tanh` / `_differentiable_tanh` / `_analyticAt_tanh`) bridge the activity to `β`/`J` via `vdPolymerFamilies_sum_tanh_continuous_beta` / `_J`, `_differentiable_beta` / `_J`, and `_analyticAt_beta` / `_J`. `partitionFunction_continuous_beta_h_zero` / `_J_h_zero`, `partitionFunction_differentiable_beta_h_zero` / `_J_h_zero`, and `partitionFunction_analyticAt_beta_h_zero` / `_J_h_zero`: combine with the §18.4 polymer-family identity (Step 548) and continuity / differentiability / analyticity of `cosh(β·J)^|E|` to obtain `Continuous`, `Differentiable ℝ`, and `AnalyticAt ℝ` versions of `(fun β => Z(J,0,β))` and `(fun J => Z(J,0,β))`. `freeEnergy_analyticAt_beta_h_zero` / `_J_h_zero` complete the §18.6 capstone: `f = (1/|ι|) · log Z` is `AnalyticAt ℝ` in β/J at every point at h=0, via `AnalyticAt.log` plus `partitionFunction_pos`. `partitionFunction_analyticOnNhd_beta_h_zero` / `_J_h_zero` and `freeEnergy_analyticOnNhd_beta_h_zero` / `_J_h_zero` (Step 565) upgrade the per-point `AnalyticAt` to the global `AnalyticOnNhd ℝ _ Set.univ` form. `vdPolymerFamilies_sum_hasDerivAt` (Step 575) provides the explicit polynomial derivative `∑_Γ ∑_{Q ∈ Γ} (∏_{P ∈ Γ.erase Q} t^{\|P\|}) · (\|Q\| · t^{\|Q\|-1})` at every `t : ℝ`, via `HasDerivAt.fun_finset_prod` (product rule) + `hasDerivAt_pow` (monomial) + `HasDerivAt.fun_sum` (linearity). **General-h capstone** (PRs #1528-#1530): `freeEnergy_analyticAt_beta_general_h`, `freeEnergy_analyticAt_J_general_h`, `freeEnergy_analyticAt_h` — `f(J, h, β)` is `AnalyticAt ℝ` in each of `β`, `J`, `h` separately at every point (no `h = 0` restriction); per-PR also includes the `AnalyticOnNhd ℝ _ Set.univ` global form (`_analyticOnNhd_beta_general_h`, `_J_general_h`, `_h`). The `h` direction does not carry the `_general_h` suffix because the abstract theorem name uses `_h` directly. **Joint analyticity** (PR #1531): `freeEnergy_analyticAt_joint` — `f` is `AnalyticAt ℝ` jointly in `(β, J, h)` at every point. **Joint AnalyticOnNhd** (PR #1532): `freeEnergy_analyticOnNhd_joint` over `Set.univ`. **Joint Continuous + Differentiable** (PR #1533): `freeEnergy_continuous_joint`, `freeEnergy_differentiable_joint`. **Λ-layer joint analyticity** (PR #1535): introduces `IsingModel/AmbientLattice/Analyticity.lean` and lifts the joint analyticity / Continuous / Differentiable hierarchy to `freeEnergyΛ`. **Correlation joint analyticity** (PRs #1536, #1537): `correlation_analyticAt_joint` and the full regularity hierarchy (Continuous / Differentiable / AnalyticAt / AnalyticOnNhd) at the abstract and Λ layers. **`gibbsExpectation_analyticAt_joint`** (PR #1539): joint analyticity of `gibbsExpectation` for an arbitrary observable `F : Configuration → ℝ`. **`partitionFunction` Continuous + Differentiable per-direction at general h** (PR #1540) and Λ-layer wrappers (PR #1541). (Steps 555-565, 575; PRs #1528-#1541; Issue #1344.) | | §18.7 | Decay of correlations | **Done at `h = 0` (exponential decay `⟨σ_iσ_j⟩ ≤ 2^|E|·tanh(β·J)^{d_G(i,j)}` at all volume layers)** | `correlation_high_temp_h_zero_le_numerator` (Step 566): under `0 ≤ β·J`, `⟨σ_A⟩ ≤ ∑_{X : ∂X = A} tanh(β·J)^{\|X\|}` reduces capstone to numerator. `evenSubgraph_pair_boundary_card_pos` (Step 567): `1 ≤ X.card`. `correlation_high_temp_h_zero_at_pair_le_two_pow_edges_mul_tanh` (Step 568): weak upper bound `⟨σ_iσ_j⟩ ≤ 2^{\|E\|} · tanh(β·J)`. Foundation lemmas: `evenSubgraph_pair_boundary_exists_edge_incident_to` (Step 569), `filter_mem_card_erase` (Step 570), `evenSubgraph_pair_boundary_card_one_adj` (Step 571), `evenSubgraph_pair_boundary_erase_swap` (Step 572). `evenSubgraph_pair_boundary_dist_le` (Step 573): graph-distance bound `G.dist i j ≤ X.card` under `∂X = {i, j}` via strong induction building an explicit `G.Walk i j`. **`correlation_high_temp_h_zero_at_pair_le_two_pow_edges_mul_tanh_pow_dist` (Step 574, capstone)**: `⟨σ_iσ_j⟩ ≤ 2^{\|E\|} · tanh(β·J)^{d_G(i,j)}` under `0 ≤ β·J` — high-temperature exponential decay in graph distance. Combines Steps 566+573 with `tanh ≤ 1` reduction (`pow_le_pow_of_le_one`). **Λ-layer + along-ex + ℤ^d wraps** (PR #1570): `correlationΛ_high_temp_h_zero_at_pair_le_two_pow_edges_mul_tanh_pow_dist` (`AmbientLattice/Defs.lean`) + `correlationAlongExhaustion_high_temp_h_zero_at_pair_le_two_pow_edges_mul_tanh_pow_dist` (`AmbientLattice/SpecialCases.lean`, per-stage `n`) + `correlationΛ_latticeGraph_high_temp_h_zero_at_pair_le_two_pow_edges_mul_tanh_pow_dist` and `correlationAlongExhaustion_latticeGraph_high_temp_h_zero_at_pair_le_two_pow_edges_mul_tanh_pow_dist` (`Concrete/LatticeGraphCorrelation.lean`, on `latticeGraph d`). **Ferromagnetic forms** (PR #1571, under `0 ≤ J, 0 < β`): abstract `correlation_high_temp_h_zero_at_pair_le_two_pow_edges_mul_tanh_pow_dist_ferromagnetic` plus the four-layer wraps `correlationΛ_..._ferromagnetic`, `correlationAlongExhaustion_..._ferromagnetic`, `correlationΛ_latticeGraph_..._ferromagnetic`, `correlationAlongExhaustion_latticeGraph_h_zero_at_pair_le_two_pow_edges_mul_tanh_pow_dist_ferro` (the last variant drops `_high_temp` and uses `_ferro` instead of `_ferromagnetic` to keep the name under the `linter.style.longLine` 100-character budget). Each ferromagnetic form derives `0 ≤ β·J` from `mul_nonneg hβ.le hJ`. (PRs #1570, #1571; Issue #1344.) | diff --git a/tex/proof-guide.tex b/tex/proof-guide.tex index c6e26a403..f3d8f03fb 100644 --- a/tex/proof-guide.tex +++ b/tex/proof-guide.tex @@ -3500,6 +3500,22 @@ \section{Cluster (polymer / Mayer) expansion (\S18.4--\S18.7)} thin direct-instantiation wrappers (3 abstracts $\times$ 4 layers). +\paragraph{\texttt{vdPolymerFamilies\_sum} generic-\textit{t} +bounds + decomposition, all volume layers (\S18.5, PR~\#1596).} +Adds 4-layer wraps for the four abstract generic-\textit{t} +theorems +\texttt{\_ge\_one\_of\_nonneg}, +\texttt{\_le\_one\_plus\_pow\_of\_nonneg}, +\texttt{\_pos\_of\_nonneg}, and \texttt{\_eq\_one\_add} +(which had no wrappers before). 16 new thin +direct-instantiation wrappers (4 abstracts $\times$ 4 layers). +The generic-\textit{t} bounds are the non-tanh ($t \geq 0$) +counterparts of the tanh bound family from PR~\#1595; the +\texttt{\_eq\_one\_add} decomposition expresses +$\mathrm{vdSum}(G,t) = 1 + \varepsilon(t)$ where +$\varepsilon(t) = \sum_{\Gamma \neq \emptyset} \prod_{P \in +\Gamma} t^{|P|}$. + \paragraph{\texttt{vdPolymerFamilies\_sum} iff characterizations, all volume layers (\S18.5, PR~\#1594).} The four abstract iff characterizations (\texttt{\_eq\_one\_iff\_eps\_eq\_zero},