GJ §18.4–§18.7: Lattice Ising cluster expansion

[phasetr]

Purpose

Formalize the cluster (polymer) expansion for the lattice Ising model, GJ §18.4–§18.7:

• §18.4 Cluster expansion machinery (lattice version): polymer decomposition, log Z = ∑ over connected polymers
• §18.5 Convergence of the cluster expansion in activity tanh(βJ)
• §18.6 Analyticity of log Z in activity within convergence radius
• §18.7 Exponential decay of ⟨σ_iσ_j⟩ in |i-j| at high temperature

Built on the FV (3.45) closed form Z = 2^|ι|·cosh^|E|·∑_{X even} tanh^|X| already formalized through §18.3.

Background

The cluster expansion is the standard tool for proving high-temperature regime properties (uniqueness of phase, exponential decay, analyticity in coupling). For the lattice Ising model:

1. The FV (3.45) representation expresses Z / (2^|ι| · cosh^|E|) as a sum over even-degree subgraphs of G.
2. Even subgraphs decompose into vertex-disjoint connected components (= polymers).
3. log Z - |ι|·log 2 - |E|·log cosh(βJ) is then a sum over multi-sets of polymers, equivalent (via Mayer expansion) to a sum over clusters with the Ursell coefficient.
4. Convergence in tanh(βJ) (small) gives all the high-temperature analytic properties.

Tracking

§18.4 foundations (Steps 503-541, 39 PRs merged)

Foundations (Steps 503-516)

