docs: sync §18.4 / §18.6 status for PRs #1517-#1566 — #1344 - #1567
Merged
Conversation
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>
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>
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.
Summary
docs/index.md(§18.4 / §18.6) andtex/proof-guide.texcluster-expansion section up to date for the 44 PRs (feat: explicit convergence radius for Mayer log expansion (Mayer Phase A2, Issue #1499) #1517–feat: §18.4 polymerFreeEnergy tanh monotonicity in β / J GJ-命題-bundle #1566) merged in the 2026-05-03/04 session..self-local/docs/SESSION-RESUME.mdto reflect post-feat: §18.4 polymerFreeEnergy tanh monotonicity in β / J GJ-命題-bundle #1566 state.Per
CLAUDE.local.md公開ドキュメント同期 (絶対遵守), the prior 44 PRs left the public status table and proof guide partially out of sync. This PR closes that gap as a single batched documentation sync — splitting it per PR would multiply the unit needlessly.Part of #1344.
Plan
docs/index.md§18.4 row: append Phase B base cases (K_3, K_4, pathGraph 3–8, cycleGraph 3–7) plus polymerFreeEnergy / vdSum / ε iff·strict·sandwich theorem clusters with PR pointers.docs/index.md§18.6 row: append general-h capstone (β/J/h directions, joint, Λ-layer, correlation, gibbsExpectation) with PR pointers.tex/proof-guide.texcluster-expansion section: add paragraph blocks per theorem cluster..self-local/docs/SESSION-RESUME.md: refresh status.lake build(no Lean changes — should be a no-op),grep -rn "sorry" IsingModel/remains zero.Test plan
lake buildclean (no Lean changes; smoke test only)grep -rn "sorry" IsingModel/= 0tex/proof-guide.texreferences the new theorem clusters with edition + page🤖 Generated with Claude Code