docs: retract §18.4 Mayer order-3 claims left stale by #4702 - #4705
Merged
Conversation
PR #4702 (main 4d23d7c) deleted the explicit Mayer order-3 lemmas and their two modules but never touched docs/index.md or tex/proof-guide.tex, leaving stale claims about non-existent theorems/files. This branch will retract those claims while preserving the general recurrence and other live decls. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Commit 4d23d7c (#4702) deleted mayerExpansionTerm_three, mayerPartialSum_three, mayerExpansionTerm_three_eq, and mayerPartialSum_three_eq (files MayerCore/Truncations.lean, MayerCore/MayerTermThreeEval.lean), but only touched .lean files; docs/index.md and tex/proof-guide.tex still described the deleted declarations. This retracts those references: - docs/index.md §18.4 cell: drop the "Mayer truncation structure" clause outright, and retitle/trim the "Unified n=3 Ursell classification + third Mayer term" clause to keep only the still-live ursellCoefficient_fin_three_eq content. - tex/proof-guide.tex: delete the "Mayer truncation structure (§18.4)" paragraph (was lines 19368-19383), and retitle/trim the "Unified n=3 classification and the third Mayer term (§18.4)" paragraph (was lines 21076-21098) to keep only the ursellCoefficient_fin_three_eq sentence. Preserved (still-live, unaffected): UrsellFinThree, ursellCoefficient_fin_three_eq, mayerPartialSum_two, mayerPartialSum_succ, mayer_identity_general_t, and the mayerExpansionTerm_{one,two,three}_eq_of_pairwise_disjoint family. Also picks up .self-local/issues/INDEX.md, a tracked mirror-bookkeeping file left uncommitted by a prior session. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
phasetr
marked this pull request as ready for review
July 25, 2026 09:04
phasetr
added a commit
that referenced
this pull request
Jul 25, 2026
…73aabd) Records the final closed state of #4700/#4701/#4706 (all merged this session via PR #4705/#4703/#4707) so the local mirrors match GitHub, re-anchors #4704's stale-reference counts to 9/156 post-#4705, and updates the handoff report with the session's final state (merged PRs, the #4702 defect-class root-cause finding, and the next-session candidates). Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
phasetr
added a commit
that referenced
this pull request
Jul 25, 2026
…sionSupersession module docstring (#4711) ## What `IsingModel/TransferMatrix/ClusterExpansionSupersession.lean:18-19` (module doc comment) names three deleted modules — `LayerDobrushinContraction.lean`, `LayerDoeblin.lean`, `LayerDoobSpectralGap.lean` — as if they still exist in the repo. They do not. - Introduced: `ed70e3f5` (#4076, `LayerDobrushinContraction.lean`), `88cb6027` (#4078, `LayerDoeblin.lean`), `6022207f` (#4079, `LayerDoobSpectralGap.lean`) — all part of the #3511 §17.1 spectral-gap series, 2026-06-20. - Deleted: `109690bd` (#4303, the #4298 PR-B1 scaffolding removal, 2026-06-26), after #4081 established the obstruction (the global Dobrushin/Doeblin contraction cannot give a transverse-volume-uniform gap) and the author approved removal. The removed scaffolding is preserved at git tag `archive/transfermatrix-spectral-gap-scaffolding`. `grep -rn` over `IsingModel/` confirms this docstring is the **only remaining reference** to the three deleted module names anywhere in the library. This PR removes the three dead filenames from the docstring and replaces them with the same canonical note used throughout `docs/index.md` (route obstructed #4081, superseded by §18 #4228/#4255, archived at the git tag), **without changing any Lean statement, declaration, or proof** — a doc-comment-only fix. ## Scope - The only Lean change is **the module docstring of this one file** (`ClusterExpansionSupersession.lean:18-19`) — no declaration, statement, proof term, import or attribute is touched. - The diff also carries `.self-local/issues/4704.md` (issue-mirror bookkeeping for this PR), including an authorization-trail record clarifying this PR rests on the main agent's own scope judgment (finishing the #4303 dangling-reference cluster already started by PR #4710), not on user authorization. - **Systematically scanning `IsingModel/` for other stale doc-comment references is intentionally out of scope** of this PR — that would be a scope expansion of #4704 and requires explicit user authorization. - This is the last outstanding reference to the #4303 deletion. PR #4710 fixed the other one (`docs/index.md:1715`); this location was missed by the earlier docs/tex scans because it lives inside a `.lean` doc comment. (PR #4705 and PR #4708 were the same *kind* of stale- reference cleanup but stem from different removals — #4702's Mayer order-3 retraction and the `SpecialCases/Legacy.lean` module splits respectively — not from #4303.) - **Also out of scope (pending authorization)**: the count discrepancy at `docs/index.md:1974` (stated vs. measured item counts) is not touched here, since correcting it would mean walking back a progress claim and needs explicit authorization. Likewise, the unaudited candidate pool in `tex/proof-guide.tex` is not touched — prior scans found it dominated by false positives, and a reliable scan methodology has not yet been established. Part of #4704. ## Verification Measured on the implementation commit `28709f2a`: - `lake build`: exit 0, 5040 jobs, zero warnings. - The three deleted module names return zero matches across `IsingModel/`, `docs/` and `tex/`. - Zero Lean statement/declaration changes: everything from `namespace IsingModel` onward is byte-identical to `main`, including the statement and proof of `clusterExpansion_supersedes_transferMatrix_gap`. - `#print axioms clusterExpansion_supersedes_transferMatrix_gap` = `[propext, Classical.choice, Quot.sound]`, unchanged. - `lake exe GKSTest` passes; no `sorry`/`admit`/`native_decide` in use. - Longest added line in the Lean file is 89 codepoints (92 across the whole diff, in the issue mirror); no CJK characters introduced. - CI `build` re-verified green on the final HEAD `8546fd4f` (3m48s), after adding the authorization-trail record to the mirror. 🤖 Generated with [Claude Code](https://claude.com/claude-code) Co-authored-by: Claude Opus 5 (1M context) <noreply@anthropic.com>
phasetr
added a commit
that referenced
this pull request
Jul 25, 2026
Move #4704 item (a) into Done citing PR #4711, restate remaining debt as 2 items, and record that PR #4711 rests on the main agent's own scope judgment rather than user authorization. Fix #4692's stale "Item A: parked" checklist line (already disposed by PR #4702/#4705). Update the handoff report with the #4303 dangling-reference cluster's closure and this session's governance corrections (#4692/#4559/#4642 GitHub comments). 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>
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.
What
PR #4702 (commit
4d23d7cc) deleted the explicit Mayer order-3 lemmas(
mayerExpansionTerm_three,mayerPartialSum_three,mayerExpansionTerm_three_eq,mayerPartialSum_three_eq) and their two modules (MayerCore/Truncations.lean,MayerCore/MayerTermThreeEval.lean), but its commit touched only three.leanfiles — thepromised docs/tex retraction was never carried out. As a result
docs/index.mdandtex/proof-guide.texstill document Lean theorems and files that do not exist.Scope
Retract those claims only. Explicitly preserved (must NOT be retracted):
UrsellFinThree,ursellCoefficient_fin_three_eq,mayerPartialSum_two,mayerPartialSum_succ, the generalmayerExpansionTermrecurrence,mayer_identity_general_t, andmayerExpansionTerm_{one,two,three}_eq_of_pairwise_disjoint(a different proposition with asimilar name).
This PR also carries
.self-local/issues/INDEX.md, an issue-mirror bookkeeping update(#4701 close, #4700 reopen, #4704 filing) that was left uncommitted by the preceding #4703
workflow on the same day and is bundled here for convenience; it is not part of the docs/tex
retraction described above.
Targets
Line numbers below are as anchored at branch-open time; the implementer should re-grep to confirm
before editing.
docs/index.md— the §18.4 cell (currently around line 2126), 2 clauses to retract.tex/proof-guide.tex19368–19383 — delete the whole paragraph.tex/proof-guide.tex21076–21098 — the first half (theursellCoefficient_fin_three_eqdescription) is preserved/retitled; only the second half is deleted.
Plan reference
.self-local/reports/research-4702-stale-docs-retraction.md(contains drafted English replacementparagraphs).
Closes #4700.
Test plan
rgfor the 4 deleted decl names + the 2 deleted file paths returns zero hits indocs/andtex/.rg -n "[ぁ-んァ-ン一-龯]" tex/proof-guide.texreturns nothing (no Japanese contamination).tex/proof-guide.texbuilds cleanly with latexmk (549 pages).lake buildunaffected (no Lean code changes in this PR): 5040 jobs, 0 warnings.UrsellFinThree,ursellCoefficient_fin_three_eq,mayerPartialSum_two,mayerPartialSum_succ,mayer_identity_general_t,mayerExpansionTerm_{one,two,three}_eq_of_pairwise_disjoint) still exist in the source andare still referenced in
docs//tex/.🤖 Generated with Claude Code