• Step 503: IsEvenSubgraph foundation (PR feat: Step 503 — IsEvenSubgraph foundation for cluster expansion (GJ §18.4) #1345)
• Step 504: IsPolymer (connected even subgraph) (PR feat: Step 504 — IsPolymer (connected even subgraph) for cluster expansion (GJ §18.4) #1346)
• Step 505: polymer compatibility (edge-disjointness) (PR feat: Step 505 — polymer compatibility (edge-disjointness) (GJ §18.4) #1347)
• Step 506: IsCompatiblePolymerFamily (PR feat: Step 506 — compatible polymer family (GJ §18.4) #1348)
• Step 507: IsEvenSubgraph.union_disjoint (PR feat: Step 507 — union of disjoint even subgraphs is even (GJ §18.4) #1349)
• Step 508: IsCompatiblePolymerFamily.biUnion_isEvenSubgraph (PR feat: Step 508 — compatible polymer family unions to an even subgraph (GJ §18.4) #1350)
• Step 509: IsCompatiblePolymerFamily.card_biUnion (PR feat: Step 509 — card additivity over compatible polymer family (GJ §18.4) #1351)
• Step 510: pow_card_biUnion weight multiplicativity (PR feat: Step 510 — weight multiplicativity over compatible polymer family (GJ §18.4) #1352)
• Step 511: polymerPartition abstract definition (PR feat: Step 511 — polymer partition function (abstract) (GJ §18.4) #1353)
• Step 512: IsCompatiblePolymerFamily.mono (PR feat: Step 512 — monotonicity of compatible polymer family (GJ §18.4) #1354)
• Step 513: allPolymers G (PR feat: Step 513 — allPolymers G as the natural polymer universe (GJ §18.4) #1355)
• Step 514: polymerActivity + latticeIsingPolymerPartition (PR feat: Step 514 — lattice Ising polymer partition function (GJ §18.4) #1356)
• Step 515: evenSubgraphs G (PR feat: Step 515 — evenSubgraphs G as the Finset of all even subgraphs (GJ §18.4) #1357)
• Step 516: evenSubgraphs_eq_inline_filter (PR feat: Step 516 — evenSubgraphs ↔ inline FV (3.45) filter bridge (GJ §18.4) #1358)
• Step 517: FV (3.45) via evenSubgraphs G (PR feat: Step 517 — FV (3.45) closed form via evenSubgraphs G (GJ §18.4) #1359)

Vertex-disjoint compatibility (Steps 518-522, per codex feedback)

• Step 518: polymerSupport + IsPolymerVertexDisjoint (PR feat: Step 518 — polymerSupport + IsPolymerVertexDisjoint (GJ §18.4) #1360)
• Step 519: IsPolymerVertexDisjoint API (PR feat: Step 519 — IsPolymerVertexDisjoint API (GJ §18.4) #1361)
• Step 520: IsCompatiblePolymerFamilyVertexDisjoint (PR feat: Step 520 — vertex-disjoint compatible polymer family (GJ §18.4) #1362)
• Step 521: VD-family corollaries (PR feat: Step 521 — vertex-disjoint family corollaries (GJ §18.4) #1363)
• Step 522: VD-family singleton + monotonicity (PR feat: Step 522 — vertex-disjoint family singleton + monotonicity (GJ §18.4) #1364)

Edge-adjacency / connectivity / partition function API (Steps 523-531)

• Step 523: edge-adjacency symmetry (PR feat: Step 523 — edge-adjacency symmetry (GJ §18.4) #1365)
• Step 524: ReflTransGen edgeAdjacentIn symmetry (PR feat: Step 524 — ReflTransGen edgeAdjacentIn symmetry (GJ §18.4) #1366)
• Step 525: polymerSupport union/empty (PR feat: Step 525 — polymerSupport union/empty lemmas (GJ §18.4) #1367)
• Step 526: polymerSupport biUnion (PR feat: Step 526 — polymerSupport biUnion identity (GJ §18.4) #1368)
• Step 527: VD-family insertion lemma (PR feat: Step 527 — vertex-disjoint family insertion lemma (GJ §18.4) #1369)
• Step 528: polymerPartition_singleton (PR feat: Step 528 — polymerPartition singleton evaluation (GJ §18.4) #1370)
• Step 529: polymerPartition_ge_one (PR feat: Step 529 — polymerPartition_ge_one (GJ §18.4) #1371)
• Step 530: latticeIsingPolymerPartition_ge_one (PR feat: Step 530 — lattice Ising polymer partition ≥ 1 under 0 ≤ β·J (GJ §18.4) #1372)
• Step 531: VD-family support card additivity (PR feat: Step 531 — VD-family support card additivity (GJ §18.4) #1373)

Connected components decomposition (Steps 532-541) ← KEY MILESTONE

• Step 532: edgeComponent definition (PR feat: Step 532 — edgeComponent definition (GJ §18.4) #1374)
• Step 533: edgeComponent consistency under reachability (PR feat: Step 533 — edgeComponent consistency under reachability (GJ §18.4) #1375)
• Step 534: edgeComponent_eq_or_disjoint (PR feat: Step 534 — edgeComponents equal or disjoint (GJ §18.4) #1376)
• Step 535: edgeComponent_absorbs_incident (PR feat: Step 535 — edgeComponent absorbs X-incident edges (GJ §18.4) #1377)
• Step 536: IsEvenSubgraph.toEdgeComponent (component is even) (PR feat: Step 536 — edgeComponent of even subgraph is itself even (GJ §18.4) #1378)
• Step 537: edgeComponent_isPolymer for even X (PR feat: Step 537 — edgeComponent of even subgraph is a polymer (GJ §18.4) #1379)
• Step 538: polymerDecomposition X definition (PR feat: Step 538 — polymerDecomposition definition (GJ §18.4) #1380)
• Step 539: polymerDecomposition_biUnion_id = X (PR feat: Step 539 — polymerDecomposition biUnion equals X (GJ §18.4) #1381)
• Step 540: polymerDecomposition_isPolymer for even X (PR feat: Step 540 — polymerDecomposition members are polymers (GJ §18.4) #1382)
• Step 541: polymerDecomposition_isCompatibleVertexDisjoint (PR feat: Step 541 — polymerDecomposition is vertex-disjoint compatible (GJ §18.4) #1383)

Bijection X ↔ Γ (Steps 542+)

The X → Γ direction is now done (Steps 538-541). The Γ → X direction is the obvious Γ.biUnion id (already proved even by Step 508/521). Remaining:

• Step 542: polymerDecomposition_main (PR feat: Step 542 — even subgraph polymer decomposition main statement (GJ §18.4) #1384) — partial bijection statement; full Equiv between evenSubgraphs G and the VD-compatible polymer families with biUnion ⊆ G
• Steps 543-547: bijection refinement / vdCompatiblePolymerFamilies G definition / FV (3.45) ↔ polymer-family sum identity (evenSubgraphs_sum_eq_vdPolymerFamilies_sum)
• Step 548: MAIN identity partitionFunction_high_temp_expansion_h_zero_polymer_family — Z(J,0,β) = 2^|ι|·cosh(β·J)^|E|·∑_{Γ ∈ vdCompatiblePolymerFamilies G} ∏_{P ∈ Γ} tanh(β·J)^|P| (FV (3.45) in polymer-family form).
• Mayer expansion: log Ξ = ∑ Ursell terms (in progress; current identity is at the level of Z, not log Z)
  • Step 576: PolymersIncompatible foundation — incompatibility relation, decidability, symmetry, self-incompatibility for non-empty polymers (multi-set cluster convention) (PR feat: Step 576 — polymer incompatibility relation (Mayer expansion foundation, GJ §18.4) #1418)
  • Step 577: incompatibilityGraph : SimpleGraph (Finset (Sym2 ι)) via SimpleGraph.fromRel PolymersIncompatible — adjacency characterisation P ≠ Q ∧ PolymersIncompatible P Q, DecidableRel instance (PR feat: Step 577 — polymer incompatibility graph (Mayer expansion foundation, GJ §18.4) #1419)
  • Step 578: IsClusterPolymerSet G Γ (set-level cluster, no multiplicity yet) — non-empty + all-polymer + induced incompatibility subgraph Connected; singleton case IsClusterPolymerSet.singleton (PR feat: Step 578 — cluster polymer set definition (Mayer expansion foundation, GJ §18.4) #1420)
  • Step 579: polymerSeqIncompatibilityGraph (ω : α → Finset (Sym2 ι)) : SimpleGraph α — index-side incompatibility graph for polymer sequences (α arbitrary), recovers Step 577 at α = Finset (Sym2 ι), ω = id (PR feat: Step 579 — polymer-sequence incompatibility graph (Mayer expansion foundation, GJ §18.4) #1421)
  • Step 580: IsClusterPolymerSequence G (hn : 1 ≤ n) (ω : Fin n → polymers) — sequence-level cluster (allows multiplicities at distinct indices); singleton case IsClusterPolymerSequence.singleton (PR feat: Step 580 — cluster polymer sequence definition (Mayer expansion foundation, GJ §18.4) #1422)
  • Step 581: clusterSeqActivity t ω := ∏ i, t ^ (ω i).card — sequence activity factor for Mayer-expansion sums (multiplicative over polymer indices) (PR feat: Step 581 — cluster sequence activity (Mayer expansion foundation, GJ §18.4) #1423)
  • Step 582: connectedSpanningEdgeSubsets G : Finset (Finset (Sym2 V)) — edge subsets S ⊆ G.edgeFinset whose spanning fromEdgeSet ↑S is Connected; building block for the Ursell coefficient (PR feat: Step 582 — connected spanning edge subsets (Mayer expansion foundation, GJ §18.4) #1424)
  • Step 583: ursellCoefficient (ω : Fin n → polymers) := (∑_{S ∈ connectedSpanningEdgeSubsets G(ω)} (-1)^|S|) / n! — the combinatorial weight in the Mayer expansion; singleton case ursellCoefficient_singleton proves ϕ^T(ω) = 1 for n=1 (PR feat: Step 583 — Ursell coefficient definition (Mayer expansion foundation, GJ §18.4) #1425)
  • Step 584: ursellCoefficient_eq_zero_of_disconnected — ϕ^T(ω) = 0 when G(ω) is not Connected; the Mayer-expansion sum effectively restricts to cluster sequences (PR feat: Step 584 — Ursell vanishes for disconnected sequences (Mayer expansion, GJ §18.4) #1426)
  • Step 585: ursellCoefficient_pair_incompatible — ϕ^T(ω) = -1/2 for n=2 sequences with PolymersIncompatible (ω 0) (ω 1); gives leading Mayer coefficient -(1/2) ∑_{P,Q incompat} z(P)z(Q) (PR feat: Step 585 — Ursell coefficient at n=2 incompatible pair (Mayer expansion, GJ §18.4) #1427)
  • Step 586: ursellCoefficient_pair_compatible (= 0) + unified ursellCoefficient_pair (case-conditional) (PR feat: Step 586 — Ursell coefficient n=2 compatible + unified pair formula (Mayer expansion, GJ §18.4) #1428)
  • Step 587: mayerExpansionTerm G n t := ∑_{ω ∈ piFinset (allPolymers G)} ϕ^T(ω) · z(t, ω) + base cases (n=0: vanishes, n=1: total polymer activity ∑_P t^|P|) (PR feat: Step 587 — Mayer expansion n-th term + base cases (Mayer expansion, GJ §18.4) #1429)
  • Step 588: clusterSeqActivity_continuous + mayerExpansionTerm_continuous — continuity in t (PR feat: Step 588 — Mayer expansion term continuous in t (Mayer expansion, GJ §18.4) #1430)
  • Step 589: clusterSeqActivity_differentiable + mayerExpansionTerm_differentiable — differentiability in t (PR feat: Step 589 — Mayer expansion term differentiable in t (Mayer expansion, GJ §18.4) #1431)
  • Step 590: clusterSeqActivity_analyticAt + mayerExpansionTerm_analyticAt + mayerExpansionTerm_analyticOnNhd — real-analyticity in t (PR feat: Step 590 — Mayer expansion term analytic in t (Mayer expansion, GJ §18.4) #1432)
  • Step 591: mayerPartialSum G N t := ∑_{n=0..N} mayerExpansionTerm G n t + Continuous/Differentiable/AnalyticAt/AnalyticOnNhd (PR feat: Step 591 — Mayer expansion partial sum + analyticity (Mayer expansion, GJ §18.4) #1433)
  • Step 592: mayerPartialSum_zero (= 0) + mayerPartialSum_one (= ∑_P t^|P|, leading non-trivial truncation) (PR feat: Step 592 — Mayer partial sum base cases (Mayer expansion, GJ §18.4) #1434)
  • Step 593: mayerExpansionTerm_two — explicit pair sum -1/2 · ∑_{(P, Q) incompat} t^|P| · t^|Q| via piFinset ↔ ×ˢ bijection (PR feat: Step 593 — Mayer n=2 term explicit pair sum (Mayer expansion, GJ §18.4) #1435)
  • Step 594: mayerExpansionTerm_tanh_continuous_beta / _J + mayerPartialSum_tanh_continuous_beta / _J — lift continuity from t to β, J via tanh chain (PR feat: Step 594 — Mayer expansion term continuous in β, J (Mayer expansion, GJ §18.4) #1436)
  • Step 595: mayerExpansionTerm_tanh_differentiable_beta / _J + mayerPartialSum_tanh_differentiable_beta / _J — lift differentiability from t to β, J via tanh chain (PR feat: Step 595 — Mayer expansion term differentiable in β, J (Mayer expansion, GJ §18.4) #1437)
  • Step 596: mayerExpansionTerm_tanh_analyticAt_beta / _J + mayerPartialSum_tanh_analyticAt_beta / _J + global AnalyticOnNhd over Set.univ — lift real-analyticity from t to β, J (PR feat: Step 596 — Mayer expansion term analytic in β, J (Mayer expansion, GJ §18.4) #1438)
  • Step 597: mayerExpansionTerm_two_filter — cleaner form -1/2 · ∑_{(P,Q) incompat} t^|P| · t^|Q| (filter form) (PR feat: Step 597 — Mayer n=2 term filter form (Mayer expansion, GJ §18.4) #1439)
  • Step 598: mayerExpansionTerm_at_zero + mayerPartialSum_at_zero — vanishing at t=0 (n=0 via Step 587, n ≥ 1 via 0^|P| = 0 for polymers) (PR feat: Step 598 — Mayer expansion term vanishes at t=0 (Mayer expansion, GJ §18.4) #1440)
  • Step 599: vdPolymerFamilies_sum_at_zero = 1 — only empty family contributes; verifies Mayer identity at t=0 (log 1 = 0 = mayerPartialSum) (PR feat: Step 599 — vdPolymerFamilies_sum at t=0 (Mayer expansion, GJ §18.4) #1441)
  • Step 600 milestone: mayer_identity_at_zero — first verified instance of log (vdPolymerFamilies_sum G t) = mayerPartialSum G N t (at t=0; general t deferred) (PR feat: Step 600 — Mayer identity at t=0 milestone (Mayer expansion, GJ §18.4) #1442)
  • Step 601: ursellCoefficient_abs_le — triangle bound |ϕ^T(ω)| ≤ |connectedSpanningEdgeSubsets G(ω)| / n! (PR feat: Step 601 — Ursell coefficient absolute bound (Mayer expansion, GJ §18.4) #1443)
  • Step 602: connectedSpanningEdgeSubsets_card_le_pow — |connSpan| ≤ 2^|E| (filter ⊆ powerset) (PR feat: Step 602 — connectedSpanningEdgeSubsets card bound (Mayer expansion, GJ §18.4) #1444)
  • Step 603: ursellCoefficient_abs_le_pow_div_factorial — uniform bound |ϕ^T(ω)| ≤ 2^|E| / n! (combine 601 + 602) (PR feat: Step 603 — uniform Ursell bound (Mayer expansion, GJ §18.4) #1445)
  • Step 604: mayerExpansionTerm_abs_le — triangle bound |mayerExpansionTerm| ≤ ∑_ω |ϕ^T| · |z| (PR feat: Step 604 — Mayer expansion term absolute bound (Mayer expansion, GJ §18.4) #1446)
  • Step 605: vdPolymerFamilies_sum_ge_one_of_nonneg + _pos_of_nonneg — generic ≥ 1 / > 0 under t ≥ 0 (PR feat: Step 605 — vdPolymerFamilies_sum ≥ 1 under t ≥ 0 (Mayer expansion, GJ §18.4) #1447)
  • Step 606: log_vdPolymerFamilies_sum_analyticAt — Real.log (vdPolymerFamilies_sum G t) is AnalyticAt ℝ at t ≥ 0 (LHS of Mayer identity is analytic) (PR feat: Step 606 — log (vdPolymerFamilies_sum) analyticAt (Mayer expansion, GJ §18.4) #1448)
  • Step 607: log_vdPolymerFamilies_sum_analyticOnNhd_Ici_zero — global AnalyticOnNhd ℝ _ (Set.Ici 0) (PR feat: Step 607 — log (vdPolymerFamilies_sum) AnalyticOnNhd over [0,∞) (Mayer expansion, GJ §18.4) #1449)
  • Step 608: log_vdPolymerFamilies_sum_tanh_analyticAt_beta / _J under 0 ≤ β·J — log analyticity lifted to β/J via tanh chain (PR feat: Step 608 — log_vdPolymerFamilies_sum analytic in β, J (Mayer expansion, GJ §18.4) #1450)
  • Step 609: mayer_identity_at_betaJ_zero + _beta_zero + _J_zero — Mayer identity at β·J = 0 (extends Step 600) (PR feat: Step 609 — Mayer identity at β·J=0 (Mayer expansion, GJ §18.4) #1451)
  • Step 610: polymerFreeEnergy G t := Real.log (...) named wrapper + at_zero + analyticAt + AnalyticOnNhd over Set.Ici 0 (PR feat: Step 610 — polymerFreeEnergy named wrapper (Mayer expansion, GJ §18.4) #1452)
  • Step 611: polymerFreeEnergy_continuousAt + _differentiableAt + _eq_mayerPartialSum_at_zero (PR feat: Step 611 — polymerFreeEnergy continuousAt + Mayer identity (Mayer expansion, GJ §18.4) #1453)
  • Step 612: freeEnergy_eq_polymerFreeEnergy — f = log 2 + (|E|/|ι|) log cosh + polymerFreeEnergy/|ι| (PR feat: Step 612 — freeEnergy = log 2 + (|E|/|ι|) log cosh + polymerFreeEnergy/|ι| (Mayer expansion, GJ §18.4) #1454)
  • Step 613: polymerFreeEnergy_tanh_analyticAt_beta / _J + _analyticOnNhd_beta_Ici_zero / _J_Ici_zero (under sign assumptions) (PR feat: Step 613 — polymerFreeEnergy β/J analyticity wrappers (Mayer expansion, GJ §18.4) #1455)
  • Step 614: mayerPartialSum_two — = ∑_P t^|P| - (1/2) ∑_{(P,Q) incompat} t^|P|·t^|Q| (N=2 explicit Mayer truncation) (PR feat: Step 614 — mayerPartialSum G 2 t explicit formula (Mayer expansion, GJ §18.4) #1456)
  • Step 615: ursellCoefficient_abs_le_choose_pow_div_factorial — uniform |ϕ^T(ω)| ≤ 2^(n choose 2) / n! (PR feat: Step 615 — uniform Ursell bound (Mayer expansion, GJ §18.4) #1457)
  • Step 616: freeEnergy_eq_polymerFreeEnergy_ferromagnetic — ferromagnetic version of Step 612 (PR feat: Step 616 — freeEnergy_eq_polymerFreeEnergy ferromagnetic (Mayer expansion, GJ §18.4) #1458)
  • Step 617: polymerFreeEnergy_eq_mayerPartialSum_at_betaJ_zero + β=0 / J=0 specialisations (PR feat: Step 617 — polymerFreeEnergy = mayerPartialSum at β·J=0 (Mayer expansion, GJ §18.4) #1459)
  • Step 618: mayer_identity_of_no_polymers — Mayer identity polymerFreeEnergy = mayerPartialSum at every t when allPolymers G = ∅ (both = 0) (PR feat: Step 618 — Mayer identity for empty-polymer graph (Mayer expansion, GJ §18.4) #1460)
  • Step 619: mayer_identity_of_no_polymers_tanh — tanh-form restatement of Step 618 (PR feat: Step 619 — Mayer identity tanh form for empty-polymer (Mayer expansion, GJ §18.4) #1461)
  • Step 620: allPolymers_eq_empty_of_edgeFinset_empty + mayer_identity_of_edgeFinset_empty — concrete edgeless graph case (PR feat: Step 620 — allPolymers = ∅ when no edges (Mayer expansion, GJ §18.4) #1462)
  • Step 621: polymerFreeEnergy_eq_zero_of_no_polymers + mayerPartialSum_eq_zero_of_no_polymers (PR feat: Step 621 — no-polymer zero extracts (Mayer expansion, GJ §18.4) #1463)
  • Step 622: mayer_identity_of_edgeFinset_empty_tanh — lift to tanh form (PR feat: Step 622 — edgeless Mayer identity tanh form (Mayer expansion, GJ §18.4) #1464)
  • Step 623: polymerFreeEnergy_eq_zero_of_edgeFinset_empty + mayerPartialSum_eq_zero_of_edgeFinset_empty (PR feat: Step 623 — polymerFreeEnergy = 0 for edgeless (Mayer expansion, GJ §18.4) #1465)
  • Step 624: freeEnergy_eq_log_two_at_betaJ_zero — f = log 2 at β·J=0 trivial slice (PR feat: Step 624 — freeEnergy = log 2 at β·J=0 (Mayer expansion, GJ §18.4) #1466)
  • Step 625: polymerFreeEnergy_hasDerivAt — explicit log-derivative formula via vdPolymerFamilies_sum_hasDerivAt (PR feat: Step 625 — polymerFreeEnergy HasDerivAt (Mayer expansion, GJ §18.4) #1467)
  • Step 626: polymerFreeEnergy_differentiableOn_Ici_zero — DifferentiableOn over [0,∞) (PR feat: Step 626 — polymerFreeEnergy DifferentiableOn (Set.Ici 0) (Mayer expansion, GJ §18.4) #1468)
  • Step 627: polymerFreeEnergy_continuousOn_Ici_zero — ContinuousOn over [0,∞) (PR feat: Step 627 — polymerFreeEnergy ContinuousOn (Set.Ici 0) (Mayer expansion, GJ §18.4) #1469)
  • Step 628: mayerPartialSum_continuousOn + _differentiableOn (PR feat: Step 628 — mayerPartialSum restriction wrappers (Mayer expansion, GJ §18.4) #1470)
  • Step 629: vdPolymerFamilies_sum_le_one_plus_pow_of_nonneg — generic vdSum G t ≤ (1+t)^|E| for t ≥ 0 (PR feat: Step 629 — vdPolymerFamilies_sum ≤ (1+t)^|E| (Mayer expansion, GJ §18.4) #1471)
  • Step 630: polymerFreeEnergy_le_card_log_one_plus_of_nonneg — polymerFreeEnergy G t ≤ |E|·log(1+t) for t ≥ 0 (PR feat: Step 630 — polymerFreeEnergy ≤ |E|·log(1+t) (Mayer expansion, GJ §18.4) #1472)
  • Step 631: vdPolymerFamilies_sum_sandwich_of_nonneg + polymerFreeEnergy_sandwich_of_nonneg (sandwich bounds for t ≥ 0) (PR feat: Step 631 — vdSum / polymerFreeEnergy sandwich for t ≥ 0 (Mayer expansion, GJ §18.4) #1473)
  • Step 632: polymerFreeEnergy_tanh_sandwich — tanh-form sandwich under 0 ≤ β·J (PR feat: Step 632 — polymerFreeEnergy sandwich tanh form (Mayer expansion, GJ §18.4) #1474)
  • Step 633: vdPolymerFamilies_sum_monotoneOn_Ici_zero + polymerFreeEnergy_monotoneOn_Ici_zero (PR feat: Step 633 — vdSum / polymerFreeEnergy monotone in t (Mayer expansion, GJ §18.4) #1475)
  • Step 634: polymerFreeEnergy_le_card_mul_of_nonneg — sharper bound polymerFreeEnergy ≤ |E|·t for t ≥ 0 (PR feat: Step 634 — polymerFreeEnergy ≤ |E|·t under t ≥ 0 (Mayer expansion, GJ §18.4) #1476)
  • Step 635: polymerFreeEnergy_tanh_le_card_mul — tanh-form sharper bound (PR feat: Step 635 — polymerFreeEnergy ≤ |E|·tanh(β·J) (Mayer expansion, GJ §18.4) #1477)
  • Step 636: polymerFreeEnergy_tanh_sandwich_ferromagnetic + _le_card_mul_ferromagnetic (PR feat: Step 636 — polymerFreeEnergy ferromagnetic wrappers (Mayer expansion, GJ §18.4) #1478)
  • Step 637: mayerExpansionTerm_one_nonneg_of_nonneg + _two_nonpos_of_nonneg — sign analysis at n=1, 2 (PR feat: Step 637 — Mayer term sign analysis at n=1, n=2 (Mayer expansion, GJ §18.4) #1479)
  • Step 638: mayerPartialSum_succ — recurrence mayerPartialSum (N+1) = mayerPartialSum N + mayerExpansionTerm (N+1) (PR feat: Step 638 — mayerPartialSum recurrence (Mayer expansion, GJ §18.4) #1480)
  • Step 639: vdPolymerFamilies_sum_at_one — = |vdCompatiblePolymerFamilies G| at t=1 (PR feat: Step 639 — vdPolymerFamilies_sum at t=1 (Mayer expansion, GJ §18.4) #1481)
  • Step 640: polymerFreeEnergy_at_one — = log |vdCompatiblePolymerFamilies G| at t=1 (PR feat: Step 640 — polymerFreeEnergy at t=1 (Mayer expansion, GJ §18.4) #1482)
  • Step 641: mayerPartialSum_one_at_one — = |allPolymers G| at t=1 (PR feat: Step 641 — mayerPartialSum G 1 t at t=1 (Mayer expansion, GJ §18.4) #1483)
  • Step 642: polymerFreeEnergy_le_card_log_two_of_le_one — polymerFreeEnergy ≤ |E|·log 2 for 0 ≤ t ≤ 1 (PR feat: Step 642 — polymerFreeEnergy ≤ |E|·log 2 (Mayer expansion, GJ §18.4) #1484)
  • Step 643: polymerFreeEnergy_tanh_le_card_log_two — tanh form of Step 642 (PR feat: Step 643 — polymerFreeEnergy_tanh ≤ |E|·log 2 (Mayer expansion, GJ §18.4) #1485)
  • Step 644: polymerFreeEnergy_tanh_le_card_log_two_ferromagnetic (PR feat: Step 644 — polymerFreeEnergy_tanh ≤ |E|·log 2 ferromagnetic (Mayer expansion, GJ §18.4) #1486)
  • Step 645: polymerFreeEnergy_tanh_double_bound — combine Steps 635, 643 (PR feat: Step 645 — polymerFreeEnergy_tanh double bound (Mayer expansion, GJ §18.4) #1487)
  • Step 646: mayerExpansionTerm_eq_mayerPartialSum_diff (PR feat: Step 646 — mayerExpansionTerm = mayerPartialSum diff (Mayer expansion, GJ §18.4) #1488)
  • Step 647: polymerSeqIncompatibilityGraph_const_polymer = ⊤ — constant polymer sequence gives K_n (PR feat: Step 647 — polymerSeqIncompatibilityGraph const = ⊤ (Mayer expansion, GJ §18.4) #1489)
  • Step 648: polymerSeqIncompatibilityGraph_const_polymer_adj — adjacency of distinct indices (PR feat: Step 648 — polymerSeqIncompatibilityGraph const polymer edgeFinset (Mayer expansion, GJ §18.4) #1490)
  • Step 649: polymerFreeEnergy_le_of_le_of_nonneg (PR feat: Step 649 — polymerFreeEnergy_le_of_le (Mayer expansion, GJ §18.4) #1491)
  • Step 650 (75-PR Mayer infrastructure milestone): polymerFreeEnergy_le_of_le_strict_form (PR feat: Step 650 — Mayer identity tanh form named wrapper milestone (Mayer expansion, GJ §18.4) #1492)
  • Step 651: mayer_identity_of_trivial — combine β·J=0 and no-polymers cases (PR feat: Step 651 — Mayer identity disjunctive trivial condition (Mayer expansion, GJ §18.4) #1493)
  • Step 652: mayer_identity_at_J_zero_polymer_free_energy + _beta_zero specialisations (PR feat: Step 652 — Mayer identity disjunctive specialisations (Mayer expansion, GJ §18.4) #1494)
  • Step 653: mayer_identity_at_either_zero_polymer_free_energy (PR feat: Step 653 — connectedSpanningEdgeSubsets for singleton (Mayer expansion, GJ §18.4) #1495)
  • Step 654: mayerPartialSum_zero_le_polymerFreeEnergy (PR feat: Step 654 — mayerPartialSum 0 ≤ polymerFreeEnergy (Mayer expansion, GJ §18.4) #1496)
  • Step 655: mayerPartialSum_zero_tanh_le_polymerFreeEnergy — tanh form (PR feat: Step 655 — mayerPartialSum 0 ≤ polymerFreeEnergy tanh form (Mayer expansion, GJ §18.4) #1497)
  • Step 656: mayerPartialSum_zero_tanh_le_polymerFreeEnergy_ferromagnetic (PR feat: Step 656 — mayerPartialSum_zero_tanh ferromagnetic (Mayer expansion, GJ §18.4) #1498)

§18.5 — Convergence of polymer-family sum (Steps 549-554)

• Step 549: VD polymer-family sum ≥ 1
• Step 550: VD polymer-family sum ≤ 2^|E|
• Step 551: trivial sandwich 1 ≤ ∑ ≤ 2^|E| (vdPolymerFamilies_sum_sandwich)
• Step 552: sharper VD polymer-family sum ≤ (1+tanh(β·J))^|E|
• Step 553/554: sharper sandwich 1 ≤ ∑ ≤ (1+tanh(β·J))^|E| (vdPolymerFamilies_sum_sandwich_sharp)
• Sharper polymer-density / radius-of-convergence estimates (not yet started)

§18.6 — Analyticity / regularity (Steps 555-564, DONE at h=0)

• Step 555: vdPolymerFamilies_sum_continuous — Continuous (fun t => ∑_Γ ∏ t^|P|) (PR feat: Step 555 — polymer-family sum continuous in t (GJ §18.6) #1397)
• Step 556: vdPolymerFamilies_sum_tanh_continuous_beta / _J + project-local continuous_real_tanh (PR feat: Step 556 — polymer-family sum continuous in β via tanh (GJ §18.6) #1398)
• Step 557: partitionFunction_continuous_beta_h_zero / _J_h_zero via polymer expansion (PR feat: Step 557 — Z continuous in β via polymer expansion (GJ §18.6) #1399)
• Step 558: vdPolymerFamilies_sum_differentiable (polynomial in t) (PR feat: Step 558 — polymer-family sum Differentiable in t (GJ §18.6) #1400)
• Step 559: vdPolymerFamilies_sum_tanh_differentiable_beta / _J + project-local differentiable_real_tanh (PR feat: Step 559 — polymer-family sum Differentiable in β/J via tanh (GJ §18.6) #1401)
• Step 560: partitionFunction_differentiable_beta_h_zero / _J_h_zero via polymer expansion (PR feat: Step 560 — Z Differentiable in β/J via polymer expansion (GJ §18.6) #1402)
• Step 561: vdPolymerFamilies_sum_analyticAt (polymer sum is AnalyticAt ℝ in t; via Finset.induction + helper analyticAt_prod_pow) (PR feat: Step 561 — polymer-family sum AnalyticAt in t (GJ §18.6) #1403)
• Step 562: vdPolymerFamilies_sum_tanh_analyticAt_beta / _J + project-local analyticAt_real_tanh (PR feat: Step 562 — polymer-family sum AnalyticAt in β/J via tanh (GJ §18.6) #1404)
• Step 563: partitionFunction_analyticAt_beta_h_zero / _J_h_zero via polymer expansion (PR feat: Step 563 — Z AnalyticAt in β/J via polymer expansion (GJ §18.6) #1405)
• Step 564: §18.6 capstone — freeEnergy_analyticAt_beta_h_zero / _J_h_zero: f = (1/|ι|) · log Z is AnalyticAt ℝ in β/J at every point at h=0, via AnalyticAt.log + partitionFunction_pos (PR feat: Step 564 — free energy AnalyticAt in β/J via polymer expansion (GJ §18.6) #1406)
• Step 565: §18.6 global form — partitionFunction_analyticOnNhd_beta_h_zero / _J_h_zero and freeEnergy_analyticOnNhd_beta_h_zero / _J_h_zero: per-point AnalyticAt upgraded to AnalyticOnNhd ℝ _ Set.univ (PR feat: Step 565 — freeEnergy AnalyticOnNhd over univ at h=0 (GJ §18.6) #1407)
• Step 575: vdPolymerFamilies_sum_hasDerivAt — explicit polynomial derivative formula ∑_Γ ∑_{Q ∈ Γ} (∏_{P ∈ Γ.erase Q} t^|P|) · ((|Q|:ℝ)·t^(|Q|-1)) via HasDerivAt.fun_finset_prod + hasDerivAt_pow + HasDerivAt.fun_sum (PR feat: Step 575 — explicit polynomial derivative for polymer-family sum (GJ §18.6) #1417)
• General-h AnalyticAt + AnalyticOnNhd + jointly in (β, J, h) (PRs feat: freeEnergy AnalyticAt in β / J at general h (§18.6 capstone, Issue #1499) #1528-feat: freeEnergy jointly Continuous + Differentiable in (β, J, h) (§18.6, Issue #1499) #1533): direct sum-of-exp proof (bypasses polymer expansion). Z and freeEnergy are jointly real-analytic in (β, J, h) ∈ ℝ³; per-direction Continuous / Differentiable already exist; full joint Continuous / Differentiable / AnalyticAt / AnalyticOnNhd ℝ _ Set.univ now established.

§18.7 — Correlation decay

• Step 566: foundation — correlation_high_temp_h_zero_le_numerator (under 0 ≤ β·J, ⟨σ_A⟩ ≤ ∑_{X : ∂X = A} tanh(β·J)^|X|; reduces capstone to numerator-only estimate) (PR feat: Step 566 — correlation ≤ FV (3.46) numerator at h=0 (GJ §18.7 foundation) #1408)
• Step 567: foundation — evenSubgraph_pair_boundary_card_pos (every X in numerator filter for A = {i,j} satisfies 1 ≤ |X|, parity argument at v = i) (PR feat: Step 567 — pair-numerator |X| ≥ 1 for §18.7 (GJ §18.7 foundation) #1409)
• Step 568: weak upper bound — correlation_high_temp_h_zero_at_pair_le_two_pow_edges_mul_tanh (under 0 ≤ β·J, ⟨σ_iσ_j⟩ ≤ 2^|E| · tanh(β·J); companion to Step 386 lower bound tanh / 2^|E| ≤ ⟨σ_iσ_j⟩) (PR feat: Step 568 — pair correlation ≤ 2^|E|·tanh(β·J) at h=0 (GJ §18.7 weak upper bound) #1410)
• Step 569: foundation — evenSubgraph_pair_boundary_exists_edge_incident_to (∂X = {i,j} → ∃ e ∈ X, i ∈ e; parity at v=i forces filter card to be odd ≥ 1) (PR feat: Step 569 — ∂X = {i,j} → ∃ e ∈ X, i ∈ e (GJ §18.7 foundation) #1411)
• Step 570: foundation — filter_mem_card_erase (parity transition: (X.filter (v ∈ ·)).card = ((X.erase e).filter (v ∈ ·)).card + (if v ∈ e then 1 else 0) for e ∈ X) (PR feat: Step 570 — filter_mem_card_erase parity transition (GJ §18.7 foundation) #1412)
• Step 571: foundation — evenSubgraph_pair_boundary_card_one_adj (when X.card = 1, ∂X = {i,j}, i ≠ j: X = {s(i,j)} and G.Adj i j; base case for inductive distance bound) (PR feat: Step 571 — pair-boundary card-1 case → G.Adj (GJ §18.7 foundation) #1413)
• Step 572: foundation — evenSubgraph_pair_boundary_erase_swap (parity transition: ∂X = {i,j} ∧ s(i,k) ∈ X ∧ k ∉ {i,j} → ∂(X.erase s(i,k)) = {k,j}; mod-2 case analysis on v) (PR feat: Step 572 — parity transition lemma evenSubgraph_pair_boundary_erase_swap (GJ §18.7) #1414)
• Step 573: graph-distance bound — evenSubgraph_pair_boundary_dist_le (∂X = {i,j} → G.dist i j ≤ X.card; strong induction on X.card building explicit G.Walk i j; combines Steps 567/569/572 + SimpleGraph.dist_le) (PR feat: Step 573 — graph-distance bound G.dist i j ≤ |X| for ∂X = {i,j} (GJ §18.7) #1415)
• Step 574: §18.7 capstone — correlation_high_temp_h_zero_at_pair_le_two_pow_edges_mul_tanh_pow_dist: under 0 ≤ β·J, ⟨σ_{i,j}⟩ ≤ 2^|E| · tanh(β·J)^{G.dist i j} (high-temperature exponential decay in graph distance; combines Steps 566+573 with pow_le_pow_of_le_one and Finset.sum_le_card_nsmul) (PR feat: Step 574 — §18.7 capstone: ⟨σ_iσ_j⟩ ≤ 2^|E|·tanh(β·J)^d(i,j) (GJ §18.7) #1416)
• Sharper / smaller-prefactor §18.7 bounds (deferred; current bound has 2^|E| prefactor which is loose)

References

• GJ Quantum Physics §18.4-§18.7
• Friedli-Velenik §3.7 (lattice high-temp expansion) and §5.7 (Pirogov-Sinai variant)
• Existing §18.3 work: partitionFunction_high_temp_expansion_h_zero_closed (FV (3.45)) in IsingModel/Conditioning.lean