Purpose
Prove the general-t Mayer expansion identity at finite volume:
log (∑_{Γ ∈ vdCompatiblePolymerFamilies G} ∏_{P ∈ Γ} t^|P|)
i.e. polymerFreeEnergy G t = mayerPartialSum G ∞ t in somet = 0.
Background
Steps 575-656 established complete infrastructure (PRs #1417 -#1498 ).
Tracking
Phase A — formal-series infrastructure
vdPolymerFamilies_sum_eq_one_add (PR feat: Step 657 — vdPolymerFamilies_sum = 1 + (Γ ≠ ∅) (Mayer general-t, GJ §18.4) #1500 polymerFreeEnergy_eq_log_one_add_eps (PR feat: Step 658 — polymerFreeEnergy = log(1 + ε) form (Mayer general-t, GJ §18.4) #1501 vdPolymerFamilies_sum_minus_one_at_zero (PR feat: Step 659 — ε(0) = 0 (Mayer general-t, GJ §18.4) #1502 vdPolymerFamilies_sum_minus_one_nonneg_of_nonneg (PR feat: Step 660 — ε(t) ≥ 0 for t ≥ 0 (Mayer general-t, GJ §18.4) #1503 vdPolymerFamilies_sum_minus_one_le_of_nonneg — ε ≤ (1+t)^|E| - 1 (PR feat: Step 661 — ε(t) ≤ (1+t)^|E| - 1 (Mayer general-t, GJ §18.4) #1504 feat: Mayer general-t identity bundled (GJ §18.4 capstone, Issue #1499) #1512 polymerFreeEnergy_hasSum_via_log — log Taylor expansion under |ε| < 1feat: explicit convergence radius for Mayer log expansion (Mayer Phase A2, Issue #1499) #1517 polymerFreeEnergy_hasSum_via_log_of_pow_lt_two — explicit convergence radius (1+t)^|E| < 2feat: mayer expansion term — filter to connected G(ω) (§18.4 sharpening, Issue #1499) #1521 mayerExpansionTerm_filter_connected — sharpens to cluster sequencesfeat: mayer partial sum filter-connected form (§18.4 sharpening, Issue #1499) #1522 mayerPartialSum_filter_connectedfeat: polymerFreeEnergy ≤ ε(t) ≤ (1+t)^|E| - 1 (§18.4 sharper bound, Issue #1499) #1523 polymerFreeEnergy_le_eps_of_nonneg and polymerFreeEnergy_le_pow_sub_one_of_nonnegfeat: polymerFreeEnergy < log 2 under (1+t)^|E| < 2 (§18.4 sharpening, Issue #1499) #1524 polymerFreeEnergy_lt_log_two_of_pow_lt_twofeat: polymerFreeEnergy ≤ ε(tanh(β·J)) bound for ferromagnetic high-temperature (§18.4 sharpening, Issue #1499) #1525 feat: polymerFreeEnergy ≤ ε(t) ≤ (1+t)^|E| - 1 (§18.4 sharper bound, Issue #1499) #1523 feat: polymerFreeEnergy < log 2 under (1+t)^|E| < 2 (§18.4 sharpening, Issue #1499) #1524 feat: polymerFreeEnergy high-temperature regime bundled summary (§18.4 sharpening, Issue #1499) #1526 polymerFreeEnergy_high_temp_sandwich — bundled summary
Phase B — combinatorial identity for K_n
Phase C — capstone
References
Purpose
Prove the general-t Mayer expansion identity at finite volume:
log (∑_{Γ ∈ vdCompatiblePolymerFamilies G} ∏_{P ∈ Γ} t^|P|)
= ∑_{n ≥ 0} mayerExpansionTerm G n t
i.e.
polymerFreeEnergy G t = mayerPartialSum G ∞ tin someneighbourhood of
t = 0.Background
Steps 575-656 established complete infrastructure (PRs #1417-#1498).
Recent sharpenings extend the convergence-regime bound infrastructure.
Tracking
Phase A — formal-series infrastructure
vdPolymerFamilies_sum_eq_one_add(PR feat: Step 657 — vdPolymerFamilies_sum = 1 + (Γ ≠ ∅) (Mayer general-t, GJ §18.4) #1500)polymerFreeEnergy_eq_log_one_add_eps(PR feat: Step 658 — polymerFreeEnergy = log(1 + ε) form (Mayer general-t, GJ §18.4) #1501)vdPolymerFamilies_sum_minus_one_at_zero(PR feat: Step 659 — ε(0) = 0 (Mayer general-t, GJ §18.4) #1502)vdPolymerFamilies_sum_minus_one_nonneg_of_nonneg(PR feat: Step 660 — ε(t) ≥ 0 for t ≥ 0 (Mayer general-t, GJ §18.4) #1503)vdPolymerFamilies_sum_minus_one_le_of_nonneg— ε ≤ (1+t)^|E| - 1 (PR feat: Step 661 — ε(t) ≤ (1+t)^|E| - 1 (Mayer general-t, GJ §18.4) #1504)polymerFreeEnergy_hasSum_via_log— log Taylor expansion under |ε| < 1polymerFreeEnergy_hasSum_via_log_of_pow_lt_two— explicit convergence radius(1+t)^|E| < 2mayerExpansionTerm_filter_connected— sharpens to cluster sequencesmayerPartialSum_filter_connectedpolymerFreeEnergy_le_eps_of_nonnegandpolymerFreeEnergy_le_pow_sub_one_of_nonnegpolymerFreeEnergy_lt_log_two_of_pow_lt_twopolymerFreeEnergy_high_temp_sandwich— bundled summaryPhase B — combinatorial identity for K_n
(-1)^(n-1) · (n-1)!—alternatingConnectedSubgraphSum_completeGraph_closed_forminMayerRootComponent.lean. Proved via the root-component recurrenceD_n = ∑_{C ∋ 0} c_{|C|} D_{n-|C|}(no chromatic-polynomial / matrix-tree machinery needed). Chain: Add Mayer K_n D_n foundation: signed all-subgraph sum (GJ §18.4) #3489 D_n foundation → Add Mayer K_n iso-invariance of c and D (GJ §18.4) #3490 iso-invariance → Add Mayer K_n root-component bijection foundations (GJ §18.4) #3491-Add Mayer K_n edge-count split and inside-connected crux (GJ §18.4) #3493 root-component split + inside-connected crux → Add Mayer K_n root-component fiber sum (GJ §18.4) #3494 fibre product split → Add Mayer K_n root-component fiberwise recurrence (GJ §18.4) #3495 fibrewise → Add Mayer K_n root-component reindex to subtype complete graphs (GJ §18.4) #3496 outside reindex → Add Mayer K_n inside factor reindex (GJ §18.4) #3497 inside reindex + recurrence → Add Mayer K_n recurrence collapse toward closed form (GJ §18.4) #3498 collapse + closed form.deciderequires ≥30 min build per CI run (1024 powerset elements), not viablePhase C — capstone
mayer_identity_general_t: UNBLOCKED (Phase B K_n closed form done; Issue GJ §18.4–18.5: general interacting cluster-expansion convergence (Kotecký–Preiss / tree-graph) #3954 M2 convergence chain done through feat(gj-18.4): high-temperature convergence of the Ising cluster expansion — #3954 #3997: Penrose tree-graph inequality, Ursell tree bound, K_n count bound, summable majorant, general absolute convergence, high-temperature Ising convergence). Remaining = the Mayer-Montroll identity equating the log-Taylor epsilon-series (polymerFreeEnergy_hasSum_via_log, LogTaylor.lean) with the cluster sumtsum (mayerExpansionTerm G . t). Planned as one large GJ-unit PR (Part of Mayer expansion general-t identity for log Ξ (GJ §18.4 capstone) #1499). Verified first brick:logTaylor_eps_term_eq_sum_vdFamilyTuplesviavdPolymerFamilies_sum_minus_one_pow(LogTaylor.lean:131).References