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

IsingModel/Concrete/LatticeGraphCorrelation/MayerAnalyticity.lean

@@ -69,12 +69,12 @@ live in `MayerAnalyticityExpansionTerm.lean`. -/
 
 /-! ## Moved: Mayer tanh-composed analyticity wrappers
 
-The eight `*_tanh_analytic*` wrappers at the tanh substitution live in
-`MayerAnalyticityTanhAlongEx.lean`
-(`mayerPartialSumAlongExhaustion_*`, four wrappers) and
-`MayerAnalyticityTanhExpansionTerm.lean`
-(`mayerExpansionTerm_Λ_*` / `mayerExpansionTermAlongExhaustion_*`,
-four wrappers). -/
+The four remaining `*_tanh_analytic*` wrappers at the tanh substitution
+live in `MayerAnalyticityTanhAlongEx.lean`
+(`mayerPartialSumAlongExhaustion_*`, four wrappers). The four ℤ^d
+`mayerExpansionTerm` tanh `AnalyticAt` counterparts at the Λ and
+along-exhaustion layers were deleted; no consumer of them was found in
+this repository. -/
 
 
 end Ambient

IsingModel/Concrete/LatticeGraphCorrelation/MayerEdgeCases.lean

@@ -24,18 +24,19 @@ The four wrappers
 `MayerEdgeCasesLambda.lean`. -/
 
 
-/-! ## Moved: along-ex Mayer identity edge-case wrappers
+/-! ## Deleted: along-ex Mayer identity edge-case wrappers
 
-The four wrappers
-`mayer_identity_at_{zero,betaJ_zero,beta_zero,J_zero}_AlongExhaustion_latticeGraph`
-now live in `MayerEdgeCasesAlongExIdentity.lean`. -/
+The four ℤ^d along-exhaustion `mayer_identity_at_*` wrappers at the
+trivial parameter slices were deleted; no consumer of them was found in
+this repository. -/
 
 
-/-! ## Moved: Λ polymerFreeEnergy = mayerPartialSum edge cases
+/-! ## Deleted: Λ polymerFreeEnergy = mayerPartialSum edge cases
 
-The four wrappers
-`polymerFreeEnergy_Λ_latticeGraph_eq_mayerPartialSum_at_{zero,betaJ_zero,beta_zero,J_zero}`
-now live in `MayerEdgeCasesLambdaPolymer.lean`. -/
+The four ℤ^d Λ-layer
+`polymerFreeEnergy_Λ_latticeGraph_eq_mayerPartialSum_at_*` wrappers at
+the trivial parameter slices were deleted; no consumer of them was found
+in this repository. -/
 
 /-! ## Moved: along-ex polymerFreeEnergy = mayerPartialSum edge cases
 

IsingModel/Concrete/LatticeGraphCorrelation/MayerVdBounds.lean

@@ -68,12 +68,13 @@ wrappers (`ge_one_of_nonneg`, `le_one_plus_pow_of_nonneg`,
 
 
 
-/-! ## Moved: AlongEx vdPolymerFamilies_sum `_of_nonneg` family
+/-! ## Deleted: AlongEx vdPolymerFamilies_sum generic-`t` bound family
 
-The four
-`vdPolymerFamilies_sumAlongExhaustion_latticeGraph_*_of_nonneg`
-wrappers (`{ge_one, le_one_plus_pow, pos, eq_one_add}`) now live
-in `MayerVdBoundsAlongExNonneg.lean`. -/
+The four ℤ^d along-exhaustion generic-`t` bound wrappers of the
+`vdPolymerFamilies_sumAlongExhaustion_latticeGraph_*` family (the lower
+bound, the `(1 + t)^|E|` upper bound, positivity under `0 ≤ t`, and the
+`1 + ε(t)` decomposition) were deleted; no consumer of them was found in
+this repository. -/
 
 
 end Ambient