docs: repoint the dangling scaffolding references in the ClusterExpansionSupersession module docstring - #4711
Merged
Merged
Conversation
…nSupersession docstring -- #4704
…cstring The module docstring named three transfer-matrix scaffolding files (LayerDobrushinContraction.lean, LayerDoeblin.lean, LayerDoobSpectralGap.lean) that were removed in PR-B1 (#4303). Replace the dangling names with the same removal note used throughout docs/index.md: PR-B1, obstruction #4081, superseded by §18 #4228/#4255, archived at git tag archive/transfermatrix-spectral-gap-scaffolding. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
…8709f2 UPDATE #8's closing sentence said the docstring fix was "not yet implemented (draft, no doc edit staged)" while the same PR's current HEAD already contains implementation commit 28709f2. Correct the mirror to state the implemented status and the gate results (CI build pass, dev-verify PASS/10, dev-audit-tier1 PASS), and record the side effect that the three retired module names now have zero surviving references repo-wide. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
phasetr
marked this pull request as ready for review
July 25, 2026 13:20
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 25, 2026
#4709 to 9 incidents (#4723) ## What Two `.self-local/issues/` governance corrections found by `dev-issue-manager`, both mirror/ metadata-only (no `IsingModel/`, `docs/index.md`, or `tex/` change): 1. **`.self-local/issues/4721.md` was missing** — #4721 (build-speed: replace cast-positivity with `Nat.cast_nonneg` at the two FV ratio modules, `dev-perf` A/B measured -3.75s) was the only open GitHub issue with no local mirror. Created verbatim from the GitHub issue body; no implementation has started (all acceptance-criteria checkboxes remain unchecked). 2. **Issue #4709 was stale** — its title/body still said "four false-claim incidents" while the session's actual count reached **nine**: the original #4702/#4703/#4707/#4708, plus #4710 (a provenance-claim error about which commit introduced 3 retired modules), #4711 (a mis-stated codepoint count), and #4716/#4720 (#4720 across two rounds). GitHub title/body updated via `gh issue edit` to the full count, and to record a **newly-identified subclass** for #4716/#4720: a PR (and its `.self-local/issues/` mirror) drafted at open time in plan/future-tense form on the premise it will be rewritten once implementation is pushed — and the rewrite is forgotten. This subclass is not caught by "diff the body against the diff" alone (the body's factual claims can stay diff-consistent; only the tense is stale). A proposed (not-implemented, authorization-pending) fix is recorded in the GitHub issue body. ## Scope 3 files changed, all under `.self-local/`: - `.self-local/issues/4721.md` (new) - `.self-local/issues/4709.md` (append an UPDATE section + title line resync; earlier history untouched) - `.self-local/issues/INDEX.md` (new dated entry) No `IsingModel/`, `docs/index.md`, or `tex/` file is touched. `lake build` is unaffected (no Lean/doc file in the diff); CI is expected to replay from cache. ## Verification - `git diff main...HEAD --stat` = the 3 files above only. - GitHub #4709 re-fetched after edit: title/body confirmed to state "nine" incidents and the two-subclass structure; #4721 re-fetched: mirror content matches the GitHub issue body verbatim. - No Japanese characters in either mirror file. 🤖 Generated with [Claude Code](https://claude.com/claude-code)
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
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.ed70e3f5(feat(gj-17.1): prove the Dobrushin oscillation contraction — #3511 #4076,LayerDobrushinContraction.lean),88cb6027(feat(gj-17.1): Doeblin minorization and a strict Dobrushin bound — #3511 #4078,LayerDoeblin.lean),6022207f(feat(gj-17.1): bound the subdominant ratio by the Doob Dobrushin coefficient — #3511 #4079,LayerDoobSpectralGap.lean) — all part of theTransfer-matrix formalization (GJ §17.1/§17.5): 1D Ising chain and beyond #3511 §17.1 spectral-gap series, 2026-06-20.
109690bd(refactor(gj-17.1): remove obstructed transfer-matrix spectral-gap scaffolding (~6.6k lines) — #4298 PR-B1 #4303, the Post-axiom-free refactoring: build speedup + simplification/abstraction (investigation → execution) #4298 PR-B1 scaffolding removal, 2026-06-26), after feat(gj-17.1): site factorization of the identity-transition cross-ratio — #3511 #4081established 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 -rnoverIsingModel/confirms this docstring is the only remaining reference tothe 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
(
ClusterExpansionSupersession.lean:18-19) — no declaration, statement, proof term, importor attribute is touched.
.self-local/issues/4704.md(issue-mirror bookkeeping for this PR).That file is local tracking material, not library code or published documentation.
IsingModel/for other stale doc-comment references isintentionally out of scope of this PR — that would be a scope expansion of 960 gating + 93 advisory, PR #4743 #4704 and
requires explicit user authorization.
(
docs/index.md:1715); this location was missed by the earlier docs/tex scans because itlives inside a
.leandoc comment. (PR docs: retract §18.4 Mayer order-3 claims left stale by #4702 #4705 and PR docs: repoint four stale .lean path citations in docs/index.md #4708 were the same kind of stale-reference cleanup but stem from different removals — refactor: remove unused explicit Mayer order-3 lemmas + retract §18.4 order-3 docs claim #4702's Mayer order-3 retraction and
the
SpecialCases/Legacy.leanmodule splits respectively — not from refactor(gj-17.1): remove obstructed transfer-matrix spectral-gap scaffolding (~6.6k lines) — #4298 PR-B1 #4303.)docs/index.md:1974(stated vs. measured item counts) is not touched here, sincecorrecting it would mean walking back a progress claim and needs explicit authorization.
Likewise, the unaudited candidate pool in
tex/proof-guide.texis not touched — priorscans 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.IsingModel/,docs/andtex/.namespace IsingModelonward isbyte-identical to
main, including the statement and proof ofclusterExpansion_supersedes_transferMatrix_gap.#print axioms clusterExpansion_supersedes_transferMatrix_gap=[propext, Classical.choice, Quot.sound], unchanged.lake exe GKSTestpasses; nosorry/admit/native_decidein use.mirror); no CJK characters introduced.
🤖 Generated with Claude Code