feat(gj-17.1): §18 cluster expansion supersedes the transfer-matrix infinite-volume gap — #4214 (B-ii) by phasetr · Pull Request #4228 · phasetr/ising-model

phasetr · 2026-06-22T16:12:47Z

Part of #4214

Summary

Issue #4214 item B, option (ii): formalize the explicit statement that the §18
cluster-expansion route supersedes the obstructed transfer-matrix
transverse-volume-uniform spectral-gap route (option (i), a documented obstruction —
single-step Dobrushin/Doeblin insufficient; Codex counterexample u≡1, k=exp(t·∑ab),
ρ~exp(O(|S|)); roadmap Phase 5).

New module IsingModel/TransferMatrix/ClusterExpansionSupersession.lean:

clusterExpansion_supersedes_transferMatrix_gap — for every d ≥ 1, J > 0 there is a
single high-temperature threshold β₀ > 0 (= min β₁ (1/(J·2d)), β₁ the analyticity radius)
on which the infinite-volume ℤ^d Ising model simultaneously has, via the cluster expansion:

(a) No phase transition — freeEnergyInfinite, internal energy ∂_β f, specific heat
∂_β² f all AnalyticOnNhd ℝ on (0, β₀) (from exists_high_temp_no_phase_transition,
§18.6, KP discharged from Δ²e|t| < 1/6, transferred to the smaller interval by
AnalyticOnNhd.mono); and
(b) A mass gap — for every β ∈ (0, β₀), exponential two-point decay with positive rate
−log(βJ·2d) (from hasExponentialDecay_latticeGraph_of_betaJ_two_d_lt_one, §18.7,
Simon–Lieb; β < 1/(J·2d) is exactly βJ·2d < 1).

These are precisely the infinite-volume high-temperature payoffs a transverse-uniform
transfer-matrix spectral gap aimed to produce, obtained here with no spectral-gap hypothesis.
The obstruction of option (i) is therefore no longer an obstacle to the infinite-volume
high-temperature theory.

Verification

lake build (5585 jobs) ✓
lake exe GKSTest ✓
linter warnings: zero on the new module
axiom-free: [propext, Classical.choice, Quot.sound]

Docs

docs/index.md: §17.1/§18.6–18.7 supersession row.
tex/proof-guide.tex: supersession section (compiles, no new warnings; no Japanese).

🤖 Generated with Claude Code

