refactor: delete 9 zero-consumer partition/free-energy, magnetization/Mayer and J = 0 pseudo-mass wrapper modules (safe-to-delete batch 4)

[phasetr]

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