feat: §18.6 partitionFunction/freeEnergy Continuous + Differentiable along-ex + ℤ^d wraps GJ-命題-bundle - #1611
Merged
Conversation
…ng-ex + ℤ^d wraps
…along-ex + ℤ^d wraps Lifts eight abstract regularity theorems to the missing along-exhaustion + ℤ^d (Λ + along-ex) layers (Λ-layer wraps already exist via PR #1541, #1533): - `partitionFunction_continuous_beta_general_h` - `partitionFunction_continuous_J_general_h` - `partitionFunction_differentiable_beta_general_h` - `partitionFunction_differentiable_J_general_h` - `partitionFunction_continuous_h` - `partitionFunction_differentiable_h` - `freeEnergy_continuous_joint` - `freeEnergy_differentiable_joint` Bundle contents: 24 new theorems (8 abstracts × 3 missing layers). `docs/index.md` §18.6 row + `tex/proof-guide.tex` updated. `lake build` clean (zero linter warnings); `grep -rn "sorry" IsingModel/` = 0; `lake exe GKSTest` passes. Part of #1344. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
phasetr
marked this pull request as ready for review
May 4, 2026 17:05
phasetr
added a commit
that referenced
this pull request
Jul 28, 2026
…h 4) Deletes the nine fully-dead modules of issue #4746 Item A batch 4: 31 declarations, 712 lines, all of them zero-consumer thin Z^d Lambda-layer or along-exhaustion wrappers. Concrete/LatticeGraphCorrelation/ PartitionFreeEnergyBoundsAlongExBridges.lean (4 decls, 78 lines) PartitionFreeEnergyMonotonicityFreeEnergyAlongEx.lean (3 decls, 56 lines) PartitionFreeEnergyRegularity.lean (4 decls, 87 lines) PartitionFunctionGeneralAnalyticity.lean (5 decls, 83 lines) PartitionFunctionSymmetryCubicAbsH.lean (2 decls, 42 lines) MagnetizationCorrelationBasic.lean (4 decls, 72 lines) MayerFilterConnected.lean (4 decls, 96 lines) MayerVdBounds.lean (3 decls, 81 lines) PseudoMass/FromParamsHZero/JZeroJointRegularity.lean (2 decls, 117 lines) The batch is the union of the three cascade-0 groups of the 32 lane-eligible fully-dead modules, so no declaration anywhere else loses its last consumer. Library wiring: 8 import lines drop from Umbrella/PartitionAndPerStage.lean (5) and Umbrella/MagnetizationAndMayer.lean (3). Deleting JZeroJointRegularity.lean would leave PseudoMass/FromParamsHZero.lean an empty umbrella and break its only consumer (FromParamsBounds/LogBounds.lean, which reached Mathlib through that one line), so the umbrella is repointed at JZeroHRegularity, which the deleted module itself imported. The public import surface is unchanged. Documentation retraction, in the same commit because the build never reads docs: * docs/index.md: 4 module-directory bullets removed; the nested-brace family label at the free-energy monotonicity row split so it no longer names the 3 deleted members; the BddAbove_freeEnergyAlongExhaustion_latticeGraph* family label dropped (it lost every member); 4 wrapper-count claims re-measured (PR #1595 12 -> 9, PR #1610 20 -> 15, PR #1611 24 -> 20, PR #1613 20 -> 16). * tex/proof-guide.tex: the same 4 counts, plus the 4 "now live in" sentences that named the deleted child modules. * 11 in-library module doc comments that pointed at the deleted modules. The PR #1611 and PR #1613 count claims are retractions the batch-4 design did not list; they were found by measuring every layer of each affected wrapper family rather than by trusting the scanner, which cannot see prose counts. Script recalibration: * scripts/test_dead_candidate_scan.py: the ferromagnetic family pin moves SAFE 47 -> 46 and UNCERTAIN 77 -> 78 (one declaration moves away from safe-to-delete, the safe direction), and three docs/index.md line pins shift by the 8 removed bullet lines. * scripts/test_audit_gate.py: the floors are NOT lowered. The comment blocks are corrected: they recorded 2003/1996 as "measured", which were the counts from before PR #4751's deletion, making the derived "46 below" false. Measured now: 1984 / 1977 / 2014 against floors 1957 / 1950 / 1977. * scripts/audit/citation_baseline.tsv: 4 rows hand-moved from AMBIGUOUS to BASENAME_ONLY. Deleting one of two files sharing a basename makes the tex citation resolve uniquely, which is a class change and not new erosion; the gating finding total is unchanged at 960. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
This was referenced Jul 28, 2026
phasetr
added a commit
that referenced
this pull request
Jul 28, 2026
…/Mayer and J = 0 pseudo-mass wrapper modules (safe-to-delete batch 4) (#4754) Part of #4746 (Item A, batch 4). Deletes the nine fully-dead modules of batch 4 — **31 declarations, 712 lines** — and retracts every documentation claim that counted them. The batch is the union of the three cascade-0 groups of the 32 lane-eligible fully-dead modules, so no declaration anywhere else in the library loses its last consumer. Measured on `fd7a2a71` (`git ls-remote origin main` at branch time) in a throw-away worktree with an APFS-cloned warm `.lake`. ## What was deleted | module | decls | lines | |---|---|---| | `Concrete/LatticeGraphCorrelation/PartitionFreeEnergyBoundsAlongExBridges.lean` | 4 | 78 | | `Concrete/LatticeGraphCorrelation/PartitionFreeEnergyMonotonicityFreeEnergyAlongEx.lean` | 3 | 56 | | `Concrete/LatticeGraphCorrelation/PartitionFreeEnergyRegularity.lean` | 4 | 87 | | `Concrete/LatticeGraphCorrelation/PartitionFunctionGeneralAnalyticity.lean` | 5 | 83 | | `Concrete/LatticeGraphCorrelation/PartitionFunctionSymmetryCubicAbsH.lean` | 2 | 42 | | `Concrete/LatticeGraphCorrelation/MagnetizationCorrelationBasic.lean` | 4 | 72 | | `Concrete/LatticeGraphCorrelation/MayerFilterConnected.lean` | 4 | 96 | | `Concrete/LatticeGraphCorrelation/MayerVdBounds.lean` | 3 | 81 | | `PseudoMass/FromParamsHZero/JZeroJointRegularity.lean` | 2 | 117 | | **total** | **31** | **712** | The line total is 712, not the 721 the batch-4 design recorded: the design's per-file figures are each one higher than `wc -l`, and `git diff --stat` charges 712 deletions. Build jobs go 5015 → 5006. **No build-time claim is made.** Own elaboration cost of these modules is at or below the per-module import-only baseline (issue #4724), so the wall-clock effect is not measurable and none is asserted. ## Declaration-level double confirmation The 31 declarations were re-extracted independently of the design, with a line-folding-aware extractor (a same-line `^theorem NAME` regex silently misses every wrapped declaration, and did so on a first pass here). All 31 names **and their line numbers** reproduce the design's appendix exactly. A boundary-aware reference check over **every tracked file** (not only `IsingModel/`, `docs/`, `tex/`) found **0** genuine references. The four raw `git grep` hits are all prefix collisions with surviving siblings, and none is a reference to a deleted declaration: | raw hit | why it is not a reference | |---|---| | `PartitionFreeEnergyBoundsFeAlongExId.lean:46` | `…_nonneg_of_ferromagnetic` — different identifier | | `PartitionFunctionSymmetryLog.lean:63,64`, `PartitionFunctionSymmetryLogCubic.lean:29,39` | `log_…` prefix — different identifiers | | `PolymerFreeEnergyEpsilonSharpening.lean:31` | `…_minus_one_pow_at_zero` — different identifier | ## Requirement (i): `--lean` cross-check `python3 scripts/dead_candidate_scan.py <31 names> --lean`, run against the green pre-deletion build (scanner blob `7f47c6bd`, unmodified), exit 0: ``` --lean cross-check: 31 candidate(s) compared against the elaborated graph; no consumer seen by Lean was missed on a safe-to-delete verdict canary: 1021 declarations carrying 'Λ'x1018, 'β'x1, 'σ'x2 each find themselves: PASS canary: 10162 code citations in tex/proof-guide.tex, none broken across a line: PASS -- published-result: 0 -- -- load-bearing: 0 -- -- uncertain: 0 -- -- safe-to-delete: 31 -- -- coverage warnings: 0 -- ``` Every one of the 31 carries the reason *"no reference outside the delete set, no citation in the scanned documentation"*. ## Requirement (v): the two sweeps Both sweeps run the full-library scan (`--pattern '.'`, 10,868 scanned declarations) on the **pre-deletion library**, changing only the documentation. | sweep | docs/tex | safe-to-delete | delete set | |---|---|---|---| | 1 | pre-deletion | 1127 | 31/31 safe | | 2 | this commit's | 1123 | 31/31 safe | **Condition (v) assertion: 0 violations.** No declaration outside the delete set moves toward `safe-to-delete`. All seven verdict moves are in the protective direction, and they are quoted rather than summarised: ``` safe-to-delete -> published-result freeEnergyAlongExhaustion_latticeGraph_cubicExhaustion_monotone_J safe-to-delete -> published-result freeEnergyAlongExhaustion_latticeGraph_cubicExhaustion_monotone_beta safe-to-delete -> published-result freeEnergyAlongExhaustion_latticeGraph_cubicExhaustion_monotone_h uncertain -> published-result freeEnergyAlongExhaustion_latticeGraph_cubicExhaustion_upper_bound uncertain -> published-result freeEnergyAlongExhaustion_latticeGraph_upper_bound uncertain -> published-result mayerPartialSum_Λ_latticeGraph_analyticOnNhd safe-to-delete -> uncertain mayerPartialSum_Λ_latticeGraph_differentiable ``` The first three are the point of the surgical brace split: replacing the nested brace by two exact labels turns a citation the scanner could not resolve into citations it can. The 29 declarations the design predicted could be stranded by a careless line rewrite are all still `published-result`. An **independent fail-closed re-expansion** of every backticked token in `docs/index.md` and every `\texttt{}`/`\path{}` token in `tex/proof-guide.tex` (recursive brace expansion, `*` as zero-or-more, cross-checked against a folding-aware index of all 10,963 library declarations) confirms the design's result and adds nothing: of every family token that covers at least one deleted name, **exactly one loses all of its members** — `` `BddAbove_freeEnergyAlongExhaustion_latticeGraph*` `` at `docs/index.md`, which this PR drops. Every other covering token keeps survivors (e.g. `` `correlation_*_latticeGraph` `` 19 members → 17, `` `freeEnergyAlongExhaustion_latticeGraph_*` `` 103 → 98). ## Documentation retraction Prose *counts* are invisible to the scanner, so each affected wrapper family was measured layer by layer instead. **Two of the four count retractions below were not in the batch-4 design** and were found by that measurement. | site | before | after | in design? | |---|---|---|---| | `docs/index.md` PR #1595 / `tex` §18.5 | `12 new thin wrappers (3 abstracts × 4 layers)` | `12 … ; the three ℤ^d Λ-layer wrappers had no consumers and were deleted in PR #4754, leaving 9 across three layers` | yes | | `docs/index.md` PR #1610 / `tex` §18.6 | `20 thin wrappers (5 abstracts × 4 layers)` | `20 … leaving 15 across three layers` | yes | | `docs/index.md` PR #1611 / `tex` §18.6 | `24 thin wrappers (8 abstracts × 3 missing layers)` | `24 … leaving 20 across the remaining layers` | **no** | | `docs/index.md` PR #1613 / `tex` §18.5 | `20 thin wrappers (5 abstracts × 4 layers)` | `20 … leaving 16` | **no** | PR #1613 loses 4 and not 5 because the ℤ^d Λ-layer `mayerPartialSum_Λ_latticeGraph_analyticOnNhd` lives in another module and survives; the retraction says so. Family labels and module lists: | site | before | after | |---|---|---| | `docs/index.md` module-directory bullets | 4 bullets naming the deleted concrete modules | removed (8 lines) | | `docs/index.md` §4.6 monotonicity row | `` `freeEnergyAlongExhaustion_latticeGraph{,_cubicExhaustion}_{upper_bound,monotone_{J,h,beta}}` `` (8 members, 3 deleted) | `` `…latticeGraph{,_cubicExhaustion}_upper_bound` `` + `` `…latticeGraph_cubicExhaustion_monotone_{J,h,beta}` `` | | `docs/index.md` §4.6 bounds row | `` , and `BddAbove_freeEnergyAlongExhaustion_latticeGraph*` now live in `PartitionFreeEnergyBounds.lean` `` (2 members, both deleted) | token dropped; location claim widened to `` `PartitionFreeEnergyBounds.lean` and its child modules `` | | `tex` ×4 "now live in …" sentences | claimed the deleted ℤ^d Λ-layer children among the surviving ones | each names the surviving children and records the ℤ^d Λ-layer deletion | `docs/index.md:1411` (`` `correlation_*_latticeGraph` ``, 17 of 19 survive) and `docs/index.md:1983` are deliberately left alone, as the design determined. The retraction sentences describe the removed wrappers **by layer, never by name**. A first draft named them, and sweep 2 caught it immediately: 11 of the 31 flipped to `published-result` because the retraction itself had become a citation of a declaration about to stop existing. **12 in-library module doc comments** that pointed at the deleted modules were corrected in the same commit: four parent-module "Moved:"/"Removed:" sections (`Magnetization.lean:66`, `PartitionFreeEnergyBounds.lean:102`, `PartitionFreeEnergyMonotonicity.lean:46` and `PartitionFunctionSymmetry.lean:75`) and eight "extracted from `X.lean`" provenance notes. Five of those eight were the basename trap: a same-named module survives under `AmbientLattice/SpecialCases/`, so the reference would silently re-resolve to the wrong file instead of dangling. This closure was not enumerated by the design. ## Ratchet and floor recalibration `scripts/test_dead_candidate_scan.py` * `test_ferromagnetic_family_counts`: `SAFE 47 → 46`, `UNCERTAIN 77 → 78`; `LOAD_BEARING` (64), `PUBLISHED` (35), the 223 total and `test_zero_consumer_count` (112) are unchanged. Exactly one declaration moves, and it moves *away* from `safe-to-delete`: `freeEnergyAlongExhaustion_latticeGraph_nonneg_of_ferromagnetic` `safe-to-delete → uncertain`, because the deleted sibling was the other member of the `nonneg*` component of its family label. The docstring records the mechanism. * Three `docs/index.md` line pins (`1200/1201/1809 → 1192/1193/1801`) shift by the 8 removed bullet lines. Same three rows, different numbers. `scripts/test_audit_gate.py` — **the floors are not lowered.** | counter | `fd7a2a71` | this PR | floor | slack | |---|---|---|---|---| | `iter_checked_files()` | 1993 | 1984 | `CHECKED_FILE_FLOOR` 1957 | 27 | | `iter_lib_files()` | 1986 | 1977 | `LIB_FILE_FLOOR` 1950 | 27 | | `iter_v4_files()` | 2023 | 2014 | `V4_FILE_FLOOR` 1977 | 37 | The comment block claimed *"Measured 2026-07-27 … `iter_checked_files()` = 2003 and `iter_lib_files()` = 1996 … The floors sit 46 below the measured counts"*. Both halves were wrong: 2003/1996 were the counts from *before* PR #4751 deleted its ten modules, so on `fd7a2a71` the real gap was 36, not 46. The block is rewritten against the fresh measurement, and it now records the standing decision that **the next batch that would actually trip a floor must land F1 (per-directory assertions) rather than another recalibration.** A follow-up commit fixes one figure the rewritten block had carried over unchanged: the largest library directory is `Concrete` **851**, not 869. 869 predates PR #4751's ten-module deletion (859 at `fd7a2a71`). Re-measured on this branch, the eight largest are `Concrete` 851, `AmbientLattice` 275, `ClusterExpansion` 205, `TransferMatrix` 109, `Peierls` 105, `AmbientComplexAnalyticity` 76, `Inequalities` 71, `Conditioning` 48 — so the block's claim survives the correction: losing the smallest of the eight takes `iter_checked_files()` from 1984 to 1936, below `CHECKED_FILE_FLOOR` 1957. `scripts/audit/citation_baseline.tsv` — 4 rows hand-moved from `AMBIGUOUS` to `BASENAME_ONLY` (`MayerFilterConnected.lean`, `MayerVdBounds.lean` ×2, `PartitionFreeEnergyRegularity.lean`, `PartitionFunctionGeneralAnalyticity.lean`). Deleting one of two files that share a basename makes the tex citation resolve uniquely, which is a class change, not erosion: **gating findings stay at 960**. `--update-baseline` refuses a row that rises and directs the change to a hand edit so the diff shows it, which is what this is. ## Verification, all re-measured here | gate | result | |---|---| | `lake build` | exit 0, **5006 jobs**, build text grepped: 0 `warning`, 0 `error` (the 2 `info:` `ring` notes are present on `fd7a2a71` too) | | `scripts/audit_gate.py` | PASS — V1 no `axiom` (1984 files), V2 no sorry/admit/native_decide (1984 files), V3 13 capstones all `{propext, Classical.choice, Quot.sound}`, V4 no Japanese (2014 files) | | `grep -rn "sorry" IsingModel/` | 2 hits, both prose inside doc comments, same as `fd7a2a71` | | `lake exe GKSTest` | all tests passed | | `scripts/citation_audit.py` | PASS — 960 gating findings (unchanged), coverage OK, ratchet **0 cleared / 0 new**, tex 1210 raw / 1217 citations, docs 2636 raw / 2700 citations | | `dead_candidate_scan.py --self-test` | **100 tests OK** | | `python3 -m unittest scripts.test_audit_gate` | **166 tests, OK (1 skipped)** | | `citation_audit.py --self-test` | 150 tests OK | | Japanese scan | none in `tex/`, `docs/`, `README.md`, `IsingModel/`, `scripts/` | ## Final check on a synthesized tree A separate throw-away worktree at `fd7a2a71` (**pre-deletion library**) carrying **this commit's** `docs/index.md` and `tex/proof-guide.tex`, scanned with the unmodified scanner: ``` -- published-result: 0 -- -- load-bearing: 0 -- -- uncertain: 0 -- -- safe-to-delete: 31 -- -- coverage warnings: 0 -- canary (unicode self-find): PASS canary (tex line-break): PASS ``` and the full-library sweep on that same tree reports **0 condition-(v) violations**. So the documentation in this commit still justifies deleting exactly these 31 declarations and nothing else. On the merged tree, no exact name among the 31 and none of the five uniquely named deleted modules occurs anywhere in `IsingModel/`, `docs/` or `tex/`. The four shared basenames that remain (`MayerVdBounds.lean`, `MayerFilterConnected.lean`, `PartitionFreeEnergyRegularity.lean`, `PartitionFunctionGeneralAnalyticity.lean`) all resolve to the surviving `AmbientLattice/SpecialCases/` modules. ## Follow-up recorded, not fixed here The three scanner fail-open constructs found while validating this batch are recorded as a child item of #4746 and are deliberately out of scope for this PR: nested braces, a bare trailing `*` with no separating underscore, and `*` read as one-or-more. All three are fail-open on the deletion side, the same polarity class as #4745. The affected sites in this batch were handled by hand and verified by the independent expander above. 🤖 Generated with [Claude Code](https://claude.com/claude-code)
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Summary
Lifts eight abstract
partitionFunction/freeEnergyregularity theorems to the missing along-ex + ℤ^d (Λ + along-ex) layers (Λ-layer wraps already exist via PR #1541, #1533, #1532):partitionFunction_continuous_beta_general_hpartitionFunction_continuous_J_general_hpartitionFunction_differentiable_beta_general_hpartitionFunction_differentiable_J_general_hpartitionFunction_continuous_hpartitionFunction_differentiable_hfreeEnergy_continuous_jointfreeEnergy_differentiable_jointTotal ~24 new thin direct-instantiation wrappers (8 abstracts × 3 missing layers).
Part of #1344.
🤖 Generated with Claude Code