phasetr · phasetr · Aug 11, 2026 · Aug 11, 2026 · Aug 11, 2026 · Aug 11, 2026
diff --git a/IsingModel/AmbientLattice/AnalyticityLambdaBasicIdentities.lean b/IsingModel/AmbientLattice/AnalyticityLambdaBasicIdentities.lean
@@ -11,7 +11,9 @@ on the induced subgraph `inducedGraph G Λ`. Write `E` for `(inducedGraph G Λ).
 statement that mentions one carries the summation written out; the `mayerPartialSum` and
 `mayerExpansionTerm` statements mention neither, and `ε` occurs only in the decomposition
 `Ξ t = 1 + ε t`. Of the two, only `Ξ` is abbreviated in the theorem names, as
-`vdPolymerFamilies_sum_Λ`.
+`vdPolymerFamilies_sum_Λ`. The declaration comments below write `vdSum` for `Ξ`, `vdSum_tanh`
+for `Ξ (tanh (β * J))` and `ε(t)` for `ε t`; all three are prose shorthands of this file and
+none is a name in the library.
 
 Special values are recorded at literal arguments substituted into the statement: `Ξ 0 = 1`,
 `Ξ 1 = (vdCompatiblePolymerFamilies (inducedGraph G Λ)).card`,

diff --git a/IsingModel/AmbientLattice/AnalyticityLambdaCapstones.lean b/IsingModel/AmbientLattice/AnalyticityLambdaCapstones.lean
@@ -18,7 +18,9 @@ connectedness-filter identities are phrased through `Fintype.piFinset`, `allPoly
 `polymerSeqIncompatibilityGraph`, `mayerExpansionTerm` occurring in their names and in no
 statement of this file. Writing `E` for
 `(inducedGraph G Λ).edgeFinset`, `polymerFreeEnergy (inducedGraph G Λ) t` is by definition
-`Real.log` of that sum at activity `t`.
+`Real.log` of that sum at activity `t`. The declaration comment on the power identity writes
+`ε(t)` for the polymer sum with its empty family removed; that is a prose shorthand of this
+file and not a name in the library.
 
 The high-temperature expansion gives `partitionFunctionΛ G Λ ⟨J, 0, β⟩` in closed form as
 `2 ^ Fintype.card ↑Λ * Real.cosh (β * J) ^ E.card` times the polymer sum at activity
@@ -67,7 +69,7 @@ theorem partitionFunctionΛ_high_temp_expansion_h_zero_polymer_family
   exact IsingModel.partitionFunction_high_temp_expansion_h_zero_polymer_family
     (inducedGraph G Λ) J β
 
-/-- **Λ-layer: §18.4 partitionFunction even-subgraph form** (FV (3.45))**:
+/-- **Λ-layer: §18.4 partitionFunction even-subgraph form** (FV (3.45)):
 `Z_Λ = 2^|Λ| · cosh(β·J)^|E_Λ| · ∑_X tanh(β·J)^|X|`. -/
 theorem
 partitionFunctionΛ_high_temp_expansion_h_zero_closed_evenSubgraphs

diff --git a/IsingModel/AmbientLattice/AnalyticityLambdaEpsilonIff.lean b/IsingModel/AmbientLattice/AnalyticityLambdaEpsilonIff.lean
@@ -12,7 +12,11 @@ the same sum over `… .erase ∅`, so that `Ξ t = 1 + ε t` and
 its own, so a statement that mentions one carries the summation written out — never both in
 the same statement here — while the statements phrased through `polymerFreeEnergy` mention
 neither. The theorem names abbreviate `Ξ` to `vdPolymerFamilies_sum_Λ` and `ε` to
-`vdPolymerFamilies_sum_Λ_minus_one`.
+`vdPolymerFamilies_sum_Λ_minus_one`. The comments below, declaration and section alike, write
+`vdSum` for `Ξ` and `pFE` for `polymerFreeEnergy (inducedGraph G Λ)`, and parenthesise the
+activity: `vdSum(t)`, `ε(t)` and `pFE(tanh)` are `Ξ t`, `ε t` and the polymer free energy at
+`Real.tanh (β * J)`. All three are prose shorthands of this file, and only the last
+abbreviates something that is a `def`.
 
 The characterisations are exact and their two cases are complementary. Under `0 ≤ t`:
 `0 < ε t` precisely when `0 < t` and `(allPolymers (inducedGraph G Λ)).Nonempty`, and