… (issue #4214 B-ii) -- #4214

…nfinite-volume gap — #4214 (B-ii) Issue #4214 item B, option (ii): formalize the explicit statement that the §18 cluster-expansion route supersedes the obstructed transfer-matrix transverse-volume-uniform spectral-gap route. New module `TransferMatrix/ClusterExpansionSupersession.lean`: `clusterExpansion_supersedes_transferMatrix_gap` — for every `d ≥ 1`, `J > 0` there is a single high-temperature threshold `β₀ > 0` (`= min β₁ (1/(J·2d))`) on which the infinite-volume `ℤ^d` Ising model simultaneously has, via the cluster expansion: - (a) no phase transition: `freeEnergyInfinite`, `∂_β f`, `∂_β² f` all `AnalyticOnNhd ℝ` on `(0, β₀)` (from `exists_high_temp_no_phase_transition`, §18.6, transferred via `AnalyticOnNhd.mono`); and - (b) a mass gap: for every `β ∈ (0, β₀)` exponential two-point decay with positive rate `−log(βJ·2d)` (from `hasExponentialDecay_latticeGraph_of_betaJ_two_d_lt_one`, §18.7). These are exactly the infinite-volume high-temperature payoffs the transfer-matrix transverse-uniform spectral gap aimed at; the bundling records that the cluster-expansion route obtains them with no spectral-gap hypothesis, so the documented obstruction of option (i) is no longer an obstacle. Axiom-free. Docs: docs/index.md §17.1/§18.6–18.7 supersession row; tex/proof-guide.tex supersession section. Part of #4214 Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>

…ws superseded Comprehensive re-audit (book + all code) findings and fixes: - Confirmed: zero sorry / admit / native_decide in library theorems; exactly TWO declared axioms (FunctionTheory.vitaliPorter_tendstoLocallyUniformlyOn, Ambient.lemma_17_5_2_derivativeLimitProvider_latticeGraph), both documented, isolated, scope-excluded analytic (normal-families) inputs. - README Formalization status: now records the two scope-excluded axioms (precise role + reason out of scope) and the book-order completeness of the §17–18 programme — previously the README said only "zero sorry" and omitted the axioms. - docs/index.md progress table: the only remaining "Partial"-status rows were the ~34 §17.1 Issue #3511 transfer-matrix transverse spectral-gap scaffolding rows. That route was PROVEN OBSTRUCTED (#4081) and SUPERSEDED by the §18 cluster-expansion route (#4228, option ii); the infinite-volume mass-gap / no-phase-transition conclusion is Done via #4228/#4255. Each such row is now marked "Superseded — … conditional scaffolding only, not an open book gap", so the table no longer reads as if these were open gaps. No genuine Partial book gap remains. Docs-only change (README.md, docs/index.md); no Lean/theorem changes. Part of #4214 (final book-order completeness bookkeeping). Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>

…superseded (#4279) * chore(docs): scaffold axiom-status README + §17.1 supersession cleanup * docs: record axiom status in README; mark §17.1 #3511 spectral-gap rows superseded Comprehensive re-audit (book + all code) findings and fixes: - Confirmed: zero sorry / admit / native_decide in library theorems; exactly TWO declared axioms (FunctionTheory.vitaliPorter_tendstoLocallyUniformlyOn, Ambient.lemma_17_5_2_derivativeLimitProvider_latticeGraph), both documented, isolated, scope-excluded analytic (normal-families) inputs. - README Formalization status: now records the two scope-excluded axioms (precise role + reason out of scope) and the book-order completeness of the §17–18 programme — previously the README said only "zero sorry" and omitted the axioms. - docs/index.md progress table: the only remaining "Partial"-status rows were the ~34 §17.1 Issue #3511 transfer-matrix transverse spectral-gap scaffolding rows. That route was PROVEN OBSTRUCTED (#4081) and SUPERSEDED by the §18 cluster-expansion route (#4228, option ii); the infinite-volume mass-gap / no-phase-transition conclusion is Done via #4228/#4255. Each such row is now marked "Superseded — … conditional scaffolding only, not an open book gap", so the table no longer reads as if these were open gaps. No genuine Partial book gap remains. Docs-only change (README.md, docs/index.md); no Lean/theorem changes. Part of #4214 (final book-order completeness bookkeeping). Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com> --------- Co-authored-by: Claude Opus 4.8 (1M context) <noreply@anthropic.com>

… scaffolding (~6.6k lines) — #4298 PR-B1 (#4303) The §17.1 transverse spectral-gap route was proven OBSTRUCTED (#4081) and is SUPERSEDED by the §18 cluster-expansion route (#4228/#4255), documented in `TransferMatrix/ClusterExpansionSupersession.lean` (kept). Per author decision (#4298), remove the now-superseded spectral-gap construction scaffolding. **Scope correction (transparency):** my initial closure estimate of "46 files / 9,314 lines" conflated genuine standalone §17.1 1D-Ising results with the spectral-gap scaffolding. After classifying by doc status + dependency on the obstructed spectral core, the accurate scaffolding set is **30 files / ~6,566 lines** — the Layer* spectral machinery (Dobrushin/Doeblin/Doob contraction, Perron, quadratic-form Gershgorin/deflation, top-deflation, projective diameter, cylinder/infinite/high-temperature spectral windows). The remaining **16 standalone files are KEPT** as live terminal 1D-Ising results per #4298's keep-caveat: `OneDimField{,Magnetization,Power,Susceptibility}`, `OneDimGibbsFreeEnergy`, `GibbsTwoPoint{,Decay}`, `CubicLayerOpenBox*`, `FreeLayerWalshOpenAxis*`, `MarkedTrace1D`, `LayerOpenExplicitSubdominantRatio`, `LayerOpenFiniteTransverseHermitian`, `OneSiteLayerOpenBoundaryWindow`. None of the 16 imports any of the 30 (verified). The 30 form a closed import island reachable only via the root catch-all umbrella; the live 61-file 1D-Ising closure and the supersession record do not import them. Removed their 30 root-umbrella import lines. Doc-sync: per the author's "keep the Partial/Superseded record rows" choice, the docs/index.md and tex/proof-guide.tex rows describing these lemmas are RETAINED as the historical obstruction record, with their now-stale `TransferMatrix/*.lean` file references replaced by an archive marker pointing to the git tag. Pre-deletion state archived at git tag `archive/transfermatrix-spectral-gap-scaffolding`. Verification: `lake build` green (5560 → 5530 jobs, −30); `lake exe GKSTest` pass; no `sorry`/`admit`/`native_decide` in library theorems; `latexmk` clean, no Japanese; no dangling reference to any deleted module/decl in surviving Lean files; `#print axioms` unchanged on the capstones (`peierls_spontaneous_magnetization_pos_cubic`, `correlationInfinite_latticeGraph_two_point_analytic_high_temp`) = [propext, Classical.choice, Quot.sound]. Part of #4298. Co-authored-by: Claude Opus 4.8 (1M context) <noreply@anthropic.com>

…index.md:1715 ## What `docs/index.md:1715` cites `TransferMatrix/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 commit `109690bd` (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_gap` in `IsingModel/TransferMatrix/ClusterExpansionSupersession.lean:77`, which **still exists**. Only the supplementary 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 a citation fix, **not a retraction, and no progress claim changes**. ## Scope Exactly one line in `docs/index.md`. No Lean change, no `tex/` change, no progress-claim change. **Explicitly out of scope, awaiting user authorization**: `docs/index.md:1974` overstates wrapper counts (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 build` exits 0 with 5040 jobs and zero warnings (no Lean file changed, so the build replays from cache). - `docs/index.md` no longer references `LayerDobrushinContraction`, `LayerDoeblin`, or `LayerDoobSpectralGap`: zero matches. - `clusterExpansion_supersedes_transferMatrix_gap` is confirmed present at `IsingModel/TransferMatrix/ClusterExpansionSupersession.lean:77`, and the two declarations it cites are confirmed present: `exists_high_temp_no_phase_transition` at `HighTempAnalyticityCapstone.lean:143` and `hasExponentialDecay_latticeGraph_of_betaJ_two_d_lt_one` at `HighTempMassGap.lean:269`. - The inserted annotation is verbatim-identical to the annotation already present on 30 other rows in main (base: 31 occurrences; head: 32 occurrences). - The diff of progress claims (`**Done (...)**` cell text and counts) is empty. - The diff is confined to `docs/index.md`, one file, one line changed (1 insertion / 1 deletion). - `docs/index.md:1974` is unchanged: the wrapper-count correction (8→6 / 12→10) awaiting authorization is untouched. - Zero CJK character intrusion in `docs/index.md`. - `dev-review` and codex both returned APPROVE; `dev-audit-tier1` re-audit PASS. - CI `build` check passed in 3m28s at `63088fc3`. 🤖 Generated with [Claude Code](https://claude.com/claude-code) Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>

…cstring The module docstring named three transfer-matrix scaffolding files (LayerDobrushinContraction.lean, LayerDoeblin.lean, LayerDoobSpectralGap.lean) that were removed in PR-B1 (#4303). Replace the dangling names with the same removal note used throughout docs/index.md: PR-B1, obstruction #4081, superseded by §18 #4228/#4255, archived at git tag archive/transfermatrix-spectral-gap-scaffolding. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>

…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>

… PR-4) (#4743) `scripts/citation_audit.py` reported `MISSING=12` on `docs/index.md` at main `32f6afa5` -- 12 occurrences over 9 distinct tokens, listed by `python3 scripts/citation_audit.py --format tsv | grep -P '^MISSING\t'`. This PR takes that class to 0. It edits 11 lines of `docs/index.md` and regenerates `scripts/audit/citation_baseline.tsv` with `--update-baseline`. No Lean source is touched, so no build was run. The scope is the `MISSING` class only. `AMBIGUOUS` (107) and `BASENAME_ONLY` (624) on this document are untouched and unchanged; nothing here is a claim about them. ## (a) Two citations that never named a real path (lines 1915, 1916) `MassContinuityFiniteVolumeDerivCombine/BindingPairDeriv.lean` and `MassContinuityFiniteVolumeIncidentEdge/IncidentSum/DerivCombine/DerivSharp/BindingPairDeriv.lean` are **not** stale references to files that were deleted. **No path with a `MassContinuity*/` directory component has ever existed in this repository**: ``` git log --all --pretty=format: --name-only \ | grep -oE '[^/]*MassContinuity[^/]*/' | sort -u # empty ``` They are slash-joined lists of flat basenames -- a docs-authoring bug at the time the two rows were written, which never resolved on any commit. Which flat modules were meant is fixed by the authoring commits' own file lists, not by guesswork: | row | authoring commit | its `MassContinuity*` files | now cited | |---|---|---|---| | 1915 | `bd84f731` (PR #4383) | SharpRFactor, FiniteVolumeUniformCombine, FiniteVolumeUniformPowDeriv (the three the row already cited) + **FiniteVolumeDerivCombine, FiniteVolumeBindingPairDeriv** | the latter two, as `Lemma_17_5_2/...` | | 1916 | `cd7e6ca8` (PR #4382) | DenomRatioGeneral, ConvolutionMassUniformDart (the two the row already cited) + **FiniteVolumeIncidentEdge, FiniteVolumeIncidentSum, FiniteVolumeDerivCombine, FiniteVolumeDerivSharp, FiniteVolumeBindingPairDeriv** | those five, as `Lemma_17_5_2/...` -- matching the row's own words "all five FV files" | Cross-check on row 1915: `grep -c _core` over the five candidate modules gives 2 hits in `MassContinuityFiniteVolumeDerivCombine.lean` (`combined_derivative_div_c_bound_core_finiteRegionFV`, declared there) and 2 in `MassContinuityFiniteVolumeBindingPairDeriv.lean` (`pseudoMassFromParamsAtPairFV_pow_succ_hasDeriv_abs_le_binding_core`, declared there); the other three give 0 (`SharpRFactor`), 1 (`FiniteVolumeUniformCombine`, a *call site* of the DerivCombine `_core` lemma) and 1 (`FiniteVolumeUniformPowDeriv`, a call site of the BindingPairDeriv `_core` lemma) -- so the row's "`_core` refactors of ..." still names exactly the two modules that *declare* a `_core` lemma (`FiniteVolumeDerivCombine`, `FiniteVolumeBindingPairDeriv`); the other two non-zero counts are downstream call sites, not declarations. All 7 added tokens use the directory-qualified `Lemma_17_5_2/<module>.lean` form already used at line 2000, and each is a component-aligned suffix of exactly one tracked path (checked against `git ls-files`), so all 7 land in `RESOLVED` rather than adding a new `BASENAME_ONLY` finding. ## (b) Seven archival notes, reworded (10 occurrences) Each already read as deletion history inside a row whose evidence is a different, still-tracked file. The wording follows conventions already in this repository for a removed module -- name the removing commit, and the archive tag where one exists, instead of spelling a path that no longer resolves: * `tex/proof-guide.tex:3530-3543` (the ray-exit archival note: commit hash, `git tag`, tree hash, no `.lean` basename); * `docs/index.md`, 31 rows between lines 1598 and 1715 (32 occurrences of `scaffolding removed in PR-B1`) of the form "_(scaffolding removed in PR-B1: route obstructed #4081, superseded by §18 #4228/#4255; archived at git tag `archive/transfermatrix-spectral-gap-scaffolding`)_", several of them in **Done** rows; * the `removed PR #4297; not archived --- the axiom it declared is discharged` form installed by PR #4736; * the retiring commits' own phrasing ("retired the standalone `HLSBridgeSummary` wrapper module", "retire `AmbientLattice.SpecialCases.Legacy` shim"), which is the module name without the `.lean` extension. | line(s) | token (occurrences) | removing commit (verified by `git show --name-status --diff-filter=D`) | rewording | |---|---|---|---| | 866 | `RayExitAnchorVerticalStrictBridgeNonStripTurnStep.lean` (1) | `2499fd8c` (PR #4299, Issue #4298) | "incl. the 49,402-line `X.lean`" -> "the largest single module 49,402 lines"; the row now also names commit `2499fd8c` and the tag's `IsingModel/Peierls` tree | | 1977, 1982, 1983 | `SpecialCases/Legacy.lean` (3) | `2559040c` (PR #2561) | "`SpecialCases/Legacy.lean`" -> "the `AmbientLattice.SpecialCases.Legacy` shim", plus a one-off note at 1977 | | 1979, 1982 | `Concrete/LatticeGraphCorrelation/Legacy.lean` (2) | `bb21e4b1` (PR #2562) | "`Concrete/LatticeGraphCorrelation/Legacy.lean`" -> "the `Concrete.LatticeGraphCorrelation.Legacy` shim", plus a one-off note at 1979 | | 2000 | `SharpHLSScopeExcludedAxioms.lean` (1) | `a8556e58` (PR #4297) | "deleted `X.lean`" -> "deleted the module that declared it, `Lemma_17_5_2.SharpHLSScopeExcludedAxioms`, in commit `a8556e58`; that module is not archived -- the axiom it declared is discharged" | | 2010 | `HLSConsolidatedSummary.lean` (1) | `2c613b1f` | "the former standalone `X.lean` wrapper module is retired" -> "... `X` wrapper module is retired, absorbed in commit `2c613b1f`" | | 2012 | `HLSSusceptibilityBridge.lean` (1) | `db51c080` | same shape, commit `db51c080` | | 2019 | `HLSBridgeSummary.lean` (1) | `fa2771b1` | same shape, commit `fa2771b1` | Two things worth flagging, because a name alone would have been wrong: * The three HLS absorptions each appear **twice** in `git log --all` (`34228fb6`/`fa2771b1`, `bbb34e31`/`2c613b1f`, `8a76e6c4`/`db51c080`) with the **same subject line** each time (author dates differ across all three pairs -- e.g. `fa2771b1` is 3.5 minutes after `34228fb6`; `bbb34e31`/ `2c613b1f` also differ in tree). `git merge-base --is-ancestor` says only `fa2771b1`, `2c613b1f`, `db51c080` are ancestors of `main`; those are the hashes cited. * The **local and the remote `archive/peierls-rayexit-route` tags peel to different commits** (`a8556e58` locally, `c65dc50c` on `origin`). Both carry the same `IsingModel/Peierls` tree `6bb634dce91e68b985196d92ad45e61bec6bf2b1`, so line 866 cites the tag together with that tree hash rather than the tag name alone. ## No Done claim is retracted `docs/index.md` has 908 lines matching `grep -c '\*\*Done'` (909 occurrences; 197 bare `**Done**`). Rather than reason about the class, each of the 11 edited lines was inspected individually, and for each the question asked was whether the edited clause is the Done row's evidence or provenance history: | line | status cell | Done-row evidence (still tracked, per `git ls-files`) | edited clause | |---|---|---|---| | 866 | `(archived)` -- not a Done row | n/a | the archived route's own description | | 1915 | `**Done (axiom-free; toward Thm 17.5.1)**` | 3 already-cited modules + the 2 repointed ones | evidence, and it is repointed, not withdrawn | | 1916 | `**Done (axiom-free; toward Thm 17.5.1)**` | 2 already-cited modules + the 5 repointed ones | evidence, repointed, not withdrawn | | 1977 | `**Done (ambient pointwise)**` | `AmbientLattice/SpecialCases/PartitionFreeEnergyPointwiseRegularity.lean` | "moved out of ... in PR #1858" -- provenance | | 1979 | `**Done (ℤ^d along-ex pointwise)**` | the 5 `Concrete/.../PartitionFreeEnergyPointwiseRegularity*` modules | provenance | | 1982 | `**Done (abstract + Λ + along-ex + ℤ^d analytic)**` | `AmbientLattice/SpecialCases/JointAnalyticity.lean`, `Concrete/LatticeGraphCorrelation/JointAnalyticity.lean` | "moved from ... in PR #1860" -- provenance | | 1983 | `**Done (along-ex + ℤ^d analytic joint)**` | `AmbientLattice/SpecialCases/JointAnalyticity.lean` | provenance | | 2000 | `**Done (axiom-free, modulo the per-pair profile hypothesis)**` | `Lemma_17_5_2/SharpHLSCapstone.lean` | "and deleted ..." -- deletion history | | 2010 | `**Done (GJ-proposition-unit, 7 declarations)**` | `Lemma_17_5_2/HLSLatticeMassBridge.lean` | the retired-wrapper parenthetical | | 2012 | `**Done (GJ-proposition-unit, 6 declarations)**` | `Lemma_17_5_2/HLSLatticeMassBridge.lean` | the retired-wrapper parenthetical | | 2019 | `**Done (... 27 selected/canonical declarations ...)**` | `Lemma_17_5_2/HLSBridgeFromSimonLieb.lean` is a 47-line, 0-declaration umbrella (4 `import`s only); the 27 declarations actually live in `HLSBridgeFromSimonLiebCanonical.lean` (23 by `^theorem\|^lemma\|^def` count) plus its sibling `Core`/`Tanh`/`Variants` modules | the retired-wrapper parenthetical | Of the 12, 10 findings (the 7 archival-note occurrences plus 866) touch provenance/deletion-history prose, not the Done row's evidentiary basis; the remaining 2 (rows 1915/1916) *are* evidence, but the edit repoints them to the correct files rather than withdrawing them -- no Done claim loses evidence. The `**Done` counts are unchanged by this diff (908 / 909 / 197 before and after). ## Measured * `citation_audit`, `docs/index.md`: citations 2698 -> 2693 (-5), raw `.lean` occurrences 2633 -> 2628. `RESOLVED` 1955 -> 1962, `MISSING` 12 -> 0 (the class is now empty), `AMBIGUOUS` 107 and `BASENAME_ONLY` 624 unchanged. `tex/proof-guide.tex` untouched (1216 citations, 987/104/125/4). * Gating findings **972 -> 960**; `ratchet: OK -- 12 cleared, 0 new`; `citation audit: PASS`. * R11 per-run deletion budget **134** (`max(25, 5% of the committed 2698)`); this run drops **5**. * R12 cumulative cap **404** (15% of the frozen `MEASURED_CITATIONS["docs/index.md"] = 2698`), floor 2294; live 2693, so 399 of the cap is unused. Neither budget is approached. * Advisory self-references 94 -> 93: the row `SELFREF docs/index.md SpecialCases/Legacy.lean >> SpecialCases/Legacy.lean` (line 1977) goes away with its token. No `SELFREF` row is added. * `scripts/audit/citation_baseline.tsv` regenerated with `python3 scripts/citation_audit.py --update-baseline scripts/audit/citation_baseline.tsv` (no hand edit; the tool reported `judged against 32f6afa...:..., origin/main:..., HEAD:...` and `delta: +0 finding(s), -13 finding(s)` = 12 `MISSING` + 1 `SELFREF`). The `#census` line is updated and **no `first_line` payload shifted**, because every edit is within-line. * `--format tsv` and the committed baseline are **byte-identical** (34,000 bytes each, `cmp` silent). * `python3 scripts/test_citation_audit.py`: **150 tests, OK**. `python3 scripts/citation_audit.py --self-test`: **11 consecutive runs, 150 tests OK each**. `python3 scripts/test_audit_gate.py`: **166 tests, OK (1 skipped)**. ## Structure and recurrence checks * `docs/index.md`: 2,330 lines (`wc -l`) and 1,578 table rows, both unchanged (corrected from an earlier draft's off-by-one `2,331`, the artifact of a `split('\n')` count). **No line changed its `|` count**, so no cell boundary moved (compared per line against `git show HEAD:docs/index.md`). * Backtick parity: all 11 edited lines have an even backtick count; the file's three pre-existing odd lines (1200, 1201, 1809) are untouched and still the only three. * Japanese characters: 0 (scan for codepoints U+3040-U+30FF and U+4E00-U+9FFF over the whole file). * #4714-type wrap defect: **no `.lean` token is split by a line wrap**. The 2,628 occurrences count the same per physical line, per space-folded paragraph and per glued-folded paragraph, so folding reveals no token the per-line extractor missed. * #4714-type basename mis-resolution: among the 11 edited lines, the one place where a single basename appeared under two different spellings on the same line (1982, `Legacy.lean`) is gone: the bare token `Legacy.lean` (with the `.lean` extension) occurred 4 times before this edit (lines 1977, 1979, 1982, 1983) and 0 times after (all reworded to the shim name without the extension). (An earlier draft of this note gave a whole-file "such groups" total of 245 -> 244; that aggregate does not reproduce under a basename-with->=2-distinct-qualified-paths count run against the reviewed commit and is dropped here in favor of the reproducible per-token count above.) The remaining pairs on 1982/1983 are two genuinely different `JointAnalyticity.lean` files (`AmbientLattice/SpecialCases/` and `Concrete/LatticeGraphCorrelation/`). * No archive tag is used as a resolution channel: the auditor charges every token regardless, and the tag on line 866 is prose, verified by tree hash. ## Follow-up (not fixed in this PR) The row-2019 evidence path `Lemma_17_5_2/HLSBridgeFromSimonLieb.lean` (untouched by this PR) is a 0-declaration umbrella, not the module that carries the 27 declarations the Done row claims -- tracked as a follow-up issue rather than edited here, since this PR's scope is the `MISSING` class and this file is not one of the 11 edited lines. Part of #4704 Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com>

phasetr and others added 2 commits June 23, 2026 00:59

chore(gj-17.1): scaffold §18-supersedes-transfer-matrix-gap statement…

2d847a7

… (issue #4214 B-ii) -- #4214

phasetr merged commit 6872e65 into main Jun 22, 2026
1 check passed

phasetr deleted the feat/gj-17.1-cluster-expansion-supersedes-transfer-gap branch June 22, 2026 16:26

phasetr mentioned this pull request Jun 24, 2026

docs: record axiom status in README + mark §17.1 #3511 spectral rows superseded #4279

Merged

This was referenced Jun 25, 2026

Post-axiom-free refactoring: build speedup + simplification/abstraction (investigation → execution) #4298

Closed

refactor(gj-17.1): remove obstructed transfer-matrix spectral-gap scaffolding (~6.6k lines) — #4298 PR-B1 #4303

Merged

phasetr mentioned this pull request Jun 26, 2026

GJ §17.5 Lemma 17.5.2: discharge the per-pair correlation lower bound (only remaining in-scope gap) #4313

Closed

3 tasks

This was referenced Jul 25, 2026

docs: repoint the dangling spectral-gap scaffolding citation at docs/index.md:1715 #4710

Merged

process: gate PR body against the actual diff before merge (nine false-claim incidents across the session, two failure subclasses) #4709

Closed

phasetr mentioned this pull request Jul 25, 2026

docs: repoint the dangling scaffolding references in the ClusterExpansionSupersession module docstring #4711

Merged

phasetr mentioned this pull request Jul 26, 2026

docs: repoint and rewrite the 12 MISSING docs/index.md citations (#4704 PR-4) #4743

Merged

Navigation Menu

feat(gj-17.1): §18 cluster expansion supersedes the transfer-matrix infinite-volume gap — #4214 (B-ii) - #4228

feat(gj-17.1): §18 cluster expansion supersedes the transfer-matrix infinite-volume gap — #4214 (B-ii)#4228
phasetr merged 2 commits into
mainfrom
feat/gj-17.1-cluster-expansion-supersedes-transfer-gap

phasetr commented Jun 22, 2026

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

1 participant

Conversation

phasetr commented Jun 22, 2026

Summary

Verification

Docs

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

1 participant