docs: repoint the dangling spectral-gap scaffolding citation at docs/index.md:1715 - #4710
Merged
Merged
Conversation
…ex.md:1715 Part of #4704. The row cites TransferMatrix/Layer{DobrushinContraction,Doeblin, DoobSpectralGap}.lean, three modules removed by commit 109690b (PR #4303) after the spectral-gap route was proven obstructed (#4081) and superseded by the §18 cluster-expansion route. Update the citation to reflect the removal without retracting the row's Done claim. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
The row cited TransferMatrix/Layer{DobrushinContraction,Doeblin,DoobSpectralGap}.lean,
which was deleted in PR-B1 (109690b, #4303) after #4081 established the obstruction.
109690b annotated several other affected rows with a "(scaffolding removed in PR-B1:
...)" note but missed this one. Apply the same annotation format used at
docs/index.md:1598-1619; no progress claim is changed (the row's Done-claim,
clusterExpansion_supersedes_transferMatrix_gap, remains intact and unaffected).
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
This was referenced Jul 25, 2026
phasetr
changed the title
phasetr
marked this pull request as ready for review
July 25, 2026 12:47
phasetr
added a commit
that referenced
this pull request
Jul 25, 2026
PR #4710 (merged, main d97f961) fixed the docs/index.md:1715 dangling citation; move that item from #4704's "not started" scope into "done" in the issue body and local mirror to avoid a three-layer (issue body / mirror / reality) mismatch, per dev-issue-manager's explicit instruction. Also record #4709's mirror (new tracking issue, previously untracked) and bring the session handoff doc to its final state (5 merged PRs, 2 new issues, 5 user-approval-pending items, 5 carry-forward lessons). 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
#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
docs/index.md:1715citesTransferMatrix/Layer{DobrushinContraction,Doeblin,DoobSpectralGap}.lean,three modules that no longer exist. The three modules were introduced under #3511 (
ed70e3f5/#4076,88cb6027/#4078,6022207f/#4079, 2026-06-20) and removed by commit109690bd(PR #4303, PR-B1 of#4298, 2026-06-26), which retired the obstructed spectral-gap scaffolding under the author's
approval after #4081 established the obstruction. The citing row itself was added by
752f31ae(PR #4228, item B of #4214), which never touched the Layer* modules. The removed scaffolding is preserved under the git tag
archive/transfermatrix-spectral-gap-scaffolding.Key point (this PR is not a retraction)
The row's substantive "Done" claim is
clusterExpansion_supersedes_transferMatrix_gapinIsingModel/TransferMatrix/ClusterExpansionSupersession.lean:77, which still exists. Only thesupplementary citation to the three retired modules is dangling. The removal commit annotated the
other affected rows with
(scaffolding removed in PR-B1 …)but missed this one row. So this is acitation fix, not a retraction, and no progress claim changes.
Scope
Exactly one line in
docs/index.md. No Lean change, notex/change, no progress-claim change.Explicitly out of scope, awaiting user authorization:
docs/index.md:1974overstates wrappercounts (8 vs the measured 6; row total 12 vs the measured 10). Correcting it would walk back a
progress claim, so it is deferred pending authorization (see the #4704 comment).
Part of #4704
Verification
lake buildexits 0 with 5040 jobs and zero warnings (no Lean file changed, so the build replaysfrom cache).
docs/index.mdno longer referencesLayerDobrushinContraction,LayerDoeblin, orLayerDoobSpectralGap: zero matches.clusterExpansion_supersedes_transferMatrix_gapis confirmed present atIsingModel/TransferMatrix/ClusterExpansionSupersession.lean:77, and the two declarations itcites are confirmed present:
exists_high_temp_no_phase_transitionatHighTempAnalyticityCapstone.lean:143andhasExponentialDecay_latticeGraph_of_betaJ_two_d_lt_oneat
HighTempMassGap.lean:269.in main (base: 31 occurrences; head: 32 occurrences).
**Done (...)**cell text and counts) is empty.docs/index.md, one file, one line changed (1 insertion / 1 deletion).docs/index.md:1974is unchanged: the wrapper-count correction (8→6 / 12→10) awaitingauthorization is untouched.
docs/index.md.dev-reviewand codex both returned APPROVE;dev-audit-tier1re-audit PASS.buildcheck passed in 3m28s at63088fc3.🤖 Generated with Claude Code