feat: §18.5 vdPolymerFamilies_sum generic-t bound family 4-layer wraps GJ-命題-bundle

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

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

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

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},