GJ §18.4–18.5: general interacting cluster-expansion convergence (Kotecký–Preiss / tree-graph)

[phasetr]

Purpose

Establish the general interacting Mayer/cluster expansion identity and its
convergence — the capstone of GJ §18.4–18.5 (the Mayer–Montroll exponential
formula Ξ = exp(∑ cluster terms) / log Ξ = ∑_n mayerExpansionTerm, valid for
arbitrary activity t in a convergence regime), for an interacting polymer gas
(not just the non-interacting / vertex-disjoint case already done).

Background

The non-interacting case is complete (MayerCore/Independent*.lean,
PRs #3945–#3948, #3951): there the Mayer expansion converges to the polymer free
energy by the diagonal collapse + single-polymer log(1+t^|P|) series. The
finite-order coefficients are also done: the n = 3 Ursell classification
(#3949, #3950, #3952) and the closed form of the third (first interacting) Mayer
term (#3953), plus the n = 2 term (Step 593/614).

The general interacting case needs a genuine convergence criterion. The naive
Ursell bound |ϕ^T(ω)| ≤ 2^|E(G(ω))|/n! (Step 603) does not give absolute
convergence of ∑_n ∑_ω |ϕ^T(ω)|·|z(ω)|. The standard routes are:

• Kotecký–Preiss criterion: a function a(P) > 0 with
  ∑_{Q ≁ P} |z(Q)| e^{a(Q)} ≤ a(P) for every polymer P, giving
  ∑_{Γ ∋ P} |ϕ^T(Γ)| ∏ |z| ≤ a(P) and hence absolute convergence + analyticity.
• Penrose / tree-graph inequality: |∑_{connected S} (-1)^|S|| ≤ #{spanning trees}
  bounding the Ursell coefficient by a sum over tree subgraphs.

Tracking (PR checklist)

• Tree-graph / Penrose bound on alternatingConnectedSubgraphSum (Ursell numerator) — M1 (feat(gj-18.4): Penrose Boolean-interval cancellation + spanning-tree API — #3954 #3987-feat(gj-18.4): Penrose tree-graph inequality |altSum| ≤ numSpanningTrees — #3954 #3992) + Ursell tree bound (feat(gj-18.4): Ursell tree bound from the Penrose inequality — #3954 #3993)
• Kotecký–Preiss criterion statement + the per-polymer cluster sum bound — the activity-sum criterion e·∑_P|t|^{|P|} < 1 (feat(gj-18.4): absolute convergence of the Mayer expansion — #3954 #3996), via K_n count bound (feat(gj-18.4): K_n spanning-tree count bound n^(n-1) via parent injection — #3954 #3994) + summable majorant radius 1/e (feat(gj-18.4): summable Mayer majorant — radius 1/e via ratio test — #3954 #3995)
• Absolute convergence of ∑_n mayerExpansionTerm under KP — summable_mayerExpansionTerm_of_exp_one_mul_activity_lt_one (feat(gj-18.4): absolute convergence of the Mayer expansion — #3954 #3996, general interacting)
• Mayer–Montroll identity log Ξ = ∑_n mayerExpansionTerm (general t, KP regime) — mayer_identity_general_t (MayerMontroll.lean, Issue Mayer expansion general-t identity for log Ξ (GJ §18.4 capstone) #1499 Phase C, PR feat(gj-18.4): Mayer–Montroll cluster identity log Ξ = ∑ₙ mayerExpansionTerm (general t) — #1499 #3998) + per-site KP form polymerFreeEnergy_eq_tsum_mayerExpansionTerm_of_persite_kp (MayerIdentityPersiteKP.lean, PR feat(gj-18.6): volume-uniform per-site KP Mayer-Montroll identity — #4149 #4152)
• High-temperature Ising specialisation: KP satisfied for small tanh(βJ) — summable_mayerExpansionTerm_tanh (feat(gj-18.4): high-temperature convergence of the Ising cluster expansion — #3954 #3997)
• Λ-layer + ℤ^d wrappers (feat(gj-18.5): KP per-site Mayer bound on the ambient lattice (ℤ^d-uniform) — #3954 #4148 latticeGraph_kp_tsum_per_site_le, volume-uniform KP per-site bound); remaining tie to polymerFreeEnergy / freeEnergy

References

• Glimm–Jaffe, Quantum Physics, 2nd ed., §18.4 ("Convergence: The Main Ideas", p. 332) – §18.5 (p. 335).
• Friedli–Velenik, Statistical Mechanics of Lattice Systems, §5.7 (cluster expansion, KP).
• Kotecký–Preiss, Cluster expansion for abstract polymer models, CMP 103 (1986).
• Penrose tree-graph inequality (Brydges' lectures).

Part of the broader §18 cluster-expansion programme (Issue #1499).

[phasetr]

PR #3956 merged (first checklist item, complete-graph case): the Penrose tree-graph inequality is established for K_n — abs_alternatingConnectedSubgraphSum_completeGraph_le_cayley (|altSum K_n| ≤ n^(n-2), Cayley's spanning-tree count) and the Ursell form abs_ursellCoefficient_complete_le_cayley_div (|ϕ^T| ≤ n^(n-2)/n!), via the elementary (n-1)! ≤ n^(n-2) (factorial_pred_le_pow_sub_two). New file ClusterExpansion/TreeGraphBound.lean. Next: the general-graph Penrose partition scheme (hard), or define the spanning-tree count + Cayley framework, or pursue the abstract Kotecký–Preiss criterion directly.

[phasetr]

PR #3957 merged (reduction layer): abs_alternatingConnectedSubgraphSum_le_card (crude |altSum G| ≤ #connectedSpanning for any G) + abs_ursellCoefficient_le_of_abs_alternatingConnectedSubgraphSum_le/_le_nat (any altSum bound B ⟹ |ϕ^T| ≤ B/n!). The general-graph Penrose bound on the alternating sum is now the sole remaining hard input. Next: the Penrose partition scheme (|altSum G| ≤ #spanning-trees(G)) — needs a spanning-tree-count definition + the sign-cancellation argument; or pursue the abstract KP criterion directly.

[phasetr]

PR #3958 merged (KP criterion definition layer): KPAdmissible G z a (∀ P, ∑_{Q≁P} |z Q|·exp(a Q) ≤ a P) + structural consequences weight_nonneg (0 ≤ a P) and activity_le_weight (|z P| ≤ a P). New file ClusterExpansion/KoteckyPreiss.lean. Next: the KP main theorem (per-polymer cluster-sum bound ∑_{Γ∋P} |ϕ^T(Γ)|∏|z| ≤ a P by induction, consuming the tree-graph inequality), and/or the general-graph Penrose partition scheme — both hard, multi-PR.

[phasetr]

PR #3959 merged (KP structural API): KPAdmissible.mono_activity (monotone in activity) + KPAdmissible.activity_sum_le_weight (∑_{Q≁P}|z Q| ≤ a P). #3954 foundation now: tree-graph complete-graph bound (#3956) + reduction layer (#3957) + KP criterion (#3958) + KP structural API (#3959). Remaining hard cores: KP main theorem (per-polymer cluster-sum bound by induction) and general-graph Penrose partition scheme.