diff --git a/IsingModel/AmbientLattice/AnalyticityLambdaMayerPfeEdgeBounds.lean b/IsingModel/AmbientLattice/AnalyticityLambdaMayerPfeEdgeBounds.lean
@@ -8,7 +8,9 @@ Statements for an ambient graph `G : SimpleGraph V` and a finite volume `Λ : Fi
 on the induced subgraph `inducedGraph G Λ`. Write `E` for `(inducedGraph G Λ).edgeFinset`,
 `Ξ t` for `∑ Γ ∈ vdCompatiblePolymerFamilies (inducedGraph G Λ), ∏ P ∈ Γ, t ^ P.card` and
 `ε t` for the same sum over `… .erase ∅`; neither has a definition of its own, and
-`polymerFreeEnergy (inducedGraph G Λ) t = Real.log (Ξ t)` by definition.
+`polymerFreeEnergy (inducedGraph G Λ) t = Real.log (Ξ t)` by definition. The declaration
+comment on the decomposition below writes `ε(t)` for `ε t`; that is a prose shorthand of this
+file and not a name in the library.
 
 At order `2` the Mayer expansion term is written out over
 `allPolymers (inducedGraph G Λ) ×ˢ allPolymers (inducedGraph G Λ)`, once with the weight

diff --git a/IsingModel/AmbientLattice/AnalyticityLambdaMayerRecurrenceEpsilon.lean b/IsingModel/AmbientLattice/AnalyticityLambdaMayerRecurrenceEpsilon.lean
@@ -10,7 +10,9 @@ on the induced subgraph `inducedGraph G Λ`. Write `ε t` for the excess polymer
 polymer sum with its empty-family term removed; it has no definition of its own, so a
 statement that mentions it carries the summation written out, while the recurrence, the
 low-order sign statements and the edgeless-graph statement mention it nowhere and are
-phrased through `mayerPartialSum`, `mayerExpansionTerm` and `allPolymers`. By definition
+phrased through `mayerPartialSum`, `mayerExpansionTerm` and `allPolymers`. The comments below,
+declaration and section alike, parenthesise the activity, writing `ε(t)` and `ε(0)` for `ε t`
+and `ε 0`; that is a prose shorthand of this file and not a name in the library. By definition
 `polymerFreeEnergy (inducedGraph G Λ) t` is `Real.log` of the full polymer sum
 `∑ Γ ∈ vdCompatiblePolymerFamilies (inducedGraph G Λ), ∏ P ∈ Γ, t ^ P.card`; that this also
 equals `Real.log (1 + ε t)` is the content of the decomposition of that sum as `1 + ε t`, a

diff --git a/IsingModel/AmbientLattice/AnalyticityLambdaPfeSharpening.lean b/IsingModel/AmbientLattice/AnalyticityLambdaPfeSharpening.lean
@@ -8,7 +8,12 @@ Statements for an ambient graph `G : SimpleGraph V` and a finite volume `Λ : Fi
 on the induced subgraph `inducedGraph G Λ`. Write `E` for `(inducedGraph G Λ).edgeFinset`,
 `Ξ t` for `∑ Γ ∈ vdCompatiblePolymerFamilies (inducedGraph G Λ), ∏ P ∈ Γ, t ^ P.card` and
 `ε t` for the same sum over `… .erase ∅`; neither sum has a definition of its own, and
-`polymerFreeEnergy (inducedGraph G Λ) t = Real.log (Ξ t)` by definition.
+`polymerFreeEnergy (inducedGraph G Λ) t = Real.log (Ξ t)` by definition. The comments below,
+declaration and section alike, write `vdSum` for `Ξ` and `pFE` for
+`polymerFreeEnergy (inducedGraph G Λ)`, and parenthesise the activity: `vdSum(t)`, `ε(t)`
+and `pFE(tanh)` are `Ξ t`, `ε t` and the polymer free energy at `Real.tanh (β * J)`. All
+three are prose shorthands of this file, and only the last abbreviates something that is a
+`def`.
 
 Three parameter regimes occur and each statement belongs to exactly one, so the conditions
 below do not carry across the paragraph breaks.

