feat: §18.5 vdPolymerFamilies_sum generic-t bound family 4-layer wraps GJ-命題-bundle - #1596
Merged
Merged
Conversation
Lifts the four abstract generic-t bound family theorems (which had no wrappers prior) to all 4 volume layers: - `vdPolymerFamilies_sum_ge_one_of_nonneg` (`1 ≤ vdSum` under `0 ≤ t`, generalises `one_le_vdPolymerFamilies_sum` from tanh) - `vdPolymerFamilies_sum_le_one_plus_pow_of_nonneg` (`vdSum ≤ (1+t)^|E|` under `0 ≤ t`) - `vdPolymerFamilies_sum_pos_of_nonneg` (`0 < vdSum` under `0 ≤ t`, ensures `Real.log (vdSum)` well-defined) - `vdPolymerFamilies_sum_eq_one_add` (`vdSum = 1 + ε(t)` decomposition for the `log(1+ε)` Mayer expansion) Bundle contents: 16 new theorems (4 abstracts × 4 layers). `docs/index.md` §18.5 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 14:16
phasetr
added a commit
that referenced
this pull request
May 11, 2026
Codex cross-check flagged: - AnalyticityLambdaBasicIdentities.lean docstring listed `eq_one_iff_eps_zero` / `gt_one_iff_eps_pos` (not actually moved by this PR). Trim to the two tanh iff wrappers actually present: `tanh_gt_one_iff`, `tanh_eq_one_iff`. - docs/index.md PR #1593 / #1594 entries: redirect Λ-layer location to the new child. PR #1594 entry now explicitly splits the description across the non-tanh `AnalyticityLambdaPolymer.lean` (PR #1979) and tanh `AnalyticityLambdaBasicIdentities.lean` (PR #1986) hosts. - tex/proof-guide.tex PR #1593-#1596 entries: same redirect treatment. Part of #1850. Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
phasetr
added a commit
that referenced
this pull request
May 11, 2026
…pers (#1986) * Initial empty commit for AmbientLattice/Analyticity basic identities + bounds + iff wrappers split Part of #1850 * Split AmbientLattice/Analyticity basic identities + bounds + iff wrappers Move 17 §18.5 Λ-layer wrappers covering basic `at_zero` / `at_one` identities for vdPolymerFamilies_sum / mayerPartialSum / mayerExpansionTerm, tanh iff characterizations (`vdPolymerFamilies_sum_Λ_tanh_{gt_one_iff, eq_one_iff}`), the bound family (`le_two_pow`, `le_one_plus_tanh_pow`, `one_le_vdPolymerFamilies_sum_Λ`), and generic-`t` bounds + `_eq_one_add` decomposition (`ge_one_of_nonneg`, `le_one_plus_pow_of_nonneg`, `pos_of_nonneg`, `eq_one_add`) out of AmbientLattice/Analyticity.lean into a narrow child module AmbientLattice/AnalyticityLambdaBasicIdentities.lean. The parent re-imports the child so the legacy import path and theorem names remain unchanged. Refactor only (no new declarations, no proof changes). Parent file shrinks from 1614 to 1460 lines; new child has 202 lines. Part of #1850. Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com> * Fix codex findings on PR #1986: child docstring scope + stale doc refs Codex cross-check flagged: - AnalyticityLambdaBasicIdentities.lean docstring listed `eq_one_iff_eps_zero` / `gt_one_iff_eps_pos` (not actually moved by this PR). Trim to the two tanh iff wrappers actually present: `tanh_gt_one_iff`, `tanh_eq_one_iff`. - docs/index.md PR #1593 / #1594 entries: redirect Λ-layer location to the new child. PR #1594 entry now explicitly splits the description across the non-tanh `AnalyticityLambdaPolymer.lean` (PR #1979) and tanh `AnalyticityLambdaBasicIdentities.lean` (PR #1986) hosts. - tex/proof-guide.tex PR #1593-#1596 entries: same redirect treatment. Part of #1850. Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com> --------- Co-authored-by: Claude Opus 4.7 <noreply@anthropic.com>
phasetr
added a commit
that referenced
this pull request
Jul 28, 2026
…afe-to-delete batch 3) Deletes ten Z^d thin-wrapper modules under IsingModel/Concrete/LatticeGraphCorrelation/ (39 theorems, 724 lines) whose declarations have no consumer anywhere in the repository, and retracts the eight survival-count claims in docs/index.md and tex/proof-guide.tex that the deletion would otherwise falsify. Measured on this branch: * 39 declarations removed; the whole-tree declaration count moves 10832 -> 10793, so these ten modules account for every removal. * For each of the eight wrapper families, surviving + deleted equals the historical per-PR total, so the historical "PR #N added M wrappers" sentences stay as they are and only the survival counts change: #1582 16 = 12 + 4, #1584 24 = 12 + 12, #1585 16 = 13 + 3, #1586 24 = 20 + 4, #1587 16 = 12 + 4, #1588 16 = 12 + 4, #1589 16 = 12 + 4, #1596 16 = 12 + 4. * lake build: exit 0, 5015 jobs (5025 before), 0 warnings, 0 errors. * audit_gate.py --full: PASS; the observed axiom union stays {propext, Classical.choice, Quot.sound}. * citation_audit.py: PASS, ratchet 0 cleared / 0 new, 960 gating findings. * dead_candidate_scan.py --self-test: 100 tests OK; fixtures PASS (18 rows). * lake exe GKSTest: all tests passed. * Re-scanning the 39 names against the pre-deletion library overlaid with the retracted docs/tex keeps all 39 at safe-to-delete, with published-result, load-bearing and uncertain at 0 and no coverage warning. scripts/test_audit_gate.py carried a bare 2000 literal at three visited-list assertions, which the named floors did not describe: iter_checked_files() moves 2003 -> 1993 and trips it. The literal gives way to the named floors, with a new V4_FILE_FLOOR = 1977 calibrated 46 below the measured iter_v4_files() = 2023, the same offset the two existing floors use. The two homonym basenames under AmbientLattice/SpecialCases/ are untouched. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
phasetr
added a commit
that referenced
this pull request
Jul 28, 2026
…afe-to-delete batch 3) (#4751) ## Summary Deletes ten `ℤ^d` thin-wrapper modules under `IsingModel/Concrete/LatticeGraphCorrelation/` — **39 theorems, 724 lines** — whose declarations have no consumer anywhere in the repository, and retracts in the same commit the eight survival-count claims in `docs/index.md` and `tex/proof-guide.tex` that the deletion would otherwise falsify. The 39 declarations form the `ℤ^d` layer of eight GJ §18.4–18.5 wrapper families (Mayer expansion term, `vdPolymerFamilies_sum`, `log_vdPolymerFamilies_sum`, the Mayer identity and `polymerFreeEnergy_eq_mayerPartialSum` edge-case slices, and the generic-`t` bound family), so this is one logical layer rather than a set of unrelated lemmas. ## Deleted modules | module | thm | |---|---| | `MayerAnalyticityTanhExpansionTerm.lean` | 4 | | `MayerEdgeCasesAlongExIdentity.lean` | 4 | | `MayerEdgeCasesLambdaPolymer.lean` | 4 | | `MayerVdBoundsAlongExNonneg.lean` | 4 | | `MayerVdRegularityExpansionTerm.lean` | 4 | | `MayerVdRegularityPolymer.lean` | 3 | | `MayerVdRegularityPolymerTanh.lean` | 4 | | `MayerVdRegularityTanhExpansionTermAlongEx.lean` | 4 | | `MayerVdRegularityTanhExpansionTermLambda.lean` | 4 | | `VdPolymerFamiliesAnalyticityLog.lean` | 4 | Two umbrella modules (`Umbrella/MagnetizationAndMayer.lean`, `Umbrella/TwoPointUniform.lean`) drop the ten import lines; eight surviving sibling modules have their `Moved:` doc-comment blocks corrected. ## Documentation retraction `docs/index.md` (8 sentences) and `tex/proof-guide.tex` (8 `\paragraph` blocks) each claimed these families sit at "all 4 volume layers". Both were re-measured on this branch with a line-spanning-aware declaration extractor — a `^theorem <name>` grep misses the 615 declarations in this repository whose name sits on a later line — and rewritten to the measured survival counts: | family | historical | surviving | deleted | surviving layers | |---|---|---|---|---| | #1582 `mayerExpansionTerm` regularity | 16 | **12** | 4 | Λ 4, AlongEx 4, ℤ^d Λ 2, ℤ^d AlongEx 2 | | #1584 `mayerExpansionTerm` tanh β/J | 24 | **12** | 12 | Λ 6, AlongEx 6 | | #1585 `vdPolymerFamilies_sum` regularity | 16 | **13** | 3 | Λ 4, AlongEx 4, ℤ^d Λ 1, ℤ^d AlongEx 4 | | #1586 `vdPolymerFamilies_sum` tanh β/J | 24 | **20** | 4 | Λ 6, AlongEx 6, ℤ^d Λ 2, ℤ^d AlongEx 6 | | #1587 `log_vdPolymerFamilies_sum` analyticity | 16 | **12** | 4 | Λ 4, AlongEx 4, ℤ^d AlongEx 4 | | #1588 `mayer_identity_at_*` | 16 | **12** | 4 | Λ 4, AlongEx 4, ℤ^d Λ 4 | | #1589 `polymerFreeEnergy_eq_mayerPartialSum_at_*` | 16 | **12** | 4 | Λ 4, AlongEx 4, ℤ^d AlongEx 4 | | #1596 `vdPolymerFamilies_sum` generic-`t` bounds | 16 | **12** | 4 | Λ 4, AlongEx 4, ℤ^d Λ 4 | Two independent consistency checks hold: surviving + deleted equals the historical per-PR total in every row, and the deleted column sums to 39, which equals the whole-tree declaration delta (10832 → 10793). The ten modules therefore account for every removal, and the historical "PR #N added M wrappers" sentences are correct as they stand — only the survival counts move. The retraction text names families by label (`mayer_identity_at_*`) rather than spelling out deleted declarations, and cites no deleted module path, so it adds no dangling citation. Every module path it does cite was checked to exist. ## Gates (all measured on this branch) | gate | result | |---|---| | `lake build` | exit 0, **5015 jobs** (5025 before, matching the ten deletions), 0 warnings, 0 errors | | `#print axioms` | unchanged; observed union `{propext, Classical.choice, Quot.sound}` | | `grep -rn "sorry" IsingModel/` | 0 tactic occurrences (2 hits are prose in doc comments) | | `citation_audit.py` | PASS, ratchet **0 cleared / 0 new**, 960 gating findings, coverage OK | | `dead_candidate_scan.py --self-test` | **100 tests OK**; fixtures PASS (18 rows) | | `python3 -m unittest scripts.test_audit_gate` | **166 tests OK** (1 skipped) | | `lake exe GKSTest` | `=== All tests passed ===` | | Japanese in `docs/index.md` / `tex/proof-guide.tex` | 0 | Final cross-check, re-scanning the 39 names against the **pre-deletion library overlaid with this commit's retracted docs/tex**: **safe-to-delete 39/39**, with `published-result`, `load-bearing` and `uncertain` all **0** and **0 coverage warnings**; both scanner canaries PASS. This is the check that would catch a retraction sentence accidentally citing a declaration that is being removed. The three Markdown backtick-parity warnings at `docs/index.md:1200/1201/1809` predate this branch and are unchanged. ## Ratchet `iter_checked_files()` 2003 → 1993 and `iter_lib_files()` 1996 → 1986, against floors 1957 / 1950, leaving slack 36. Module counts under both pathspec conventions: `IsingModel/*.lean` 1996 → 1986 (the full count) and `IsingModel/**/*.lean` 1957 → 1947 (the undercount that drops the 39 depth-1 modules). Four visited-list assertions in `scripts/test_audit_gate.py` — three in `ScanExecutionTest`, one in `V4ScanTest` — carried a bare `2000` literal that the named floors did not describe, so `iter_checked_files()` at 1993 trips it — this surfaced only when the deletion was applied. The literal gives way to the named floors, with a new `V4_FILE_FLOOR = 1977` calibrated 46 below the measured `iter_v4_files()` = 2023, the same offset the two existing floors use. Slack narrows to 36 with this batch, so a per-directory assertion or a floor recalibration is worth a look before the slack absorbs further batches. ## Build-time effect Per-module process cost was measured at **2.144 s wall / 2.156 s CPU** (warm cache, 10 modules × 2 passes, minus the `lake env` wrapper), giving **≈21.6 s CPU** for the ten modules. The wall figure is a serial extrapolation, not a parallel measurement; a warm-cache full build differs only by trace replay, so the saving shows up in clean and CI builds. ## Scope note The two homonym basenames that also exist under `AmbientLattice/SpecialCases/` (`MayerVdRegularityExpansionTerm.lean`, `VdPolymerFamiliesAnalyticityLog.lean`) are untouched, as is the ambient import at `VdPolymerFamiliesAnalyticityLogAlongEx.lean`. No file under `AmbientLattice/` is modified. Part of the safe-to-delete sweep tracked in #4746, following batches 1 (#4747) and 2 (#4749). ## Review follow-up (commit `3f77b982`) Two review findings, both about prose that named the wrong thing. No Lean source is touched by this commit. **Survival-location module names (`tex/proof-guide.tex`).** Six wrapper-family paragraphs pointed readers at modules that do not hold the declarations they claim. Each name below is the module that a scan of every `theorem`/`lemma` head under `IsingModel/` puts the surviving declarations in (the scan reads the name off the next line when the head wraps, which a single-line grep misses): | Family | Claimed | Measured | | --- | --- | --- | | #1589 ℤ^d | `Concrete/LatticeGraphCorrelation/MayerEdgeCases.lean` | `Concrete/LatticeGraphCorrelation/MayerEdgeCasesAlongExPolymer.lean` | | #1588 ℤ^d | `Concrete/LatticeGraphCorrelation/MayerEdgeCases.lean` | `Concrete/LatticeGraphCorrelation/MayerEdgeCasesLambda.lean` | | #1587 along-ex | `AmbientLattice/SpecialCases/VdPolymerFamiliesAnalyticity.lean`, `Concrete/…/VdPolymerFamiliesAnalyticity.lean` | `AmbientLattice/SpecialCases/VdPolymerFamiliesAnalyticityLog.lean` (+ `…LogTanh.lean`), `Concrete/…/VdPolymerFamiliesAnalyticityLogAlongEx.lean` | | #1586 Cont./Diff. | `AmbientLattice/SpecialCases/MayerVdRegularity.lean`, `Concrete/…/MayerVdRegularity.lean` | `AmbientLattice/SpecialCases/MayerVdRegularityVdPolymerTanh.lean` (+ `…TanhDifferentiable.lean`), `Concrete/…/MayerVdRegularityPolymerTanhAlongEx.lean` | | #1586 AnalyticAt | `VdPolymerFamiliesAnalyticity.lean` (both sides) | `VdPolymerFamiliesAnalyticityTanh.lean` (both sides) | | #1585 Cont./Diff./HasDerivAt | `AmbientLattice/SpecialCases/MayerVdRegularity.lean`, `Concrete/…/MayerVdRegularity.lean` | `AmbientLattice/SpecialCases/MayerVdRegularityVdPolymer.lean` (+ `…VdPolymerHasDerivAt.lean`), `Concrete/…/MayerVdRegularityPolymerAlongEx.lean` | | #1582 Cont./Diff. | `AmbientLattice/SpecialCases/MayerVdRegularity.lean` | `AmbientLattice/SpecialCases/MayerVdRegularityExpansionTerm.lean` (+ `MayerVdRegularityDifferentiableExpansionTerm.lean`) | | #1582 ℤ^d analytic | `Concrete/LatticeGraphCorrelation/MayerAnalyticity.lean` | `Concrete/LatticeGraphCorrelation/MayerAnalyticityExpansionTerm.lean` | `Concrete/LatticeGraphCorrelation/MayerEdgeCases.lean` carries zero declarations after this batch, so the first two rows pointed at an empty signpost module. `docs/index.md` was not already right either, contrary to the premise the review worked from: its #1582 ℤ^d analytic name, its #1586 AnalyticAt names and its #1587 along-exhaustion name were the same stale names, and its #1585/#1586 "`MayerVdRegularity.lean` cluster" phrasing named no member of that cluster. Those five spots move to the measured modules, so docs and tex now say the same thing. **Stale comment (`scripts/test_audit_gate.py`).** The comment above `V4_FILE_FLOOR` said the bare `2000` literal had sat at "three sites" in `ScanExecutionTest` and `V4JapaneseTest`. It sat at four — three in `ScanExecutionTest`, one in `V4ScanTest` — and `V4JapaneseTest` is not a class in this file. Comment only; the code and the floor values are unchanged. **Verification of this commit.** * `citation_audit.py`: PASS, 960 gating findings, ratchet 0 cleared / 0 new, coverage OK. The per-target citation census moves 1216 → 1217 (tex) and 2693 → 2700 (docs), because one generic module name gives way to the two or three exact ones; the census is a deletion budget and gates only downwards, and every added path resolves. * `python3 -m unittest scripts.test_audit_gate`: 166 tests OK (1 skipped). * `dead_candidate_scan.py --self-test`: 100 tests OK. * No Japanese in `tex/proof-guide.tex`, `docs/index.md` or the edited script. **Left alone, and why.** Three survival-location claims outside the six reviewed paragraphs remain stale and are unchanged here, since correcting them means asserting provenance this commit did not measure: `#1582`'s Λ-layer sentence points at `IsingModel/AmbientLattice/Analyticity.lean` while `mayerExpansionTerm_Λ_*` sit in `AnalyticityLambdaMayer.lean` (created by #1983); the `#1587` paragraph opens with a sentence naming `Analyticity.lean` and `Concrete/LatticeGraphCorrelation.lean` that its own next sentence contradicts; and the `#1581`/`#1583`/`#1584` paragraphs use the same bare `MayerVdRegularity.lean` shorthand. ## Independent audit (dev-audit-tier1, re-measured on `3f77b982`) Every number in the tables above was re-run in a throw-away worktree with a cloned build cache, and two corrections were folded into this message. * `lake build`: exit 0, **5015 jobs**, `grep -ic warning` = 0, `grep -ic error` = 0. The pre-deletion tree at `b09535cd` builds **5025 jobs** in the same setup, so the delta is exactly the ten modules. * `grep -rn "sorry" IsingModel/`: **2** prose hits, not 4 (the table above said 4); both are doc-comment sentences and are identical on `b09535cd`. No tactic occurrence. `native_decide`: 1 prose hit. `admit`: prose only. Zero `axiom` declarations. * `#print axioms` on four capstones (`mayer_identity_at_zero_Λ_latticeGraph`, `mayerExpansionTerm_Λ_latticeGraph_analyticAt`, `log_vdPolymerFamilies_sumAlongExhaustion_latticeGraph_analyticAt`, `exists_cubicMayerClusterFreeEnergyComplex_limit`): `[propext, Classical.choice, Quot.sound]` only. * `citation_audit.py`: PASS, 960 gating findings, ratchet 0 cleared / 0 new, coverage OK, census 1216 -> 1217 (tex) and 2693 -> 2700 (docs). * `dead_candidate_scan.py --self-test`: 100 tests OK. `python3 -m unittest scripts.test_audit_gate`: 166 tests OK (1 skipped). `lake exe GKSTest`: all tests passed. * Deletion-safety, re-derived independently: the ten modules hold **39** declarations; at `b09535cd` none of the 39 names occurs anywhere outside those ten files (`IsingModel/`, `docs/`, `tex/`, `scripts/`, `test/`), and at `3f77b982` none occurs at all. Re-scanning the 39 against the pre-deletion library overlaid with this commit's docs/tex reproduces **safe-to-delete 39**, `published-result` 0, `load-bearing` 0, `uncertain` 0, coverage warnings 0, both canaries PASS. * **`dead_candidate_scan.py --lean`** (requirement (i) of #4746 Item A, not reported in the body above) was run against a green pre-deletion build: *39 candidates compared against the elaborated graph; no consumer seen by Lean was missed on a safe-to-delete verdict*. * Ratchet re-measured: `iter_checked_files()` 2003 -> 1993, `iter_lib_files()` 1996 -> 1986, `v4_visited` 2033 -> 2023, against floors 1957 / 1950 / 1977 (slack 36 / 36 / 46). * Scope: no file under `AmbientLattice/` is touched; both homonym basenames survive and are still imported; `docs/index.md` and `tex/proof-guide.tex` retain no `Concrete/LatticeGraphCorrelation/` citation of any deleted module; no `Lemma_17_5_2` path is touched (#4746 Item B stays `USER-DECISION`); no Japanese, no added declaration, no long line, no credential-shaped string in the diff. * Informational: the scanner's cascade list shows **30** ambient/abstract declarations that become reference-0 as a consequence of this batch (16 in `AmbientLattice/SpecialCases/`, 8 in `AnalyticityLambdaMayer.lean`, 6 abstract GJ Sec 18 statements in `ClusterExpansion/MayerCore/Terms.lean`). They are correctly left in place here; recorded on #4746 so a later batch does not cascade into book content. 🤖 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 the generic-
t(non-tanh) bound family forvdPolymerFamilies_sumto all 4 volume layers (Λ-direct, along-exhaustion, ℤ^d Λ-direct, ℤ^d along-exhaustion). Plus the polynomial identity_eq_one_adddecomposition.Bundle contents:
vdPolymerFamilies_sum_ge_one_of_nonneg× 4 layersvdPolymerFamilies_sum_le_one_plus_pow_of_nonneg× 4 layersvdPolymerFamilies_sum_pos_of_nonneg× 4 layersvdPolymerFamilies_sum_eq_one_add× 4 layersTotal ~16 new thin direct-instantiation wrappers (4 abstracts × 4 layers).
Part of #1344.
Test plan
lake buildclean (zero linter warnings)grep -rn "sorry" IsingModel/= 0lake exe GKSTestpassesdocs/index.md§18.5 row updatedtex/proof-guide.texparagraph added🤖 Generated with Claude Code