refactor: drop the private duplicate of finiteRegionPseudoMassDistFV_le_of_mem - #4720
Merged
Merged
Conversation
Empty commit to open the PR before implementation, per repo PR-early-create convention. Follow-up commit will delete the private duplicate finiteRegionPseudoMassDistFV_le_pair and redirect its call site to the public finiteRegionPseudoMassDistFV_le_of_mem. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Sync the .self-local/issues mirror with the opened PR number, per dev-pr-workflow's PR-early-create + source-of-truth-sync convention; this rides along on the feature branch rather than committing to main directly. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
`finiteRegionPseudoMassDistFV_le_pair` (private, in `Lemma_17_5_2/GlobalPseudoMassDistCubicInfFV.lean`) was statement- and proof-identical to the public `finiteRegionPseudoMassDistFV_le_of_mem` in `Lemma_17_5_2/FiniteRegionPseudoMassDistFV.lean`, which the former module already imports. - Delete the private duplicate and its docstring. - Redirect its single call site inside `globalPseudoMassDist_eq_csInf_finiteRegionFV_cubic` to the public lemma (same argument order, no adjustment needed). - `docs/index.md` PR-FV2 row: name the surviving public lemma instead of the deleted private helper. No statement changes. `lake build`: exit 0, 5040 jobs, zero warnings. `#print axioms` for `finiteRegionPseudoMassDistFV_le_of_mem` and `globalPseudoMassDist_eq_csInf_finiteRegionFV_cubic`: [propext, Classical.choice, Quot.sound]. `lake exe GKSTest` passes. Issue #4717. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
…of_mem docstring Preserve the reproduction-prevention knowledge from the deleted private duplicate (PR #4720): keeping this lemma standalone avoids re-triggering the heavy pseudoMassExt/correlationAlongExhaustion defeq check inside a bridge's set-folded context (cf. PR #4716's isDefEq fix). Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
phasetr
marked this pull request as ready for review
July 25, 2026 16:50
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
finiteRegionPseudoMassDistFV_le_pair(private,IsingModel/Concrete/LatticeGraphCorrelation/Lemma_17_5_2/GlobalPseudoMassDistCubicInfFV.lean:34)was a verbatim duplicate of the public
finiteRegionPseudoMassDistFV_le_of_mem(
IsingModel/Concrete/LatticeGraphCorrelation/Lemma_17_5_2/FiniteRegionPseudoMassDistFV.lean:106).A mechanical diff of the two declarations showed the only differences were 3 doc-comment lines
plus a trailing blank line — binder order, implicit/explicit split, typeclass arguments, and the
proof body (
unfold …; exact Finset.inf'_le _ hmem) were all identical. The consuming module(
GlobalPseudoMassDistCubicInfFV.lean) already imports the defining module on line 1, so removingthe private duplicate requires zero new imports.
Changes
GlobalPseudoMassDistCubicInfFV.lean.globalPseudoMassDist_eq_csInf_finiteRegionFV_cubic,now at line 137) to the public
finiteRegionPseudoMassDistFV_le_of_mem, with the same argumentlist (
hα p n hne_n hpair_mem).docs/index.md:1929to the public name. This is a rename only —the narrated proof step ("
finiteRegionFV(volume n) ≤ m⁻_FV(x,z,n)eventually") and theDone status of
globalPseudoMassDist_eq_csInf_finiteRegionFV_cubicare unchanged.finiteRegionPseudoMassDistFV_le_of_memdocstring(
FiniteRegionPseudoMassDistFV.lean:106-108): keeping this lemma standalone avoidsre-triggering the heavy
pseudoMassExt/correlationAlongExhaustiondefeq check inside abridge's
set-folded context (this is the knowledge behind PR build-speed: eliminate the failed higher-order-unification isDefEq cluster (-22.09s) #4716'sisDefEqfix, and wouldotherwise be lost with the private declaration).
tex/proof-guide.texis unchanged: it never referenced_le_pair, and already citesfiniteRegionPseudoMassDistFV_le_of_memby its public name at two locations (lines 35774 and35940). Unlike the refactor: remove unused explicit Mayer order-3 lemmas + retract §18.4 order-3 docs claim #4702-style gap (docs updated, tex left stale), tex needed no update here.
.self-local/issues/4717.mdmirror update is included in this PR.Scope
4 files changed:
IsingModel/Concrete/LatticeGraphCorrelation/Lemma_17_5_2/FiniteRegionPseudoMassDistFV.lean(docstring only — rationale moved in; no statement or proof change)
IsingModel/Concrete/LatticeGraphCorrelation/Lemma_17_5_2/GlobalPseudoMassDistCubicInfFV.lean(delete the private duplicate + redirect its call site)
docs/index.md(rename the cited helper at line 1929; narrative/Done status unchanged).self-local/issues/4717.md(mirror update)No statement changes anywhere. This is deletion + call-site redirection + docstring
relocation + doc rename only.
Verification
lake build: exit 0, 5040 jobs (same job count asmain), zero warnings.lake exe GKSTest: all tests pass.#print axiomsfor both affected declarations is[propext, Classical.choice, Quot.sound]:finiteRegionPseudoMassDistFV_le_of_memglobalPseudoMassDist_eq_csInf_finiteRegionFV_cubicgrep -rn finiteRegionPseudoMassDistFV_le_pairacrossIsingModel/,docs/,tex/,scripts/returns zero hits..leanfile exceeds 100 columns (longest added line: 95).(
docs/index.mdhas long lines throughout and is unaffected by this bound.)Closes #4717.
🤖 Generated with Claude Code