diff --git a/IsingModel/AmbientLattice/AnalyticityLambdaPolymer.lean b/IsingModel/AmbientLattice/AnalyticityLambdaPolymer.lean
@@ -14,7 +14,9 @@ here mention neither and are phrased through `polymerFreeEnergy`, `mayerPartialS
 ∏ P ∈ Γ, t ^ P.card`, which the theorem names abbreviate to `vdPolymerFamilies_sum_Λ`, and
 `ε t` for the same sum over `(vdCompatiblePolymerFamilies (inducedGraph G Λ)).erase ∅`, which
 they abbreviate to `eps`. Then `polymerFreeEnergy (inducedGraph G Λ) t = Real.log (Ξ t)` by
-definition, and `E` below is `(inducedGraph G Λ).edgeFinset`.
+definition, and `E` below is `(inducedGraph G Λ).edgeFinset`. The declaration comments below
+write `vdSum` for `Ξ` and `ε(t)` for `ε t`; both are prose shorthands of this file and
+neither is a name in the library.
 
 Growth in the activity is strict once a polymer exists: assuming
 `(allPolymers (inducedGraph G Λ)).Nonempty`, the polymer free energy at `t` exceeds the one

diff --git a/IsingModel/AmbientLattice/AnalyticityLambdaTanhFerroIff.lean b/IsingModel/AmbientLattice/AnalyticityLambdaTanhFerroIff.lean
@@ -9,7 +9,12 @@ on the induced subgraph `inducedGraph G Λ`, all at the physical activity
 `Real.tanh (β * J)`. Write `E` for `(inducedGraph G Λ).edgeFinset`, `Ξ t` for
 `∑ Γ ∈ vdCompatiblePolymerFamilies (inducedGraph G Λ), ∏ P ∈ Γ, t ^ P.card` and `ε t` for
 the same sum over `… .erase ∅`; neither sum has a definition of its own, and
-`polymerFreeEnergy (inducedGraph G Λ) t = Real.log (Ξ t)` by definition.
+`polymerFreeEnergy (inducedGraph G Λ) t = Real.log (Ξ t)` by definition. The comments below,
+declaration and section alike, write `vdSum` for `Ξ` and `pFE` for
+`polymerFreeEnergy (inducedGraph G Λ)`, and parenthesise the activity: `vdSum(tanh)`,
+`ε(tanh)` and `pFE(tanh)` are `Ξ`, `ε` and the polymer free energy at `Real.tanh (β * J)`.
+All three are prose shorthands of this file, and only the last abbreviates something that is
+a `def`.
 
 The regime here is the ferromagnetic pair: `0 ≤ β` together with `0 ≤ J`, stated as two
 separate hypotheses rather than as the single product condition `0 ≤ β * J`, which the pair

diff --git a/IsingModel/AmbientLattice/Defs/HighTempPartition/ExpBounds.lean b/IsingModel/AmbientLattice/Defs/HighTempPartition/ExpBounds.lean
@@ -146,7 +146,8 @@ theorem freeEnergyΛ_high_temp_expansion_h_zero_closed
 
 /-- **Λ-level Z high-temperature upper bound (GJ §18.3 / FV (3.45))**:
 under `0 ≤ β·J`,
-`Z_Λ(⟨J, 0, β⟩) ≤ 2^(|Λ|+|E_Λ|) · (cosh(βJ))^|E_Λ|`. ℤ^d wrapper of Step 320. -/
+`Z_Λ(⟨J, 0, β⟩) ≤ 2^(|Λ|+|E_Λ|) · (cosh(βJ))^|E_Λ|`. Λ-layer wrapper of
+`partitionFunction_high_temp_expansion_h_zero_upper_bound` (Step 320). -/
 theorem partitionFunctionΛ_high_temp_expansion_h_zero_upper_bound
     (G : SimpleGraph V) (Λ : Finset V)
     [Fintype (inducedGraph G Λ).edgeSet]

