feat: §18.6 mayerPartialSum tanh β/J 4-layer wraps (32 thm) — #1344 - #1583
Merged
Conversation
Lifts the eight abstract β/J regularity statements for
`mayerPartialSum ∘ tanh ∘ (·*J)` and `(β*·)` to all four volume
layers:
- `mayerPartialSum_tanh_{continuous,differentiable}_{beta,J}` (Steps 594, 595)
- `mayerPartialSum_tanh_{analyticAt,analyticOnNhd}_{beta,J}` (Step 596)
Bundle contents (32 new theorems): 8 abstracts × 4 layers
(Λ-direct + along-exhaustion + ℤ^d Λ-direct + ℤ^d along-exhaustion).
Each is a thin direct-instantiation wrapper of the abstract on the
corresponding `inducedGraph` subgraph.
`docs/index.md` §18.5 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>
…eedback Codex flagged that PR #1583's tex paragraph header used §18.6 while docs/index.md attaches the wrappers to the §18.5 inventory row. Aligned both to §18.5. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
phasetr
marked this pull request as ready for review
May 4, 2026 11:56
phasetr
added a commit
that referenced
this pull request
Jul 27, 2026
…ed by this deletion The five deleted zero-consumer modules carried wrappers that four count-based sentences in the docs/index.md §18.5 row still counted. Measured on the working tree (declaration extraction over every tracked IsingModel/*.lean, handling the line-broken `theorem\n<name>` spelling), the four families now read: PR #1583 mayerPartialSum tanh beta/J regularity 32 (8/8/8/8) -> 24 (8 Lambda / 8 along-ex / 0 Z^d Lambda / 8 Z^d along-ex) PR #1592 Mayer identity edge-cases 20 (5/5/5/5) -> 15 (5 / 5 / 5 / 0 Z^d along-ex) PR #1593 basic identities (at_zero/at_one) 32 (8/8/8/8) -> 27 (8 / 8 / 8 / 3 Z^d along-ex) PR #1604 polymerFreeEnergy/vdSum tanh ferromagnetic iff family 36 (9/9/9/9) -> 31 (9 / 9 / 9 / 4 Z^d along-ex) "at all 4 layers" is replaced by the surviving layer structure (three layers for the first two families, four layers with a partial Z^d along-exhaustion layer for the other two), and the "now live in / remain in" module pointers in the same sentences are repointed at the modules that actually hold the survivors: #1583 -> AnalyticityLambdaMayer, SpecialCases/MayerVdRegularityTanh(+Differentiable), SpecialCases/MayerAnalyticity, Concrete/MayerVdRegularityTanhAlongEx, Concrete/MayerAnalyticityTanhAlongEx #1592 -> Concrete/MayerTrivialCasesLambdaIdentity (was MayerTrivialCases) #1593 -> Concrete/MayerBasicIdentities + MayerBasicIdentitiesMayerExpansionTerm, Concrete/MayerBasicIdentitiesAlongExMayerExpansionTerm #1604 -> Concrete/MayerTanhFerromagneticIff + MayerTanhFerromagneticIffVdSum, Concrete/MayerTanhFerromagneticIffAlongExTail No deleted module path is cited, so no dangling citation is introduced. docs/index.md is the only file touched. citation audit: PASS, findings (gating) 960 unchanged, ratchet 0 cleared / 0 new, coverage OK (RESOLVED 1962 -> 1968, AMBIGUOUS and BASENAME_ONLY unchanged). Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
phasetr
added a commit
that referenced
this pull request
Jul 27, 2026
…e batch 1) (#4747) Deletes five `IsingModel/Concrete/LatticeGraphCorrelation/` modules (496 lines, 23 theorems) whose declarations have no consumer anywhere in the repository, and removes the five corresponding import lines from their sole importer, `IsingModel/Concrete/LatticeGraphCorrelation/Umbrella/MagnetizationAndMayer.lean`. | Module | Lines | Theorems | |---|---|---| | `MayerTanhFerromagneticIffAlongEx.lean` | 117 | 5 | | `MayerTrivialCasesAlongExIdentity.lean` | 108 | 5 | | `MayerVdRegularityTanh.lean` | 100 | 4 | | `MayerBasicIdentitiesAlongEx.lean` | 86 | 5 | | `MayerAnalyticityTanh.lean` | 85 | 4 | All five consist entirely of thin `IsingModel.latticeGraph d` pass-throughs to `Ambient.*` lemmas that are untouched by this PR. ## Declaration-level double-check (run for this PR, not inherited) `git grep -F` over the whole repository for each of the 23 declaration names, excluding the five files being deleted: * 22 of 23 names: **0 hits**. * `mayerPartialSumAlongExhaustion_latticeGraph_one`: **3 hits**, all superstring matches on the distinct surviving theorem `mayerPartialSumAlongExhaustion_latticeGraph_one_at_one` (`HighTemperatureCapstonesAlongEx.lean:71` plus two doc comments). That theorem's proof term is `Ambient.mayerPartialSumAlongExhaustion_one_at_one`, i.e. the ambient lemma, so it does not depend on anything deleted here. Verified by reading the declaration body, not by the grep count alone. The same grep was run for the five module basenames. Hits outside the deleted files fall into two groups, checked individually: * `IsingModel/AmbientLattice/SpecialCases/**` — these name the *ambient* modules `MayerVdRegularityTanh` / `MayerVdRegularityTanhExpansionTerm`, which are different files under a different directory and are not deleted, plus one pre-existing historical note in `AmbientLattice/SpecialCases/MayerAnalyticity.lean` about ambient children deleted in an earlier PR. Left unchanged. * `IsingModel/Concrete/LatticeGraphCorrelation/**` — doc-comment pointers at the modules deleted here. Fixed in this PR (next section). ### Elaborated-graph cross-check (`--lean`, condition (i) of #4746) A text scan cannot see `simp`-set usage, tactic-generated references or `open`-shortened names, so #4746 requires the elaborated graph to be consulted as well. That run has to be made on the **pre-deletion** tree: `scripts/audit/DumpDeps.lean` reads the environment of `import IsingModel`, and a declaration that has already been deleted trivially has no consumers there, so running it on this branch would be vacuous. Run instead in a green checkout of the merge base `2aa350e3` (`lake build` → `Build completed successfully (5040 jobs)`, exit 0), with the same 23 declaration names as candidates: ``` python3 scripts/dead_candidate_scan.py <file with the 23 names> --lean ``` ``` --lean cross-check: 23 candidate(s) compared against the elaborated graph; no consumer seen by Lean was missed on a safe-to-delete verdict ``` `-- safe-to-delete: 23 --`, exit 0. All 23 are compared, not just a sample, and Lean reports no consumer that the text scan did not already account for; since the text scan attributes no consumer to any of the 23, the elaborated graph likewise shows none. `docs/index.md`, `tex/proof-guide.tex`, `README.md` and `test/**` contain **no** occurrence of any of the five basenames or any of the 23 declaration names. That exact-name grep is not sufficient on its own: `docs/index.md` also describes these wrappers *in aggregate*, by family and by count, and those count-based sentences name no declaration and no module basename, so they are invisible to the grep above while still being falsified by the deletion. Four such sentences were found and corrected in commit `f2c1590a` (section "Count-based docs claims retracted" below). `tex/proof-guide.tex`, `README.md` and `test/**` remain unmodified. ## Doc-comment closure in surviving siblings (addition to the design) The design for this batch checked `docs/`, `tex/`, `README.md` and `test/` for inbound references and found none. It did not check `/-! -/` doc comments in sibling `.lean` modules, and those did carry pointers at the five modules. Deleting the files without touching them would have left dangling module references of exactly the kind PRs #4705/#4708/#4710/#4711/#4720 cleaned up, so **ten** surviving modules are updated here. (An earlier revision of this body, and the message of commit `bec042d1`, said "eight". That count was wrong: `git diff --name-only --diff-filter=M 2aa350e..HEAD -- 'IsingModel/Concrete/LatticeGraphCorrelation/*.lean'` minus `Umbrella/` returns 10 paths, and the three bullets below already sum to 4 + 1 + 5 = 10. `bec042d1` is left unamended; the correction of record is in the message of commit `16861a8f`.) * `MayerTanhFerromagneticIff.lean`, `MayerBasicIdentities.lean`, `MayerAnalyticity.lean`, `MayerVdRegularity.lean` — "Moved:" blocks restated against the modules where the surviving wrappers actually live. Every count in the new text was re-derived by counting declarations in the target files (4 in `MayerTanhFerromagneticIffAlongExTail.lean`; 3 in `MayerBasicIdentitiesAlongExMayerExpansionTerm.lean`; 4+4 in `MayerAnalyticityTanhAlongEx.lean` / `MayerAnalyticityTanhExpansionTerm.lean`; 4+4+4 in `MayerVdRegularityTanhAlongEx.lean` / `MayerVdRegularityTanhExpansionTermLambda.lean` / `MayerVdRegularityTanhExpansionTermAlongEx.lean`). * `MayerTrivialCases.lean` — the "Moved:" block named five wrappers that all cease to exist here, so the block is removed rather than repointed. * `MayerTanhFerromagneticIffAlongExTail.lean`, `MayerBasicIdentitiesAlongExMayerExpansionTerm.lean`, `MayerAnalyticityTanhAlongEx.lean`, `MayerAnalyticityTanhExpansionTerm.lean`, `MayerVdRegularityTanhAlongEx.lean` — provenance sentences of the form "extracted from `X.lean`" / "names unchanged from the former `X` declarations" for a now-deleted `X`; the stale clause is dropped. Two follow-up checks were run after editing: (a) every module basename appearing in the new text resolves to exactly one tracked file, and (b) a repeat of the basename grep shows no remaining `Concrete/` reference to a deleted module. One side effect worth recording for later batches: `MayerVdRegularityTanh.lean` existed at two paths before this PR. After the deletion the ambient copy is the unique file with that basename, so bare-basename references in `AmbientLattice/SpecialCases/` become less ambiguous rather than more. While restating the `MayerVdRegularity.lean` blocks, the sentence "The earlier import path is preserved by re-importing the new child" was dropped. That module's import list is two lines (`IsingModel.AmbientLattice.SpecialCases.MayerVdRegularity` and `IsingModel.Lattice`), and a breadth-first walk of their transitive closure — 202 modules — reaches no `MayerVdRegularityPolymer*` module at all; the only importer of `Concrete.LatticeGraphCorrelation.MayerVdRegularityPolymer` in the tree is `Umbrella/MagnetizationAndMayer.lean`. The sentence therefore did not describe the file as it stands. The sentence occurred **twice** in that file. `bec042d1` dropped only the copy in the tanh-variant block; the copy in the `vdPolymerFamilies` block, verbatim identical and fourteen lines below, survived and was caught in review. Commit `16861a8f` removes it, on the same ground and by deletion rather than restatement. A third defect in the same file was caught in a later review pass and is fixed in commit `9fcb1e3b`: the `vdPolymerFamilies` block said the wrappers "now live in `...MayerVdRegularityPolymer`", naming **one** module and counting **12**, whereas counting declarations in the surviving files gives **14** across **four** — `MayerVdRegularityPolymer.lean` (3, Λ-direct in t), `MayerVdRegularityPolymerAlongEx.lean` (3, along-ex in t), `MayerVdRegularityPolymerTanh.lean` (4, Λ-direct tanh in β/J), `MayerVdRegularityPolymerTanhAlongEx.lean` (4, along-ex tanh in β/J). The 12 was inherited, not invented here: the #2045 commit message (`04893b8a`) also says 12, while `git show 04893b8 -- <the new child> | grep -c '^+theorem'` on that same commit returns 14 — two of the fourteen use the line-broken `theorem`-then-name spelling that a single-line regex misses, the same tokenisation trap already recorded for the `docs/index.md` counts above. The same commit also corrects the module header, which advertised `mayerExpansionTerm`, `vdPolymerFamilies_sum` and tanh forwarders that this module has not held since those splits; only the four `mayerPartialSumAlongExhaustion_latticeGraph_*` wrappers remain in it. The file's other three "Moved" notes were re-measured and stand as written (4 in `MayerVdRegularityLambda.lean`, 4 in `MayerVdRegularityExpansionTerm.lean`, 4 + 4 + 4 in the three tanh children). Every gate in the table below was re-run on `9fcb1e3b` with identical results: `lake build` 5,035 jobs exit 0, `grep -ci warning` = 0 and `grep -ci error` = 0 on the log, `audit_gate.py --full` PASS with the capstone axiom union unchanged, `citation_audit.py` PASS at gating findings 960 with ratchet 0 cleared / 0 new, `dead_candidate_scan.py --self-test` 94 OK and `--expect` PASS (18 rows), `lake exe GKSTest` all tests passed. ## Verification (all run on this branch) | Gate | Result | |---|---| | `lake build` | `Build completed successfully (5035 jobs)`, exit 0 | | warnings | `grep -ci warning` on the build log = **0** (the 2 pre-existing `info: ... Try this: ring_nf` lines are unchanged and are not warnings) | | errors | `grep -ci error` on the build log = **0** | | jobs | 5,040 → **5,035** | | tracked `IsingModel/*.lean` | 2,011 → **2,006** | | `scripts/audit_gate.py --full` | **PASS** — V1 no `axiom` decls (2,013 files), V2 no sorry/admit/native_decide (2,013 files), V3 13 capstones with observed axiom union exactly `{propext, Classical.choice, Quot.sound}`, V4 no Japanese text | | `sorry` / `admit` / `native_decide` | 4 word-boundary hits **within `IsingModel/`** (an earlier revision of this row called them repo-wide, which is the wrong scope label), all prose inside doc comments ("admit on the two-sided...", "no `sorry`", "`native_decide` sanity checks in the `test` library"); identical count on `main`. The same `git grep -nw` over *all* tracked `.lean` files returns **51**: the other 47 are the deliberate `native_decide` property/sentinel tests under `test/`, which is exactly the library `IsingModel/` is required to stay free of; over all tracked text files it returns **184** (`scripts/`, `tex/`, `docs/`, `.self-local/`). The gating instrument is `audit_gate.py` V2 in the row above, not this grep | | `python3 scripts/citation_audit.py` | **PASS**, gating findings **960** (unchanged), ratchet **0 cleared, 0 new**; per-class counts on this branch are tex RESOLVED=987/AMBIGUOUS=104/BASENAME_ONLY=125/SELFREF=4 (identical to `main`) and md RESOLVED=**1968**/AMBIGUOUS=107/BASENAME_ONLY=624/SELFREF=89, the single movement being the +6 newly cited existing modules that `f2c1590a` added to `docs/index.md` (an earlier revision of this row quoted the pre-`f2c1590a` md figure 1962 and called every class unchanged). Tracked `.lean` count moves 2,018 → 2,013, well above `MIN_TRACKED_LEAN=1800` | | `python3 scripts/dead_candidate_scan.py --self-test` | **94 tests OK** | | `python3 scripts/dead_candidate_scan.py --expect scripts/audit/dead_candidate_fixtures.tsv` | **PASS (18 rows)** | | `lake exe GKSTest` | **All tests passed** | | `tex/proof-guide.tex`, `README.md`, `test/**` | unmodified | | `docs/index.md` | modified in `f2c1590a` only, to retract four count-based claims the deletion falsified | The `tracked IsingModel/*.lean` row is a **git pathspec**, in which `*` matches across `/`; `git ls-files 'IsingModel/*.lean'` is therefore the full recursive count, 2,011 before and 2,006 after. The `**` spelling is the *narrower* one here: `git ls-files 'IsingModel/**/*.lean'` gives 1,972 before / 1,967 after, because it requires at least one intermediate directory and so drops the 39 modules sitting directly in `IsingModel/` (2,011 − 39 = 1,972; 2,006 − 39 = 1,967). An earlier revision of this description had the two globs the wrong way round, calling 2,011 the top-level-only figure and 1,972 the complete one. The 2,011 → 2,006 delta itself is unaffected and correct. ## Measured build time Machine: this worktree, with `main`'s `.lake` APFS-cloned in, so caches are warm. ### Warm full `lake build` | | wall | CPU (user+sys) | jobs | |---|---|---|---| | before, first run (page cache cold) | 11.47s | 9.21s | 5,040 | | before, steady state (2 runs) | 5.32s / 3.67s | 6.20s / 5.81s | 5,040 | | deletion applied (umbrella + downstream re-elaborated) | 4:35.85 | 313.4s | 5,035 | | after, steady state (3 runs) | 6.02s / 7.15s / 5.28s | 6.10s / 5.95s / 6.09s | 5,035 | The before/after difference here is **within run-to-run noise on this machine**, which is what the design predicted: a warm build only replays traces and does no elaboration, so it is not a measurement of what the deletion saves. It also is not evidence that the deletion saves nothing. The saving appears in a clean or CI build, which is not run here. ### Per-module process cost (what the deletion removes) Because the deleted modules have zero consumers, nothing downstream is rebuilt on their account, so the clean-build saving is the cost of the five `lean` processes that no longer run. Measured by restoring the five files to a scratch path and timing them (steady-state pass, mean over the 5 modules): | measurement | wall | CPU | |---|---|---| | `lake env lean <module>.lean` | 3.083s | 3.098s | | `lake env true` (lake wrapper only, 5 steady runs) | 0.673s | 0.674s | | **net `lean` process, per module** | **2.410s** | **2.424s** | This reproduces the design's independent measurement (2.37s wall / 2.41s CPU per module) to within about 2%. Against the **2.24s CPU/module** figure extrapolated in #4746, the measurement here is **2.42s CPU, i.e. +8.2%**; the design's separate run gave +7.6%. Both runs land slightly above the extrapolation, so the extrapolated constant looks mildly conservative, and for this batch of 5 that is **about 12.1s of CPU** removed from a clean build (5 × 2.424s). One sub-measurement did **not** reproduce. The design attributed ~92% of the per-module cost to fixed import loading and ~8% to the module's own elaboration, measured against import-only stubs. Here the import-only stubs took 3.167s wall / 3.092s CPU on average against the full modules' 3.083s / 3.098s, i.e. the own-elaboration component was below this machine's noise floor and could not be resolved. That is consistent with the component being small, but it is not an independent confirmation of the 92/8 split. The **wall-clock** saving in a clean build is *not* measured here. The 0.63s/module wall figure in the issue implies an effective parallelism of about 3.8 during a clean full build; establishing it would need a clean full build, which this PR does not run. Treat the wall column as extrapolation and the CPU column as measured. ## Count-based docs claims retracted (commit `f2c1590a`) The exact-name and basename greps above come back clean, but the `docs/index.md` §18.5 row also counts these wrapper families in aggregate ("N thin wrappers ... at all 4 layers"). Those sentences quote no declaration name and no module basename, so a name-keyed scan cannot see them. Four of them were falsified by this deletion. Measured on the working tree by extracting every `theorem` / `lemma` name from every tracked `IsingModel/*.lean` — including the line-broken spelling where `theorem` sits alone on its line and the name follows on the next, which a single-line regex misses (five of the deleted declarations and two survivors use it) — then bucketing by layer on the `AlongExhaustion` and `_latticeGraph` name components: | family | claim before | measured after | layer breakdown after (Λ-direct / along-ex / ℤ^d Λ-direct / ℤ^d along-ex) | |---|---|---|---| | `mayerPartialSum` tanh β/J regularity (PR #1583) | 32, "at all 4 layers" | **24**, 3 layers | 8 / 8 / **0** / 8 | | Mayer identity edge-cases (PR #1592) | 20, "at all 4 layers" | **15**, 3 layers | 5 / 5 / 5 / **0** | | Basic identities `at_zero` / `at_one` (PR #1593) | 32, "at all 4 layers" | **27**, 4 layers, one partial | 8 / 8 / 8 / **3** of 8 | | `polymerFreeEnergy` / `vdSum` tanh ferromagnetic iff (PR #1604) | 36, "at all 4 layers" | **31**, 4 layers, one partial | 9 / 9 / 9 / **4** of 9 | Reproduction (`$BASE` = `2aa350e3`, `$HEAD` = the tip of this branch): ``` for rev in $BASE $HEAD; do for f in $(git ls-tree -r --name-only $rev -- IsingModel | grep '\.lean$'); do git show $rev:$f | awk '/^(theorem|lemma)$/{getline;sub(/^ +/,"");print $1;next} /^(theorem|lemma) /{print $2}' done > decls-$rev.txt done sort decls-$BASE.txt > a.txt; sort decls-$HEAD.txt > b.txt; comm -23 a.txt b.txt grep -cE '^mayerPartialSum(_Λ|AlongExhaustion)(_latticeGraph)?_tanh_(continuous|differentiable|analyticAt|analyticOnNhd)_(beta|J)$' decls-*.txt grep -cE '^mayer_identity_of_(no_polymers|no_polymers_tanh|trivial|edgeFinset_empty|edgeFinset_empty_tanh)_(Λ|AlongExhaustion)(_latticeGraph)?$' decls-*.txt ``` `comm -23` returns the 23 deleted declarations, plus one `awk` tokenisation artefact — the bare word `at`, which comes from a prose line inside a deleted doc comment and is not a declaration. Alongside the numbers, the "now live in / remain in" module pointers inside the same four sentences were repointed at the modules that actually hold the survivors, each count re-derived from the files: | family | corrected residency | |---|---| | PR #1583 | `AmbientLattice/AnalyticityLambdaMayer.lean` (8) · `AmbientLattice/SpecialCases/MayerVdRegularityTanh.lean` (2) + `MayerVdRegularityTanhDifferentiable.lean` (2) + `MayerAnalyticity.lean` (4) · `Concrete/LatticeGraphCorrelation/MayerVdRegularityTanhAlongEx.lean` (4) + `MayerAnalyticityTanhAlongEx.lean` (4) | | PR #1592 | `AmbientLattice/AnalyticityLambdaMayerIdentity.lean` (5) · `AmbientLattice/SpecialCases/MayerTrivialCases.lean` (5) · `Concrete/LatticeGraphCorrelation/MayerTrivialCasesLambdaIdentity.lean` (5). The old text pointed the ℤ^d side at `Concrete/LatticeGraphCorrelation/MayerTrivialCases.lean`, which holds none of them | | PR #1593 | `AmbientLattice/AnalyticityLambdaBasicIdentities.lean` (8) · `AmbientLattice/SpecialCases/MayerBasicIdentities.lean` (8) · `Concrete/LatticeGraphCorrelation/MayerBasicIdentities.lean` (5) + `MayerBasicIdentitiesMayerExpansionTerm.lean` (3) · `Concrete/LatticeGraphCorrelation/MayerBasicIdentitiesAlongExMayerExpansionTerm.lean` (3, the surviving `mayerExpansionTerm` triple) | | PR #1604 | `AmbientLattice/AnalyticityLambdaTanhFerroIff.lean` (9) · `AmbientLattice/SpecialCases/MayerTanhFerromagneticIff.lean` (9) · `Concrete/LatticeGraphCorrelation/MayerTanhFerromagneticIff.lean` (5) + `MayerTanhFerromagneticIffVdSum.lean` (4) · `Concrete/LatticeGraphCorrelation/MayerTanhFerromagneticIffAlongExTail.lean` (4) | No path of a deleted module is cited in the new text, so no dangling citation is created. `python3 scripts/citation_audit.py` after the edit: **PASS**, gating findings **960** (unchanged), ratchet **0 cleared / 0 new**, coverage OK. The only class movement is `docs/index.md` RESOLVED 1962 → 1968 (+6 newly cited existing modules); AMBIGUOUS (107), BASENAME_ONLY (624) and SELFREF (89) are unchanged, as are all four `tex/proof-guide.tex` classes. `docs/index.md` carries zero Japanese characters and zero unchecked checkboxes. `IsingModel/`, `tex/` and `scripts/` are untouched by `f2c1590a` (`git show --stat` lists `docs/index.md` alone), so the Lean verification table above still holds as measured. ## Scope note `Lemma_17_5_2` modules (Item B of #4746) are not touched by this PR. Part of #4746 Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
phasetr
added a commit
that referenced
this pull request
Jul 28, 2026
…afe-to-delete batch 3) (#4751) ## Summary Deletes ten `ℤ^d` thin-wrapper modules under `IsingModel/Concrete/LatticeGraphCorrelation/` — **39 theorems, 724 lines** — whose declarations have no consumer anywhere in the repository, and retracts in the same commit the eight survival-count claims in `docs/index.md` and `tex/proof-guide.tex` that the deletion would otherwise falsify. The 39 declarations form the `ℤ^d` layer of eight GJ §18.4–18.5 wrapper families (Mayer expansion term, `vdPolymerFamilies_sum`, `log_vdPolymerFamilies_sum`, the Mayer identity and `polymerFreeEnergy_eq_mayerPartialSum` edge-case slices, and the generic-`t` bound family), so this is one logical layer rather than a set of unrelated lemmas. ## Deleted modules | module | thm | |---|---| | `MayerAnalyticityTanhExpansionTerm.lean` | 4 | | `MayerEdgeCasesAlongExIdentity.lean` | 4 | | `MayerEdgeCasesLambdaPolymer.lean` | 4 | | `MayerVdBoundsAlongExNonneg.lean` | 4 | | `MayerVdRegularityExpansionTerm.lean` | 4 | | `MayerVdRegularityPolymer.lean` | 3 | | `MayerVdRegularityPolymerTanh.lean` | 4 | | `MayerVdRegularityTanhExpansionTermAlongEx.lean` | 4 | | `MayerVdRegularityTanhExpansionTermLambda.lean` | 4 | | `VdPolymerFamiliesAnalyticityLog.lean` | 4 | Two umbrella modules (`Umbrella/MagnetizationAndMayer.lean`, `Umbrella/TwoPointUniform.lean`) drop the ten import lines; eight surviving sibling modules have their `Moved:` doc-comment blocks corrected. ## Documentation retraction `docs/index.md` (8 sentences) and `tex/proof-guide.tex` (8 `\paragraph` blocks) each claimed these families sit at "all 4 volume layers". Both were re-measured on this branch with a line-spanning-aware declaration extractor — a `^theorem <name>` grep misses the 615 declarations in this repository whose name sits on a later line — and rewritten to the measured survival counts: | family | historical | surviving | deleted | surviving layers | |---|---|---|---|---| | #1582 `mayerExpansionTerm` regularity | 16 | **12** | 4 | Λ 4, AlongEx 4, ℤ^d Λ 2, ℤ^d AlongEx 2 | | #1584 `mayerExpansionTerm` tanh β/J | 24 | **12** | 12 | Λ 6, AlongEx 6 | | #1585 `vdPolymerFamilies_sum` regularity | 16 | **13** | 3 | Λ 4, AlongEx 4, ℤ^d Λ 1, ℤ^d AlongEx 4 | | #1586 `vdPolymerFamilies_sum` tanh β/J | 24 | **20** | 4 | Λ 6, AlongEx 6, ℤ^d Λ 2, ℤ^d AlongEx 6 | | #1587 `log_vdPolymerFamilies_sum` analyticity | 16 | **12** | 4 | Λ 4, AlongEx 4, ℤ^d AlongEx 4 | | #1588 `mayer_identity_at_*` | 16 | **12** | 4 | Λ 4, AlongEx 4, ℤ^d Λ 4 | | #1589 `polymerFreeEnergy_eq_mayerPartialSum_at_*` | 16 | **12** | 4 | Λ 4, AlongEx 4, ℤ^d AlongEx 4 | | #1596 `vdPolymerFamilies_sum` generic-`t` bounds | 16 | **12** | 4 | Λ 4, AlongEx 4, ℤ^d Λ 4 | Two independent consistency checks hold: surviving + deleted equals the historical per-PR total in every row, and the deleted column sums to 39, which equals the whole-tree declaration delta (10832 → 10793). The ten modules therefore account for every removal, and the historical "PR #N added M wrappers" sentences are correct as they stand — only the survival counts move. The retraction text names families by label (`mayer_identity_at_*`) rather than spelling out deleted declarations, and cites no deleted module path, so it adds no dangling citation. Every module path it does cite was checked to exist. ## Gates (all measured on this branch) | gate | result | |---|---| | `lake build` | exit 0, **5015 jobs** (5025 before, matching the ten deletions), 0 warnings, 0 errors | | `#print axioms` | unchanged; observed union `{propext, Classical.choice, Quot.sound}` | | `grep -rn "sorry" IsingModel/` | 0 tactic occurrences (2 hits are prose in doc comments) | | `citation_audit.py` | PASS, ratchet **0 cleared / 0 new**, 960 gating findings, coverage OK | | `dead_candidate_scan.py --self-test` | **100 tests OK**; fixtures PASS (18 rows) | | `python3 -m unittest scripts.test_audit_gate` | **166 tests OK** (1 skipped) | | `lake exe GKSTest` | `=== All tests passed ===` | | Japanese in `docs/index.md` / `tex/proof-guide.tex` | 0 | Final cross-check, re-scanning the 39 names against the **pre-deletion library overlaid with this commit's retracted docs/tex**: **safe-to-delete 39/39**, with `published-result`, `load-bearing` and `uncertain` all **0** and **0 coverage warnings**; both scanner canaries PASS. This is the check that would catch a retraction sentence accidentally citing a declaration that is being removed. The three Markdown backtick-parity warnings at `docs/index.md:1200/1201/1809` predate this branch and are unchanged. ## Ratchet `iter_checked_files()` 2003 → 1993 and `iter_lib_files()` 1996 → 1986, against floors 1957 / 1950, leaving slack 36. Module counts under both pathspec conventions: `IsingModel/*.lean` 1996 → 1986 (the full count) and `IsingModel/**/*.lean` 1957 → 1947 (the undercount that drops the 39 depth-1 modules). Four visited-list assertions in `scripts/test_audit_gate.py` — three in `ScanExecutionTest`, one in `V4ScanTest` — carried a bare `2000` literal that the named floors did not describe, so `iter_checked_files()` at 1993 trips it — this surfaced only when the deletion was applied. The literal gives way to the named floors, with a new `V4_FILE_FLOOR = 1977` calibrated 46 below the measured `iter_v4_files()` = 2023, the same offset the two existing floors use. Slack narrows to 36 with this batch, so a per-directory assertion or a floor recalibration is worth a look before the slack absorbs further batches. ## Build-time effect Per-module process cost was measured at **2.144 s wall / 2.156 s CPU** (warm cache, 10 modules × 2 passes, minus the `lake env` wrapper), giving **≈21.6 s CPU** for the ten modules. The wall figure is a serial extrapolation, not a parallel measurement; a warm-cache full build differs only by trace replay, so the saving shows up in clean and CI builds. ## Scope note The two homonym basenames that also exist under `AmbientLattice/SpecialCases/` (`MayerVdRegularityExpansionTerm.lean`, `VdPolymerFamiliesAnalyticityLog.lean`) are untouched, as is the ambient import at `VdPolymerFamiliesAnalyticityLogAlongEx.lean`. No file under `AmbientLattice/` is modified. Part of the safe-to-delete sweep tracked in #4746, following batches 1 (#4747) and 2 (#4749). ## Review follow-up (commit `3f77b982`) Two review findings, both about prose that named the wrong thing. No Lean source is touched by this commit. **Survival-location module names (`tex/proof-guide.tex`).** Six wrapper-family paragraphs pointed readers at modules that do not hold the declarations they claim. Each name below is the module that a scan of every `theorem`/`lemma` head under `IsingModel/` puts the surviving declarations in (the scan reads the name off the next line when the head wraps, which a single-line grep misses): | Family | Claimed | Measured | | --- | --- | --- | | #1589 ℤ^d | `Concrete/LatticeGraphCorrelation/MayerEdgeCases.lean` | `Concrete/LatticeGraphCorrelation/MayerEdgeCasesAlongExPolymer.lean` | | #1588 ℤ^d | `Concrete/LatticeGraphCorrelation/MayerEdgeCases.lean` | `Concrete/LatticeGraphCorrelation/MayerEdgeCasesLambda.lean` | | #1587 along-ex | `AmbientLattice/SpecialCases/VdPolymerFamiliesAnalyticity.lean`, `Concrete/…/VdPolymerFamiliesAnalyticity.lean` | `AmbientLattice/SpecialCases/VdPolymerFamiliesAnalyticityLog.lean` (+ `…LogTanh.lean`), `Concrete/…/VdPolymerFamiliesAnalyticityLogAlongEx.lean` | | #1586 Cont./Diff. | `AmbientLattice/SpecialCases/MayerVdRegularity.lean`, `Concrete/…/MayerVdRegularity.lean` | `AmbientLattice/SpecialCases/MayerVdRegularityVdPolymerTanh.lean` (+ `…TanhDifferentiable.lean`), `Concrete/…/MayerVdRegularityPolymerTanhAlongEx.lean` | | #1586 AnalyticAt | `VdPolymerFamiliesAnalyticity.lean` (both sides) | `VdPolymerFamiliesAnalyticityTanh.lean` (both sides) | | #1585 Cont./Diff./HasDerivAt | `AmbientLattice/SpecialCases/MayerVdRegularity.lean`, `Concrete/…/MayerVdRegularity.lean` | `AmbientLattice/SpecialCases/MayerVdRegularityVdPolymer.lean` (+ `…VdPolymerHasDerivAt.lean`), `Concrete/…/MayerVdRegularityPolymerAlongEx.lean` | | #1582 Cont./Diff. | `AmbientLattice/SpecialCases/MayerVdRegularity.lean` | `AmbientLattice/SpecialCases/MayerVdRegularityExpansionTerm.lean` (+ `MayerVdRegularityDifferentiableExpansionTerm.lean`) | | #1582 ℤ^d analytic | `Concrete/LatticeGraphCorrelation/MayerAnalyticity.lean` | `Concrete/LatticeGraphCorrelation/MayerAnalyticityExpansionTerm.lean` | `Concrete/LatticeGraphCorrelation/MayerEdgeCases.lean` carries zero declarations after this batch, so the first two rows pointed at an empty signpost module. `docs/index.md` was not already right either, contrary to the premise the review worked from: its #1582 ℤ^d analytic name, its #1586 AnalyticAt names and its #1587 along-exhaustion name were the same stale names, and its #1585/#1586 "`MayerVdRegularity.lean` cluster" phrasing named no member of that cluster. Those five spots move to the measured modules, so docs and tex now say the same thing. **Stale comment (`scripts/test_audit_gate.py`).** The comment above `V4_FILE_FLOOR` said the bare `2000` literal had sat at "three sites" in `ScanExecutionTest` and `V4JapaneseTest`. It sat at four — three in `ScanExecutionTest`, one in `V4ScanTest` — and `V4JapaneseTest` is not a class in this file. Comment only; the code and the floor values are unchanged. **Verification of this commit.** * `citation_audit.py`: PASS, 960 gating findings, ratchet 0 cleared / 0 new, coverage OK. The per-target citation census moves 1216 → 1217 (tex) and 2693 → 2700 (docs), because one generic module name gives way to the two or three exact ones; the census is a deletion budget and gates only downwards, and every added path resolves. * `python3 -m unittest scripts.test_audit_gate`: 166 tests OK (1 skipped). * `dead_candidate_scan.py --self-test`: 100 tests OK. * No Japanese in `tex/proof-guide.tex`, `docs/index.md` or the edited script. **Left alone, and why.** Three survival-location claims outside the six reviewed paragraphs remain stale and are unchanged here, since correcting them means asserting provenance this commit did not measure: `#1582`'s Λ-layer sentence points at `IsingModel/AmbientLattice/Analyticity.lean` while `mayerExpansionTerm_Λ_*` sit in `AnalyticityLambdaMayer.lean` (created by #1983); the `#1587` paragraph opens with a sentence naming `Analyticity.lean` and `Concrete/LatticeGraphCorrelation.lean` that its own next sentence contradicts; and the `#1581`/`#1583`/`#1584` paragraphs use the same bare `MayerVdRegularity.lean` shorthand. ## Independent audit (dev-audit-tier1, re-measured on `3f77b982`) Every number in the tables above was re-run in a throw-away worktree with a cloned build cache, and two corrections were folded into this message. * `lake build`: exit 0, **5015 jobs**, `grep -ic warning` = 0, `grep -ic error` = 0. The pre-deletion tree at `b09535cd` builds **5025 jobs** in the same setup, so the delta is exactly the ten modules. * `grep -rn "sorry" IsingModel/`: **2** prose hits, not 4 (the table above said 4); both are doc-comment sentences and are identical on `b09535cd`. No tactic occurrence. `native_decide`: 1 prose hit. `admit`: prose only. Zero `axiom` declarations. * `#print axioms` on four capstones (`mayer_identity_at_zero_Λ_latticeGraph`, `mayerExpansionTerm_Λ_latticeGraph_analyticAt`, `log_vdPolymerFamilies_sumAlongExhaustion_latticeGraph_analyticAt`, `exists_cubicMayerClusterFreeEnergyComplex_limit`): `[propext, Classical.choice, Quot.sound]` only. * `citation_audit.py`: PASS, 960 gating findings, ratchet 0 cleared / 0 new, coverage OK, census 1216 -> 1217 (tex) and 2693 -> 2700 (docs). * `dead_candidate_scan.py --self-test`: 100 tests OK. `python3 -m unittest scripts.test_audit_gate`: 166 tests OK (1 skipped). `lake exe GKSTest`: all tests passed. * Deletion-safety, re-derived independently: the ten modules hold **39** declarations; at `b09535cd` none of the 39 names occurs anywhere outside those ten files (`IsingModel/`, `docs/`, `tex/`, `scripts/`, `test/`), and at `3f77b982` none occurs at all. Re-scanning the 39 against the pre-deletion library overlaid with this commit's docs/tex reproduces **safe-to-delete 39**, `published-result` 0, `load-bearing` 0, `uncertain` 0, coverage warnings 0, both canaries PASS. * **`dead_candidate_scan.py --lean`** (requirement (i) of #4746 Item A, not reported in the body above) was run against a green pre-deletion build: *39 candidates compared against the elaborated graph; no consumer seen by Lean was missed on a safe-to-delete verdict*. * Ratchet re-measured: `iter_checked_files()` 2003 -> 1993, `iter_lib_files()` 1996 -> 1986, `v4_visited` 2033 -> 2023, against floors 1957 / 1950 / 1977 (slack 36 / 36 / 46). * Scope: no file under `AmbientLattice/` is touched; both homonym basenames survive and are still imported; `docs/index.md` and `tex/proof-guide.tex` retain no `Concrete/LatticeGraphCorrelation/` citation of any deleted module; no `Lemma_17_5_2` path is touched (#4746 Item B stays `USER-DECISION`); no Japanese, no added declaration, no long line, no credential-shaped string in the diff. * Informational: the scanner's cascade list shows **30** ambient/abstract declarations that become reference-0 as a consequence of this batch (16 in `AmbientLattice/SpecialCases/`, 8 in `AnalyticityLambdaMayer.lean`, 6 abstract GJ Sec 18 statements in `ClusterExpansion/MayerCore/Terms.lean`). They are correctly left in place here; recorded on #4746 so a later batch does not cascade into book content. 🤖 Generated with [Claude Code](https://claude.com/claude-code)
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
Lifts the abstract
mayerPartialSumtanh-form β/J regularity statements to all four volume layers:mayerPartialSum_tanh_continuous_beta/_JmayerPartialSum_tanh_differentiable_beta/_JmayerPartialSum_tanh_analyticAt_beta/_JmayerPartialSum_tanh_analyticOnNhd_beta/_JBundle contents (~32 new theorems): 8 abstracts × 4 layers (Λ-direct + along-exhaustion + ℤ^d Λ-direct + ℤ^d along-exhaustion).
Part of #1344.
Test plan
lake buildclean (zero linter warnings)grep -rn "sorry" IsingModel/= 0lake exe GKSTestpasses🤖 Generated with Claude Code