refactor: delete 10 zero-consumer Mayer/vd-polymer wrapper modules (safe-to-delete batch 3)

[phasetr]

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 [refactor] tier2 2026-07-27 technical-debt lane: safe-to-delete module deletion (A), Lemma_17_5_2 providers (B), lakefile warningAsError (C, done), tex lexicon PR-A (D), scanner fail-open (F) #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 ([refactor] tier2 2026-07-27 technical-debt lane: safe-to-delete module deletion (A), Lemma_17_5_2 providers (B), lakefile warningAsError (C, done), tex lexicon PR-A (D), scanner fail-open (F) #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 [refactor] tier2 2026-07-27 technical-debt lane: safe-to-delete module deletion (A), Lemma_17_5_2 providers (B), lakefile warningAsError (C, done), tex lexicon PR-A (D), scanner fail-open (F) #4746 so a later batch does not cascade into
  book content.

🤖 Generated with Claude Code