diff --git a/IsingModel/AmbientLattice/MagnetizationInfiniteHZeroJZero.lean b/IsingModel/AmbientLattice/MagnetizationInfiniteHZeroJZero.lean
@@ -83,7 +83,8 @@ whenever the test set `A` is contained in `Λ.volume n`,
 Specialization of `IsingModel.correlation_J_zero`
 (`⟨σ^A⟩ = tanh(β·h)^{|A|}`) along the induced-subgraph coercion.
 Reference: Glimm–Jaffe *Quantum Physics* 2nd ed., §4.1
-(infinite-temperature slice of the correlation function). -/
+(non-interacting `J = 0` slice of the correlation function; `β` is
+free here, so this is not the infinite-temperature limit `β → 0`). -/
 theorem correlationAlongExhaustion_J_zero_of_subset
     (G : SimpleGraph V) (Λ : Exhaustion V)
     [∀ n, Fintype (inducedGraph G (Λ.volume n)).edgeSet]
@@ -123,7 +124,9 @@ constant at `tanh(β·h)^A.card`, so it tends to that value; by
 `correlationInfinite`, so the two limits coincide.
 
 Reference: Glimm–Jaffe *Quantum Physics* 2nd ed., §4.1 / §5.1
-infinite-temperature slice. -/
+non-interacting `J = 0` slice (`β` is constrained only by
+`Ferromagnetic.hβ : 0 < β`, not by the infinite-temperature limit
+`β → 0`). -/
 theorem correlationInfinite_J_zero
     (G : SimpleGraph V) (Λ : Exhaustion V)
     [∀ n, Fintype (inducedGraph G (Λ.volume n)).edgeSet]

diff --git a/IsingModel/AmbientLattice/MagnetizationInfiniteLambdaHSymmetry.lean b/IsingModel/AmbientLattice/MagnetizationInfiniteLambdaHSymmetry.lean
@@ -195,8 +195,8 @@ theorem correlationΛ_ge_tanh_pow_card
     (Set.mem_Ici.mpr le_rfl) (Set.mem_Ici.mpr hJ) hJ
 
 /-- **Λ-level lower bound `magnetizationΛ ≥ tanh(β·h)`** (ferromagnetic):
-specialization of `correlationΛ_ge_tanh_pow_card` at `A = {i}` where
-`|A|^1 = |A|.card = 1`. -/
+specialization of `correlationΛ_ge_tanh_pow_card` at `A = {i}`
+(`A.card = 1`, so the power reduces to `tanh(β·h)`). -/
 theorem magnetizationΛ_ge_tanh
     (G : SimpleGraph V) (Λ : Finset V)
     [Fintype (inducedGraph G Λ).edgeSet]

diff --git a/IsingModel/AmbientLattice/MagnetizationInfiniteSusceptibility.lean b/IsingModel/AmbientLattice/MagnetizationInfiniteSusceptibility.lean
@@ -45,8 +45,21 @@ variable {V : Type*} [DecidableEq V]
 Analog of `magnetizationInfinite` / `correlationInfinite`, but for the
 susceptibility χ. Unlike `correlation` (bounded by 1) or
 `magnetization` (bounded by 1), susceptibility is *not automatically
-bounded* as the exhaustion grows: `|χ_Λ(i)| ≤ 2·|Λ|`, which diverges
-with `|Λ|`. Hence the `⨆` on `ℝ` may return the `ciSup` default `0`
+bounded* as the exhaustion grows: `susceptibilityΛ` unfolds to
+`∑ j, truncated2 …`, so the number of summands is nondecreasing in the
+stage volume, and no statement here bounds the family uniformly in the
+stage. Stage-uniform bounds do exist elsewhere in the tree, under
+hypotheses: at high temperature,
+`susceptibilityAlongExhaustion_le_of_high_temp` and
+`susceptibilityAlongExhaustion_bddAbove_latticeGraph_of_high_temp`
+(`Inequalities/HighTemp/Susceptibility.lean`), both stated at zero
+field. The latter gives `BddAbove` for the lattice-graph sequence at
+`⟨J, 0, β⟩`, which is the hypothesis of `susceptibilityInfinite_le_abs_h`
+below only when `h = 0`, where that comparison is an identity; at
+`h ≠ 0` that hypothesis sits at `⟨J, |h|, β⟩` and is not supplied by it.
+Further size facts hold on special slices, such as the
+closed form `susceptibilityInfinite_J_zero` at `J = 0`.
+Hence the `⨆` on `ℝ` may return the `ciSup` default `0`
 when the along-exhaustion sequence is unbounded (physically: near or at
 the critical point, where χ diverges in the genuine thermodynamic
 limit). Theorems that compare `susceptibilityInfinite` values
