feat: partitionFunctionΛ regularity at general h (Λ-layer wrappers, §18.6, Issue #1499) - #1541
Merged
Merged
Conversation
…18.6, Issue #1499) Add Λ-layer wrappers in `IsingModel/AmbientLattice/Analyticity.lean` for the per-direction Continuous + Differentiable theorems from PR #1540: - `partitionFunctionΛ_continuous_beta_general_h` and `_differentiable_beta_general_h` - `partitionFunctionΛ_continuous_J_general_h` and `_differentiable_J_general_h` - `partitionFunctionΛ_continuous_h` and `_differentiable_h` Each is a thin wrapper around the corresponding theorem on `inducedGraph G Λ`. Completes the regularity hierarchy for partitionFunctionΛ at general h. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
phasetr
marked this pull request as ready for review
May 2, 2026 21:15
phasetr
added a commit
that referenced
this pull request
May 4, 2026
Brings the public progress table (`docs/index.md`) and proof guide (`tex/proof-guide.tex`) up to date with the 44 PRs (#1517-#1566) merged in the 2026-05-03/04 session. §18.4 row: appends Phase B base cases (K_3, K_4, pathGraph 3-8, cycleGraph 3-7) and the polymerFreeEnergy / vdSum / ε iff·strict· sandwich theorem clusters with PR pointers. The general K_n formula and n ≥ 9 cases remain blocked on chromatic-polynomial / matrix-tree-theorem machinery not yet in Mathlib. §18.6 row: appends the general-h capstone (β/J/h directions, joint, Λ-layer, correlation, gibbsExpectation) — PRs #1528-#1541. `tex/proof-guide.tex`: adds a new section "Cluster (polymer / Mayer) expansion (§18.4-§18.7)" summarising the polymer-family identity, Mayer/Ursell infrastructure (Steps 576-615), Phase B base cases, polymer-free-energy bounds and characterisations, the §18.6 general-h analyticity capstone, and the §18.7 high-temperature exponential-decay result. No Lean source changes. Part of #1344. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
phasetr
added a commit
that referenced
this pull request
May 4, 2026
* chore: open doc-sync PR for #1517-#1566 (Part of #1344) * docs: sync §18.4 / §18.6 / §18.7 status for PRs #1517-#1566 Brings the public progress table (`docs/index.md`) and proof guide (`tex/proof-guide.tex`) up to date with the 44 PRs (#1517-#1566) merged in the 2026-05-03/04 session. §18.4 row: appends Phase B base cases (K_3, K_4, pathGraph 3-8, cycleGraph 3-7) and the polymerFreeEnergy / vdSum / ε iff·strict· sandwich theorem clusters with PR pointers. The general K_n formula and n ≥ 9 cases remain blocked on chromatic-polynomial / matrix-tree-theorem machinery not yet in Mathlib. §18.6 row: appends the general-h capstone (β/J/h directions, joint, Λ-layer, correlation, gibbsExpectation) — PRs #1528-#1541. `tex/proof-guide.tex`: adds a new section "Cluster (polymer / Mayer) expansion (§18.4-§18.7)" summarising the polymer-family identity, Mayer/Ursell infrastructure (Steps 576-615), Phase B base cases, polymer-free-energy bounds and characterisations, the §18.6 general-h analyticity capstone, and the §18.7 high-temperature exponential-decay result. No Lean source changes. Part of #1344. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> * docs: correct §18.6 h-direction theorem names + #1557 PR mapping Codex cross-check found two issues: 1. docs/index.md §18.6 row used `freeEnergy_analyticAt_h_general_h` but the actual theorem in source is named `freeEnergy_analyticAt_h` (no `_general_h` suffix); the global form is `freeEnergy_analyticOnNhd_h`. The β/J directions correctly use the `_general_h` suffix. 2. tex/proof-guide.tex §18.4 cluster-expansion paragraph cited PR #1557 next to the prose `vdPolymerFamilies_sum = 1 iff no polymers`, but PR #1557 is `_eq_one_iff_eps_eq_zero` and `_gt_one_iff_eps_pos` (the ε-based iff pair). Replaced the prose with the explicit theorem names. Part of #1344. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> --------- Co-authored-by: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
phasetr
added a commit
that referenced
this pull request
May 4, 2026
Lifts eight abstract partitionFunction _h_zero regularity theorems to all 4 volume layers (Λ, along-ex, ℤ^d Λ, ℤ^d along-ex): - `partitionFunction_continuous_beta_h_zero` - `partitionFunction_continuous_J_h_zero` - `partitionFunction_differentiable_beta_h_zero` - `partitionFunction_differentiable_J_h_zero` - `partitionFunction_analyticAt_beta_h_zero` - `partitionFunction_analyticAt_J_h_zero` - `partitionFunction_analyticOnNhd_beta_h_zero` - `partitionFunction_analyticOnNhd_J_h_zero` Bundle contents: 32 new theorems (8 abstracts × 4 layers). These provide polymer-expansion-derived h_zero regularity of `Z(J, 0, β)` in β / J at every volume layer, complementing the existing general-h wrappers (PR #1541). `docs/index.md` §18.6 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) <noreply@anthropic.com>
phasetr
added a commit
that referenced
this pull request
May 4, 2026
…undle (#1608) * wip: §18.6 partitionFunction h_zero regularity 4-layer wraps * feat: §18.6 partitionFunction h_zero regularity 4-layer wraps Lifts eight abstract partitionFunction _h_zero regularity theorems to all 4 volume layers (Λ, along-ex, ℤ^d Λ, ℤ^d along-ex): - `partitionFunction_continuous_beta_h_zero` - `partitionFunction_continuous_J_h_zero` - `partitionFunction_differentiable_beta_h_zero` - `partitionFunction_differentiable_J_h_zero` - `partitionFunction_analyticAt_beta_h_zero` - `partitionFunction_analyticAt_J_h_zero` - `partitionFunction_analyticOnNhd_beta_h_zero` - `partitionFunction_analyticOnNhd_J_h_zero` Bundle contents: 32 new theorems (8 abstracts × 4 layers). These provide polymer-expansion-derived h_zero regularity of `Z(J, 0, β)` in β / J at every volume layer, complementing the existing general-h wrappers (PR #1541). `docs/index.md` §18.6 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) <noreply@anthropic.com> --------- Co-authored-by: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
phasetr
added a commit
that referenced
this pull request
May 4, 2026
…along-ex + ℤ^d wraps Lifts eight abstract regularity theorems to the missing along-exhaustion + ℤ^d (Λ + along-ex) layers (Λ-layer wraps already exist via PR #1541, #1533): - `partitionFunction_continuous_beta_general_h` - `partitionFunction_continuous_J_general_h` - `partitionFunction_differentiable_beta_general_h` - `partitionFunction_differentiable_J_general_h` - `partitionFunction_continuous_h` - `partitionFunction_differentiable_h` - `freeEnergy_continuous_joint` - `freeEnergy_differentiable_joint` Bundle contents: 24 new theorems (8 abstracts × 3 missing layers). `docs/index.md` §18.6 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) <noreply@anthropic.com>
phasetr
added a commit
that referenced
this pull request
May 4, 2026
…along-ex + ℤ^d wraps GJ-命題-bundle (#1611) * wip: §18.6 partitionFunction/freeEnergy continuous/differentiable along-ex + ℤ^d wraps * feat: §18.6 partitionFunction/freeEnergy Continuous + Differentiable along-ex + ℤ^d wraps Lifts eight abstract regularity theorems to the missing along-exhaustion + ℤ^d (Λ + along-ex) layers (Λ-layer wraps already exist via PR #1541, #1533): - `partitionFunction_continuous_beta_general_h` - `partitionFunction_continuous_J_general_h` - `partitionFunction_differentiable_beta_general_h` - `partitionFunction_differentiable_J_general_h` - `partitionFunction_continuous_h` - `partitionFunction_differentiable_h` - `freeEnergy_continuous_joint` - `freeEnergy_differentiable_joint` Bundle contents: 24 new theorems (8 abstracts × 3 missing layers). `docs/index.md` §18.6 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) <noreply@anthropic.com> --------- Co-authored-by: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Part of #1499. Λ-layer wrappers for PR #1540.