@@ -97,7 +110,7 @@ along-exhaustion sequence.
 Stage-wise pointwise inequality `χ_along(h) ≤ χ_along(|h|)` at every
 `n` (A-4c, PR #780) transfers to the `⨆` once the `|h|`-side is
 known to be bounded above. Under the `BddAbove` hypothesis, the
-pointwise comparison plus `ciSup_le_ciSup` gives the result.
+pointwise comparison plus `ciSup_mono` gives the result.
 
 **Necessity of `BddAbove`**: the susceptibility is unbounded at the
 ferromagnetic critical point, where `⨆ χ_along(|h|)` would default to

diff --git a/IsingModel/AmbientLattice/SpecialCases/HighTemperatureBoundsRatioLogFeNonemptyZ.lean b/IsingModel/AmbientLattice/SpecialCases/HighTemperatureBoundsRatioLogFeNonemptyZ.lean
@@ -23,7 +23,10 @@ namespace Ambient
 
 variable {V : Type*} [DecidableEq V]
 
-/-- **Along-ex Z strict deviation under nonempty volume**. -/
+/-- **Along-ex Z strict deviation under a nonempty edge set**: the hypotheses are
+`0 < β * J` and `0 < |E|`. Unlike its `_of_nonempty` siblings in
+`HighTemperatureBoundsRatioLogFeNonempty`, this statement takes no nonemptiness
+hypothesis on the stage volume. -/
 theorem partitionFunctionAlongExhaustion_high_temp_expansion_h_zero_pow_two_lt_of_nonempty
     (G : SimpleGraph V) (Λ : Exhaustion V)
     [∀ n, Fintype (inducedGraph G (Λ.volume n)).edgeSet]

diff --git a/IsingModel/AmbientLattice/SpecialCases/HighTemperatureVdSandwichFE.lean b/IsingModel/AmbientLattice/SpecialCases/HighTemperatureVdSandwichFE.lean
@@ -6,7 +6,7 @@ import IsingModel.AmbientLattice.SpecialCases.HighTemperatureVdSandwichFEFerro
 /-!
 # §18.5 cluster-expansion convergence sandwich wrappers along an exhaustion
 
-Provides the GJ §18.5 two-sided bound on the van-den-Berg polymer-family sum along an
+Provides the GJ §18.5 two-sided bound on the vertex-disjoint polymer-family sum along an
 exhaustion, in plain and sharpened form — the convergence input for the stagewise
 cluster-expansion estimates. Each passes through to its
 `vdPolymerFamilies_sum_Λ_sandwich*` ambient counterpart.

diff --git a/IsingModel/AmbientLattice/SpecialCases/MayerVdRegularityVdPolymer.lean b/IsingModel/AmbientLattice/SpecialCases/MayerVdRegularityVdPolymer.lean
@@ -6,9 +6,9 @@ import IsingModel.AmbientLattice.SpecialCases.MayerVdRegularityVdPolymerHasDeriv
 /-!
 # `vdPolymerFamilies_sum` regularity wrappers along an exhaustion
 
-Records continuity and differentiability of the along-exhaustion van-den-Berg polymer-family
-sum (GJ §18.5), which is what lets the cluster expansion be differentiated in the model
-parameters stage by stage.
+Records continuity and differentiability of the along-exhaustion vertex-disjoint
+polymer-family sum (GJ §18.5), which is what lets the cluster expansion be differentiated in
+the model parameters stage by stage.
 -/
 
 namespace IsingModel

diff --git a/IsingModel/AmbientLattice/SpecialCases/MayerVdRegularityVdPolymerTanh.lean b/IsingModel/AmbientLattice/SpecialCases/MayerVdRegularityVdPolymerTanh.lean
@@ -5,7 +5,7 @@ import IsingModel.AmbientLattice.SpecialCases.MayerVdRegularityVdPolymerTanhDiff
 /-!
 # `vdPolymerFamilies_sum` tanh `Continuous` wrappers along an exhaustion
 
-Records continuity of the along-exhaustion van-den-Berg polymer-family sum in the
+Records continuity of the along-exhaustion vertex-disjoint polymer-family sum in the
 `tanh`-composed parameters `β` and `J` (GJ §18.5), one wrapper varying `β` at fixed `J` and
 the other varying `J` at fixed `β`. Each is a pass-through of the corresponding
 `vdPolymerFamilies_sum_Λ_tanh_continuous_*` ambient lemma. The matching

diff --git a/IsingModel/AmbientLattice/SpecialCases/VdPolymerFamiliesAnalyticityLog.lean b/IsingModel/AmbientLattice/SpecialCases/VdPolymerFamiliesAnalyticityLog.lean
@@ -5,7 +5,7 @@ import IsingModel.AmbientLattice.SpecialCases.VdPolymerFamiliesAnalyticityLogTan
 /-!
 # Ambient log_vdPolymerFamilies_sumAlongExhaustion analyticity wrappers
 
-Carries analyticity of the logarithm of the van-den-Berg polymer-family sum to the
+Carries analyticity of the logarithm of the vertex-disjoint polymer-family sum to the
 along-exhaustion layer (GJ §18.5), where it feeds the analyticity of the infinite-volume
 free energy. Each result passes through the corresponding Λ-level
 `log_vdPolymerFamilies_sum_Λ_*` lemma.

diff --git a/IsingModel/AmbientLattice/TruncatedFunctions/FourPoint.lean b/IsingModel/AmbientLattice/TruncatedFunctions/FourPoint.lean
@@ -369,8 +369,10 @@ in `Inequalities/GHS.lean`). Uses the ∞-vol closed form
 six Finsets of card 2.
 
 Complements `truncated4Infinite_beta_zero` (vanishing slice at
-`β = 0`): this is the J=0 slice with explicit closed form `-2·t⁴`
-(non-vanishing). Note `-2·t⁴ ≤ 0` always, consistent with
+`β = 0`): this is the J=0 slice with explicit closed form `-2·t⁴`,
+which over the `Ferromagnetic` range `0 ≤ h`, `0 < β` is `0` exactly
+when the external field vanishes and is strictly negative otherwise.
+Note `-2·t⁴ ≤ 0` always, consistent with
 `truncated4Infinite_nonpos_h_zero`.
 
 Reference: Glimm–Jaffe *Quantum Physics* 2nd ed., §5.1 pp. 72–74

diff --git a/IsingModel/AmbientLatticeSum/InfiniteBounds.lean b/IsingModel/AmbientLatticeSum/InfiniteBounds.lean
@@ -85,8 +85,13 @@ Combines the per-stage uniform bound
 condition is discharged via the ferromagnetic lower bound
 `freeEnergyAlongExhaustion_ge_log_two_cosh` at `h = 0`.
 
-Globally tighter than `freeEnergyInfinite_le_uniform_upper_bound` at
-`h = 0` (the cosh-based bound). -/
+Numerically the same bound as `freeEnergyInfinite_le_uniform_upper_bound`
+at `h = 0`: that lemma's `log 2 + |β|·(|J|·c + |h|)` collapses to
+`log 2 + β·J·c` under `0 ≤ J`, `0 < β`, `h = 0`. What this statement adds
+is the specialized form, not a sharper constant. (`Real.cosh` occurs in
+neither conclusion; it enters only through the lower bound
+`freeEnergyAlongExhaustion_ge_log_two_cosh` used to discharge
+coboundedness in both proofs.) -/
 theorem freeEnergyInfinite_high_temp_h_zero_upper_bound_exp_uniform
     [Nonempty V] (G : SimpleGraph V) (Λ : Exhaustion V)
     [∀ n, Fintype (inducedGraph G (Λ.volume n)).edgeSet]

diff --git a/IsingModel/AmbientLatticeSum/InfiniteHighTemp.lean b/IsingModel/AmbientLatticeSum/InfiniteHighTemp.lean
@@ -283,9 +283,11 @@ theorem freeEnergyInfinite_high_temp_h_zero_deviation_sandwich_exp
     G Λ J β hJ hβ hc
   exact ⟨by linarith, h_upper⟩
 
-/-- **∞-vol f ratio upper bound at J=0 trivial slice (GJ §18.3)**:
-under ferromagnetic + bounded-edge-density witness `c`,
+/-- **∞-vol f difference upper bound against the J=0 trivial slice
+(GJ §18.3)**: under ferromagnetic + bounded-edge-density witness `c`,
 `freeEnergyInfinite ⟨J, 0, β⟩ - freeEnergyInfinite ⟨0, 0, β⟩ ≤ β·J·c`.
+The bounded quantity is the difference displayed above, not a ratio;
+the `_ratio_bound` in the name does not describe the statement.
 
 Reformulation of Step 418 deviation bound using the trivial slice
 identity `f_∞⟨0, 0, β⟩ = log 2`. -/
@@ -303,7 +305,9 @@ theorem freeEnergyInfinite_high_temp_h_zero_ratio_bound
   exact freeEnergyInfinite_high_temp_h_zero_deviation_bound_exp
     G Λ J β hJ hβ hc
 
-/-- **∞-vol f ratio upper bound at β=0 trivial slice**. -/
+/-- **∞-vol f difference upper bound against the β=0 trivial slice**:
+`freeEnergyInfinite ⟨J, 0, β⟩ - freeEnergyInfinite ⟨J, 0, 0⟩ ≤ β·J·c`.
+As above, the bounded quantity is a difference, not a ratio. -/
 theorem freeEnergyInfinite_high_temp_h_zero_ratio_bound_beta_zero
     [Nonempty V] (G : SimpleGraph V) (Λ : Exhaustion V)
     [∀ n, Fintype (inducedGraph G (Λ.volume n)).edgeSet]

diff --git a/IsingModel/Concrete/LatticeGraphCorrelation/ComplexSlitPlane.lean b/IsingModel/Concrete/LatticeGraphCorrelation/ComplexSlitPlane.lean
@@ -26,7 +26,10 @@ theorem partitionFunctionComplex_continuousAt_real_h_latticeGraph
   IsingModel.partitionFunctionComplex_continuousAt_real_h
     (Ambient.inducedGraph (IsingModel.latticeGraph d) Λ) J β h₀
 
-/-- **ℤ^d `f_ℂ` `ContinuousAt` real positive `h₀`** (Λ-induced). -/
+/-- **ℤ^d `f_ℂ` `ContinuousAt` real `h₀`** (Λ-induced): continuity holds at
+every real `h₀`. The `_pos_h_` in the name, inherited from the ambient
+`freeEnergyComplex_continuousAt_real_pos_h`, promises a positivity hypothesis
+that neither statement carries. -/
 theorem freeEnergyComplex_continuousAt_real_pos_h_latticeGraph
     (d : ℕ) (Λ : Finset (Fin d → ℤ)) (J β : ℝ) (h₀ : ℝ) :
     ContinuousAt (fun h : ℂ => IsingModel.freeEnergyComplex

diff --git a/IsingModel/Concrete/LatticeGraphCorrelation/LatticeMassHighTempZeroBoundary.lean b/IsingModel/Concrete/LatticeGraphCorrelation/LatticeMassHighTempZeroBoundary.lean
@@ -112,7 +112,7 @@ private lemma inducedLatticeGraph_correlation_le_const_mul_beta
   exact ge_of_tendsto h_g_tendsto h_eventual
 
 /-- **Linear bound on corr_∞ at β = 0** (Step 176, GJ §17.5):
-For `0 ≤ J`, `1 ≤ d`, `0 < b` with `bJ·2d < 1`, and any `r ≠ s`, on the interval `(0, b]`:
+For `0 ≤ J`, `0 < b` with `bJ·2d < 1`, and any `r ≠ s`, on the interval `(0, b]`:
 `corr_∞(r, s, β) ≤ (J·M(b)² + J·4d) · β`,
 where `M(b) = bJ·2d/(1 - bJ·2d)`.