diff --git a/IsingModel/AmbientLattice/AnalyticityLambdaBasicIdentities.lean b/IsingModel/AmbientLattice/AnalyticityLambdaBasicIdentities.lean index aa3a3302f..c323d768e 100644 --- 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 index 74f8f568d..258525071 100644 --- 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 index da7d38334..9f009ca63 100644 --- 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 index 140fac134..1060881de 100644 --- 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 index 66839ccc0..be1c99804 100644 --- 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 index 9a105d7e6..aedae89b9 100644 --- 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 index 873750aad..2725a595b 100644 --- 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 index 552bc1aa1..7b22d5e04 100644 --- 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 index fbb8110e5..8657b42ee 100644 --- 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 index 1417f517e..e1d5b6691 100644 --- 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 index 6664aa98f..ae0f8a6c1 100644 --- 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 index ccd34ede6..5c01b0dd5 100644 --- 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 index e916fa20d..706f52d4a 100644 --- 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 index 31e134f34..75a5a2aee 100644 --- 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 index 3e1a52267..0a6380ebb 100644 --- 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 index ce486387a..5bfcf22b7 100644 --- 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 index d82f02faf..6a3db9af3 100644 --- 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 index dd2539297..a38387c0c 100644 --- 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 index 785d91ddb..db9003a67 100644 --- 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 index e6ef8c1ca..3a452f244 100644 --- 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 index d16885f72..97419db92 100644 --- 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 index ea0de7970..7058faf32 100644 --- 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)`. diff --git a/IsingModel/Concrete/LatticeGraphCorrelation/Lemma_17_5_2/FiniteRegionPseudoMassDistContinuity.lean b/IsingModel/Concrete/LatticeGraphCorrelation/Lemma_17_5_2/FiniteRegionPseudoMassDistContinuity.lean index 69e0989fd..2db7b17da 100644 --- a/IsingModel/Concrete/LatticeGraphCorrelation/Lemma_17_5_2/FiniteRegionPseudoMassDistContinuity.lean +++ b/IsingModel/Concrete/LatticeGraphCorrelation/Lemma_17_5_2/FiniteRegionPseudoMassDistContinuity.lean @@ -62,9 +62,14 @@ infimum over the finitely many distinct pairs of the bounded region `A` of the distance-parametrized per-pair pseudo-mass `pseudoMassFromParamsAtPairDist`. Each contributing pair uses its own ℓ¹ lattice distance as the profile radius, -so this finite infimum is the genuine inverse correlation length restricted to -the region `A`. It is the book's continuous object (a *finite* infimum, hence -continuous), in contrast to the infinite lower envelope `globalPseudoMassDist`. +so the radius is faithful to the pair rather than fixed. No relation between +this infimum and the inverse correlation length `latticeMass` is proved here. +For the global envelope the two directions are asymmetric: the lower bound +`globalPseudoMassDist_le_latticeMass` carries no constant, whereas the reverse +direction needs one and is restricted to the high-temperature window (the upper +half of `globalPseudoMassDist_fullSandwich`). It is the book's continuous +object (a *finite* infimum, hence continuous), in contrast to the infinite lower +envelope `globalPseudoMassDist`. References: Glimm--Jaffe §17.5, Lemma 17.5.2, pp.~311--312. -/ noncomputable def finiteRegionPseudoMassDist {α d : ℕ} (hα : 1 ≤ α) diff --git a/IsingModel/Concrete/LatticeGraphCorrelation/Lemma_17_5_2/MassContinuityPairMassUpperIcc.lean b/IsingModel/Concrete/LatticeGraphCorrelation/Lemma_17_5_2/MassContinuityPairMassUpperIcc.lean index 964eb23cb..9875f9d0d 100644 --- a/IsingModel/Concrete/LatticeGraphCorrelation/Lemma_17_5_2/MassContinuityPairMassUpperIcc.lean +++ b/IsingModel/Concrete/LatticeGraphCorrelation/Lemma_17_5_2/MassContinuityPairMassUpperIcc.lean @@ -10,8 +10,9 @@ The per-pair distance pseudo-mass is bounded **above by a single constant** on a This is the interval-uniform **upper** bound (companion to the lower bound #4360), needed to bound the `m^{2α}` factor in the GJ p.312 uniform Lipschitz constant. Per-β `m⁻(x,z) ≤ −log tanh(βJ)` -(from the faithful correlation lower bound #4333 + `pseudoMass_le_iff_pseudoMassG_le`); the rate -`−log tanh(βJ)` is decreasing in β (tanh increasing), so `≤ −log tanh(β₁J)` on the interval. +(from the direct-path-rate correlation lower bound #4333 + +`pseudoMass_le_iff_pseudoMassG_le`); the rate `−log tanh(βJ)` is decreasing in β (tanh +increasing), so `≤ −log tanh(β₁J)` on the interval. References: @@ -26,8 +27,8 @@ open Real /-- **Interval-uniform per-pair m⁻ upper bound** (GJ p.312): for a distinct pair `x ≠ z` and `β ∈ Icc β₁ β₂` with `0 < β₁` and `Icc β₁ β₂ ⊆ ConvergenceRegion.window d J`, `pseudoMassFromParamsAtPairDist hα (cubicExhaustion d) ⟨J,0,β⟩ x z ≤ −log tanh(β₁·J)` — a single -constant upper bound uniform over the interval. Per-β `m⁻(x,z) ≤ −log tanh(βJ)` (faithful rate -#4333 + `pseudoMass_le_iff_pseudoMassG_le`); the rate is antitone in β. -/ +constant upper bound uniform over the interval. Per-β `m⁻(x,z) ≤ −log tanh(βJ)` (direct-path +rate #4333 + `pseudoMass_le_iff_pseudoMassG_le`); the rate is antitone in β. -/ theorem pseudoMassFromParamsAtPairDist_le_neg_log_tanh_beta1_on_Icc {α d : ℕ} (hα : 1 ≤ α) {J β₁ β₂ : ℝ} (hJ : 0 < J) (hβ₁ : 0 < β₁) (hIcc : Set.Icc β₁ β₂ ⊆ ConvergenceRegion.window d J) diff --git a/IsingModel/Concrete/LatticeGraphCorrelation/Lemma_17_5_2/UnconditionalFiniteRegionLipschitz.lean b/IsingModel/Concrete/LatticeGraphCorrelation/Lemma_17_5_2/UnconditionalFiniteRegionLipschitz.lean index c1208ff69..3bb48e869 100644 --- a/IsingModel/Concrete/LatticeGraphCorrelation/Lemma_17_5_2/UnconditionalFiniteRegionLipschitz.lean +++ b/IsingModel/Concrete/LatticeGraphCorrelation/Lemma_17_5_2/UnconditionalFiniteRegionLipschitz.lean @@ -5,8 +5,8 @@ import IsingModel.Concrete.LatticeGraphCorrelation.Lemma_17_5_2.UnconditionalPro # GJ §17.5 Lemma 17.5.2(a) — UNCONDITIONAL finite-region Lipschitz of `m⁻(σ, A)` This module removes the `hprofile` hypothesis from the conditional finite-region Lipschitz -(`FiniteRegionPseudoMassDistLipschitz.lean`, #4332) by re-parametrizing the chain to the **faithful -inverse-correlation-length rate `−log tanh(βJ)`** and discharging the per-pair profile lower bound +(`FiniteRegionPseudoMassDistLipschitz.lean`, #4332) by re-parametrizing the chain to the +**direct-path rate `−log tanh(βJ)`** and discharging the per-pair profile lower bound with the unconditional bound `pseudoMassG_dist_tanh_rate_le_correlationInfinite_cubic` (#4333). The engine is the rate-agnostic abstracted interval Lipschitz @@ -139,7 +139,7 @@ theorem pseudoMassFromParamsAtPair_pow_succ_lipschitz_on_window_of_ratio_lower `pseudoMassG α ρ q ≤ c` (and active range `c ∈ Ioo 0 2`), the denominator ratio is lower-bounded: `pseudoMassG α ρ q / q^(2α) ≤ c / m^(2α)` (`m = pseudoMassFromParamsAtPair`). This is the rate-generalized form of `lemma_17_5_2_profile_lower_ratio_lower_cubic` (#4330), which fixed -`q = −log(βJ·2d)`; here `q` is arbitrary (used at the faithful rate `q = −log tanh(βJ)`). -/ +`q = −log(βJ·2d)`; here `q` is arbitrary (used at the direct-path rate `q = −log tanh(βJ)`). -/ theorem pseudoMassFromParamsAtPair_ratio_lower_of_pseudoMassG_le_corr {α d : ℕ} (hα : 1 ≤ α) {ρ : ℝ} (hρ : 0 < ρ) {J β q : ℝ} (hq_pos : 0 < q) {x z : Fin d → ℤ} @@ -180,7 +180,7 @@ theorem pseudoMassFromParamsAtPair_ratio_lower_of_pseudoMassG_le_corr /-- **GJ §17.5 UNCONDITIONAL per-pair distance interval Lipschitz of `(m⁻(x,z,·))^{2α+1}` on the window.** For any distinct pair `x ≠ z` and `Icc β₁ β₂ ⊆ ConvergenceRegion.window d J`, `∃ K>0, |m⁻(x,z,β₂)^{2α+1} − m⁻(x,z,β₁)^{2α+1}| ≤ (2α+1)K/dist·(β₂−β₁)` with **no profile -hypothesis** — the faithful profile lower bound is discharged by +hypothesis** — the direct-path-rate profile lower bound is discharged by `pseudoMassG_dist_tanh_rate_le_correlationInfinite_cubic` (#4333) at the rate `−log tanh(βJ)`. The interval-uniform ratio lower bound `Lmin = pseudoMassG α (dist) q₁ / q₁^{2α}` @@ -276,7 +276,7 @@ convergence window, **with no profile hypothesis**, This removes the conditional `hprofile` of #4332: each per-pair distance interval Lipschitz is now unconditional (`pseudoMassFromParamsAtPairDist_pow_succ_lipschitz_on_window`, discharged via the -faithful-rate profile bound #4333); the finite `Finset.inf'` assembly is unchanged (odd-power +direct-path-rate profile bound #4333); the finite `Finset.inf'` assembly is unchanged (odd-power commutes with `inf'`; `inf'` of finitely many Lipschitz functions is Lipschitz via the achieved infimum). The constant is per-`A` (uniform-in-`A` / infinite-envelope continuity remains a separate question, #4320). diff --git a/IsingModel/Concrete/LatticeGraphCorrelation/MayerStrictPositivityAlongEx.lean b/IsingModel/Concrete/LatticeGraphCorrelation/MayerStrictPositivityAlongEx.lean index 7af4e2b9d..46815be5b 100644 --- a/IsingModel/Concrete/LatticeGraphCorrelation/MayerStrictPositivityAlongEx.lean +++ b/IsingModel/Concrete/LatticeGraphCorrelation/MayerStrictPositivityAlongEx.lean @@ -5,12 +5,12 @@ import IsingModel.AmbientLattice.SpecialCases.MayerStrictPositivity # Concrete AlongExhaustion Mayer strict positivity wrappers Instantiates at `IsingModel.latticeGraph d` the along-exhaustion strict bounds for the -van-den-Berg polymer-family sum, the strict half of the GJ §18.5 bounds: strict monotonicity, -as the comparison at `0 ≤ s`, `s < t` and as `StrictMonoOn (Set.Ici 0)`, and then, only under -`0 < t`, the lower bound `1` for the sum and strict positivity of the same sum with the empty -family removed. Those last two need `0 < t`: at `t = 0` each polymer, being a nonempty edge -set, contributes a factor `0`, so only the empty family survives and the two sums are `1` and -`0`. All four assume the stage polymer set is nonempty. +vertex-disjoint polymer-family sum, the strict half of the GJ §18.5 bounds: strict +monotonicity, as the comparison at `0 ≤ s`, `s < t` and as `StrictMonoOn (Set.Ici 0)`, and +then, only under `0 < t`, the lower bound `1` for the sum and strict positivity of the same +sum with the empty family removed. Those last two need `0 < t`: at `t = 0` each polymer, +being a nonempty edge set, contributes a factor `0`, so only the empty family survives and +the two sums are `1` and `0`. All four assume the stage polymer set is nonempty. -/ namespace IsingModel diff --git a/IsingModel/Concrete/LatticeGraphCorrelation/PartitionFreeEnergyBoundsFeAlongExId.lean b/IsingModel/Concrete/LatticeGraphCorrelation/PartitionFreeEnergyBoundsFeAlongExId.lean index 331a1c6e9..7855ee027 100644 --- a/IsingModel/Concrete/LatticeGraphCorrelation/PartitionFreeEnergyBoundsFeAlongExId.lean +++ b/IsingModel/Concrete/LatticeGraphCorrelation/PartitionFreeEnergyBoundsFeAlongExId.lean @@ -46,9 +46,13 @@ theorem freeEnergyAlongExhaustion_latticeGraph_nonneg_of_ferromagnetic freeEnergyAlongExhaustion_nonneg_of_ferromagnetic (IsingModel.latticeGraph d) Λ p hf hne -/-- **ℤ^d `freeEnergyAlongExhaustion` as `log Z / card`** (any-Exhaustion): -alternate form of `freeEnergyAlongExhaustion_eq_inv_card_mul_log` using the -Fintype-card expression. -/ +/-- **ℤ^d `freeEnergyAlongExhaustion` as `log Z / card`** (any-Exhaustion). + +Restates `freeEnergyAlongExhaustion_latticeGraph_eq_inv_card_mul_log` above: +the two conclusions are the same proposition, and the declarations differ only +in the ambient lemma they delegate to. The genuinely different cardinality +spelling is `freeEnergyAlongExhaustion_latticeGraph_eq_inv_Λcard_mul_log`, +which uses `(Λ.volume n).card` in place of `Fintype.card`. -/ theorem freeEnergyAlongExhaustion_latticeGraph_eq_log_div_card (d : ℕ) (Λ : Ambient.Exhaustion (Fin d → ℤ)) (p : IsingParams ℝ) (n : ℕ) : diff --git a/IsingModel/Concrete/LatticeGraphCorrelation/PolymerFreeEnergyHighTemperatureBoundsAlongEx.lean b/IsingModel/Concrete/LatticeGraphCorrelation/PolymerFreeEnergyHighTemperatureBoundsAlongEx.lean index fa570b3d3..173a61da7 100644 --- a/IsingModel/Concrete/LatticeGraphCorrelation/PolymerFreeEnergyHighTemperatureBoundsAlongEx.lean +++ b/IsingModel/Concrete/LatticeGraphCorrelation/PolymerFreeEnergyHighTemperatureBoundsAlongEx.lean @@ -5,7 +5,7 @@ import IsingModel.AmbientLattice.SpecialCases.PolymerFreeEnergyHighTemperatureBo # ℤ^d §18.5 AlongExhaustion `vdPolymerFamilies_sum` high-temperature bounds Instantiates the along-exhaustion high-temperature bounds and monotonicity of the -van-den-Berg polymer-family sum at `IsingModel.latticeGraph d`, the convergence input for +vertex-disjoint polymer-family sum at `IsingModel.latticeGraph d`, the convergence input for the ℤ^d cluster expansion. -/ diff --git a/docs/index.md b/docs/index.md index 2b5be3775..1eaf9119e 100644 --- a/docs/index.md +++ b/docs/index.md @@ -1898,7 +1898,7 @@ inventory (2026-04-17). | §17.5 | `m⁻`-scaled sharp convolution + exponential cancellation (Theorem 17.5.1, p. 312 c-denominator) | **Done (axiom-free; PR #4329)** | `IsingModel/PseudoMass/HLSSharpPairBound.lean`. Foundations for the GJ p. 312 `c`-denominator handling (where two-point functions are replaced by their `m⁻`-scaled rational majorants): `tsum_one_div_one_add_scaled_pow_pair_le` (`∃C>0, ∀x y, ∑'_z 1/(1+(t·d(x,z))^α)·1/(1+(t·d(y,z))^α) ≤ C·(1+d(x,y))^{−(2α−d)}` for `t>0`, `d/2<α0, Lemma_17_5_2_InfiniteHLSDenominatorComparison (cubicExhaustion d) J x z β α K (pseudoMass profile)`. Helper `lemma_17_5_2_profile_lower_ratio_lower_cubic`: `hprofile` ⇒ the *pair-independent* positive ratio lower bound `pseudoMassG α ρ q / q^(2α) ≤ c / m^(2α)` (via `m ≤ q` and `pseudoMassG ≥ 0`). **Method** (GJ p. 312, reorganized to avoid the exponential/polynomial mismatch): numerator `\|c'\|` bounded above by the pair-/stage-independent constant `B = J·(βJ2d/(1−βJ2d))²+J·4d` (existing susceptibility bound `lemma_17_5_2_finite_deriv_abs_le_high_temp_on_Icc_all_stages` + axiom-free window provider `ConvergenceRegion.derivativeLimit_on_window` + `le_of_tendsto`); `hprofile` lower-bounds `c/m^(2α)` by the constant `L = pseudoMassG α ρ q/q^(2α)`; `K := max 1 (B/L)` closes `\|c'\| ≤ B ≤ K·L ≤ K·c/m^(2α)`. All axiom-free `[propext, Classical.choice, Quot.sound]`. **Conditional/Partial:** the `∀`-displacement form of `hprofile` is *provably false* (no-go #4270) — a fixed-radius profile cannot lower-bound an exponentially-decaying correlation at all displacements — so this is a genuine per-pair hypothesis (satisfiable e.g. for large `ρ` at any active pair) matching the lower side of the existing §17.5 sandwich; the unconditional headline is the faithful distance-parametrized `globalPseudoMassDist_fullSandwich` (#4317). **Note (route):** this PR belongs to the #4320 sharp-HLS thread but, notably, the `hcomp` discharge *does not use the sharp-HLS convolution* `darts_cross_sum_le_sharp_decay` (#4326–#4329) at all — the numerator is controlled by the pair-independent susceptibility bound `B`, so the proof is strictly simpler than the originally-planned decay route; the #4321–#4329 foundations remain available for the unconditional (decay-based) route still gated on §18. Reference: GJ §17.5 Theorem 17.5.1, p. 312. (Issue #4320.) | | §17.5 | Conditional interval Lipschitz of (m⁻)^{2α+1} on the convergence window (Theorem 17.5.1 intermediate Lipschitz claim) | **Done (axiom-free, Partial/conditional; PR #4331)** | `IsingModel/Concrete/LatticeGraphCorrelation/Lemma_17_5_2/SharpHLSDenominatorComparison.lean`. `lemma_17_5_2_pseudoMass_pow_succ_lipschitz_on_window_of_profile_lower`: for a distinct pair `x ≠ z` and `Icc β₁ β₂ ⊆ ConvergenceRegion.window d J`, the interval profile lower bound `hprofile` (∀ β ∈ Icc) gives `∃ K>0, \|m⁻(β₂)^{2α+1} − m⁻(β₁)^{2α+1}\| ≤ (2α+1)·K/ρ·(β₂−β₁)` (`m⁻(β) = pseudoMassFromParamsAtPair … x z`). Feeds a **fixed-K** interval `hcomp` into the existing consumer `pseudoMassFromParamsAtPair_beta_pow_succ_lipschitz_on_Icc_of_corr_differentiableAt`. The single `K` combines: the pair-/stage-uniform numerator bound `B = J·(β₂J2d/(1−β₂J2d))²+J·4d` (susceptibility bound + axiom-free window provider `ConvergenceRegion.derivativeLimit_on_window` + `correlationInfinite_hasDerivAt_beta_of_tendstoLocallyUniformlyOn_deriv` + `le_of_tendsto`); and the **interval-uniform** ratio lower bound `L_min = pseudoMassG α ρ q₁/q₁^{2α}` (`q₁ = −log(β₁J2d)`) obtained from the per-β `lemma_17_5_2_profile_lower_ratio_lower_cubic` (#4330) plus monotonicity of `q` and `pseudoMassG_antitoneOn` (no compactness needed) — `q(β) ≤ q₁` for `β ≥ β₁`, so `L_min ≤ L(β) ≤ c/m^{2α}`. Then `K := max 1 (B/L_min)` closes `\|deriv c β\| ≤ B ≤ K·L_min ≤ K·c/m^{2α}` for all `β ∈ Icc`. Axiom-free `[propext, Classical.choice, Quot.sound]`. **Conditional/Partial:** `hprofile` is a genuine per-pair hypothesis (∀-displacement form false, #4270); the unconditional headline is `globalPseudoMassDist_fullSandwich` (#4317). **Downstream obstruction (documented):** the *system* `globalPseudoMassDist` (infinite lower envelope) continuity does **not** follow — large-separation pairs blow up the per-pair Lipschitz constant `(2α+1)K/ρ` — so this is the per-pair endpoint of the conditional Lipschitz chain. Reference: GJ §17.5 Theorem 17.5.1, pp. 311–312. (Issue #4320.) | -| §17.5 | **UNCONDITIONAL faithful correlation profile lower bound on the convergence window** (discharges the §17.5 `hprofile`, previously thought §18-gated) | **Done (axiom-free, UNCONDITIONAL; PR #4333)** | `IsingModel/Concrete/LatticeGraphCorrelation/Lemma_17_5_2/UnconditionalProfileLower.lean`. **The faithful per-pair correlation lower bound `pseudoMassG α (dist x z) (−log tanh(βJ)) ≤ ⟨φ_x φ_z⟩^∞` is proven UNCONDITIONALLY** for every distinct pair `x ≠ z` on `β ∈ ConvergenceRegion.window d J` — `pseudoMassG_dist_tanh_rate_le_correlationInfinite_cubic` (general pair) + `..._cubic_zero` (anchored). This is the genuine discharge of the §17.5 correlation-lower-bound hypothesis at the **faithful inverse-correlation-length rate `−log tanh(βJ)`** (NOT the slower Simon–Lieb rate `−log(βJ·2d)` whose ∀-displacement form is false, #4270). Method: (i) `pseudoMassG_le_exp_neg_of_one_le` — `1 ≤ t·r ⇒ pseudoMassG α r t ≤ e^{−tr}`; (ii) on the window `tanh(βJ) < R d ≤ e⁻¹` (`tanh_betaJ_lt_exp_neg_one_of_window`, via `R d = min(…) ≤ 1/(64((2d)²+1)e) ≤ e⁻¹`), so the rate `q := −log tanh(βJ) ≥ 1` (`one_le_neg_log_tanh_betaJ_of_window`), hence `q·dist ≥ 1` and `pseudoMassG α (dist) q ≤ e^{−q·dist} = tanh(βJ)^{dist}`; (iii) the GKS **direct-path** lower bound `twoPointFunction_ge_tanh_betaJ_pow_dist` gives `tanh(βJ)^{dist} ≤ ⟨φ₀φ_z⟩`; (iv) translation invariance (`correlationInfinite_latticeGraph_pair_eq_twoPointFunction`, `latticeDistance_translate_eq`) extends from anchored to general pairs. Axiom-free `[propext, Classical.choice, Quot.sound]`. **Significance:** the per-pair `hprofile` that gated the §17.5.1 conditional chain (#4330–#4332) is now an unconditional theorem on the window; re-parametrizing that chain to the `−log tanh(βJ)` rate (next PR) yields the **unconditional** finite-region `m⁻(σ,A)^{2α+1}` Lipschitz. Reference: GJ §17.5 Theorem 17.5.1 / Lemma 17.5.2, pp. 311–312; GKS direct path. (Issue #4320.) | +| §17.5 | **UNCONDITIONAL correlation profile lower bound at the direct-path rate on the convergence window** (supplies the ratio hypothesis of the rate-agnostic §17.5 Lipschitz engine, not the #4330–#4332 `hprofile` binder uniformly in its radius) | **Done (axiom-free, UNCONDITIONAL; PR #4333)** | `IsingModel/Concrete/LatticeGraphCorrelation/Lemma_17_5_2/UnconditionalProfileLower.lean`. **The per-pair correlation lower bound `pseudoMassG α (dist x z) (−log tanh(βJ)) ≤ ⟨φ_x φ_z⟩^∞` is proven UNCONDITIONALLY** for every distinct pair `x ≠ z` on `β ∈ ConvergenceRegion.window d J` — `pseudoMassG_dist_tanh_rate_le_correlationInfinite_cubic` (general pair) + `..._cubic_zero` (anchored). This is an unconditional correlation lower bound at the **direct-path rate `−log tanh(βJ)`** — the exponent of the GKS direct-path bound. For general `d` the tree relates that rate to the inverse correlation length only from above, by `latticeMass ≤ ofReal(−log tanh(βJ))` (`latticeMass_le_neg_log_tanh_betaJ`, bundled with the Simon–Lieb lower bound in `latticeMass_two_sided_bound`) and by the sharper on-axis `onAxisInverseCorrelationLength ≤ −log tanh(βJ)` (`onAxisInverseCorrelationLength_le_neg_log_tanh`); an equality is proved in `d = 1` only, where `latticeMass_one_eq_correlationMass` gives `latticeMass 1 (cubicExhaustion 1) ⟨J,0,β⟩ = ofReal(correlationMass (βJ))` with `correlationMass a = −log tanh a`. The bound is stated at the pair distance `dist x z` as radius, and at a different rate from the slower Simon–Lieb rate `−log(βJ·2d)` whose ∀-displacement form is false (#4270). Method: (i) `pseudoMassG_le_exp_neg_of_one_le` — `1 ≤ t·r ⇒ pseudoMassG α r t ≤ e^{−tr}`; (ii) on the window `tanh(βJ) < R d ≤ e⁻¹` (`tanh_betaJ_lt_exp_neg_one_of_window`, via `R d = min(…) ≤ 1/(64((2d)²+1)e) ≤ e⁻¹`), so the rate `q := −log tanh(βJ) ≥ 1` (`one_le_neg_log_tanh_betaJ_of_window`), hence `q·dist ≥ 1` and `pseudoMassG α (dist) q ≤ e^{−q·dist} = tanh(βJ)^{dist}`; (iii) the GKS **direct-path** lower bound `twoPointFunction_ge_tanh_betaJ_pow_dist` gives `tanh(βJ)^{dist} ≤ ⟨φ₀φ_z⟩`; (iv) translation invariance (`correlationInfinite_latticeGraph_pair_eq_twoPointFunction`, `latticeDistance_translate_eq`) extends from anchored to general pairs. Axiom-free `[propext, Classical.choice, Quot.sound]`. **Significance:** this does **not** discharge the `hprofile` binder of #4330–#4332 uniformly in that binder's radius. That binder is `pseudoMassG α ρ (−log(βJ·2d)) ≤ correlationInfinite {x,z}` at the **Simon–Lieb rate**, with `ρ` a free radius in #4330/#4331 and the pair distance `latticeDistance d x z` in #4332 — whereas the theorem here is at rate `−log tanh(βJ)` (radius `dist x z`). At #4332's **matched radius** the two statements differ only in the rate and the comparison closes: on the window `tanh(βJ) < βJ ≤ βJ·2d` for `1 ≤ d`, so the direct-path rate is the larger of the two, and `pseudoMassG` is antitone in the rate (`pseudoMassG_antitoneOn`) — the bound proved here is therefore *strictly weaker* than #4332's binder and does not discharge it. For the free-radius #4330/#4331 that rate-only inference is unavailable: `pseudoMassG α r t = 2·e^{−(t·r)}/(1+(t·r)^α)` depends on rate and radius only through the product `t·r`, strictly decreasing in it (`pseudoMassG_strictAntiOn` at `r = 1`), so the theorem here *does* yield their binder at every radius satisfying the criterion `ρ·(−log(βJ·2d)) ≥ dist x z·(−log tanh(βJ))`, and yields it at no radius where that criterion fails. At `ρ = 2·dist x z` the criterion reads `(βJ·2d)² ≤ tanh(βJ)`, which the window supplies with room to spare, and its left-hand side is increasing in `ρ` (the rate `−log(βJ·2d)` is positive on the window, `window_subset_highTemp`), so the criterion is met at every `ρ ≥ 2·dist x z`. What fails there is only the discharge uniform in `ρ`, the form #4330/#4331 are stated in. What it does discharge is the per-pair profile lower bound *at the tanh rate* that supplies the rate-free ratio hypothesis `hratio : Lmin ≤ c(β)/m(β)^{2α}` of the **rate-agnostic** engine `pseudoMassFromParamsAtPair_pow_succ_lipschitz_on_window_of_ratio_lower` (the engine itself carries no rate); re-parametrizing the chain through that engine (#4334) is what yields the **unconditional** finite-region `m⁻(σ,A)^{2α+1}` Lipschitz. Reference: GJ §17.5 Theorem 17.5.1 / Lemma 17.5.2, pp. 311–312; GKS direct path. (Issue #4320.) | | §17.5 | GJ Theorem 17.5.1 proof — PR-1d: per-dart correlation ratio (binding pair) | **Done (axiom-free; PR #4338; toward Thm 17.5.1)** | `IsingModel/Concrete/LatticeGraphCorrelation/Lemma_17_5_2/MassContinuityDartSum.lean`. `correlationInfinite_dart_ratio_le`: for a distinct binding pair `x ≠ y` (`m⁻(x,y) = globalPseudoMassDist`) and an adjacent dart `u ∼ v` (`x≠u`, `y≠v`), `⟨φ_x φ_u⟩·⟨φ_y φ_v⟩/⟨φ_x φ_y⟩ ≤ 2·e^{m⁻}·(1+(m⁻·d(x,y))^α)·(1/(1+(m⁻·d(x,u))^α))·(1/(1+(m⁻·d(y,v))^α))` — the per-term bound of the GJ p.312 sum. Composes #4335 (system-mass majorant + (17.5.3) identity) + #4337 (`pseudoMassG_ratio_le` profile-ratio algebra + `exp_neg_scaled_dart_pair_le_exp` dart exp-cancellation): numerator factors majorized, denominator = profile at the binding pair, ratio-algebra closes. Axiom-free. Next (PR-1e): dart-sum assembly via the fiber decomposition (mirror #4329) + #4336 convolution ⇒ `Σ_dart ⟨xδ⟩⟨yδ⟩/c ≤ const·(1+(m⁻r)^α)(1+r)^{d-2α}`. Reference: GJ §17.5 Theorem 17.5.1, p. 312. (Issue #4320.) | | §17.5 | GJ Theorem 17.5.1 proof — PR-1e core: c-cancelling incident Lebowitz β-derivative bound | **Done (axiom-free; toward Thm 17.5.1)** | `IsingModel/BetaDerivative/LebowitzCancelling.lean`. `summand_le_symmDiff`: the c-cancelling per-summand bound `corr(A△B) − corr(A)·corr(B) ≤ corr(A△B)` (drop the non-negative GKS-I product). `correlation_beta_deriv_le_lebowitz_cancelling`: the c-cancelling variant of `correlation_beta_deriv_le_lebowitz_tight` — the *incident* (degenerate) edges contribute the **reduced** correlation `corr({r,s}△{e})` instead of the coarse `1`, i.e. `∂_β ⟨σ_r σ_s⟩ ≤ J·∑_e leb_e + J·∑_{e incident} corr({r,s}△{e})`. This is GJ's `2A` mechanism: for an incident edge `{r,v}`, `corr({r,s}△{r,v}) = ⟨σ_s σ_v⟩` and `⟨σ_s σ_v⟩/c` stays bounded (`v∼r ⇒ dist(s,v) ≥ dist(r,s)−1`), replacing the loose `J·|incident|/c` that blows up in the p.312 mass-continuity estimate. Method: mirror the tight Lebowitz proof, splitting `edgeFinset` into incident/disjoint; on the disjoint part use `summand_le_lebowitz_of_disjoint`, on the incident part use `summand_le_symmDiff`. Axiom-free `[propext, Classical.choice, Quot.sound]`. Reference: GJ §17.5 Theorem 17.5.1 proof, p. 312. (Issue #4320.) | | §17.5 | GJ Theorem 17.5.1 proof — PR-1e: cubic c-cancelling finite-volume Lebowitz profile bound | **Done (axiom-free; toward Thm 17.5.1)** | `IsingModel/Concrete/LatticeGraphCorrelation/Lemma_17_5_2/CubicDerivativeProfileCancelling.lean`. `derivative_profile_cubic_le_lebowitz_cancelling`: the c-cancelling counterpart of `derivative_profile_cubic_le_lebowitz_tight` — for `0≤J`, `0<β`, `x≠z`, `{x,z}⊆volume n`, `∂_β c_n ≤ J·∑_{⟨u,v⟩∈E}[⟨σ_xσ_u⟩⟨σ_zσ_v⟩+⟨σ_xσ_v⟩⟨σ_zσ_u⟩] + J·∑_{e incident} corr({⟨x⟩,⟨z⟩}△{e})`, where the incident (degenerate) edges contribute the **reduced** correlation `corr({⟨x⟩,⟨z⟩}△{e})` instead of the coarse `1` (per-edge `card`). This carries GJ's bounded `2A` mechanism (#4339 `correlation_beta_deriv_le_lebowitz_cancelling`) to the cubic finite-volume profile, via `correlationAlongExhaustion_of_subset` + `liftFinset_pair` (same profile-identification as the tight version). Axiom-free. Next: infinite-volume bridge (reduce the incident `corr({⟨x⟩,⟨z⟩}△{e})` to `corr∞{z,v}` / `corr∞{x,v}` and bound `/c` via the single-factor pseudoMassG majorant, `dist(z,v)≥r−1`). Reference: GJ §17.5 Theorem 17.5.1 proof, p. 312. (Issue #4320.) | @@ -1922,7 +1922,7 @@ inventory (2026-04-17). | §17.5 | GJ Theorem 17.5.1 proof — PR-1j: n-uniform combined β-derivative `/c` bound | **Done (axiom-free; toward Thm 17.5.1)** | `IsingModel/Concrete/LatticeGraphCorrelation/Lemma_17_5_2/MassContinuityDerivCombineUniform.lean`. `combined_derivative_div_c_bound_tight_uniform`: `∃C>0, ∀ n, {x,z}⊆volume n → ∂_β c_n/c ≤ J·[2(1+(m⁻r)^α)e^{m⁻}·C(1+r)^{−(2α−d)}] + J·[4d(1+2^α)e^{m⁻}]` — the **same** `C` for every exhaustion stage `n`. The n-uniform version of #4356, with `C` from the n-uniform convolution #4357 and the `∀n` quantifier inside (the bounded incident #4355 is already n-independent). This is the finite-stage bound the `n→∞` limit consumes. Same proof structure as #4356 with `C` out front + per-`n` `hCbd n x z` (#4357). Axiom-free `[propext, Classical.choice, Quot.sound]`. Next: `hgB_sharp` (limit ⇒ `|g'|≤c·⟨sharp⟩` via `derivativeLimit_on_window` + GKS-II monotonicity) + uniform-K consumer variant ⇒ uniform Lipschitz ⇒ system continuity ⇒ capstone. Reference: GJ §17.5 Theorem 17.5.1 proof, p. 312. (Issue #4320.) | | §17.5 | GJ Theorem 17.5.1 proof — PR-1j: sharp infinite-volume β-derivative bound | **Done (axiom-free; toward Thm 17.5.1)** | `IsingModel/Concrete/LatticeGraphCorrelation/Lemma_17_5_2/MassContinuityDerivInfiniteSharp.lean`. `abs_deriv_correlationInfinite_le_sharp`: for a non-adjacent binding pair `x≠z` with `m⁻(x,z)=globalPseudoMassDist>0` at `β∈window`, `∃C>0, |∂_β ⟨φ_xφ_z⟩^∞| ≤ ⟨sharp(C)⟩·⟨φ_xφ_z⟩^∞` where `⟨sharp(C)⟩ = J·[2(1+(m⁻r)^α)e^{m⁻}C(1+r)^{−(2α−d)}] + J·[4d(1+2^α)e^{m⁻}]`. The `n→∞` limit of #4358: the finite-stage deriv ∈ `[0, c·⟨sharp⟩]` (GKS-II monotonicity `correlationAlongExhaustion_latticeGraph_beta_deriv_nonneg` + #4358), so the limit `g'β` (via `derivativeLimit_on_window` + `correlationInfinite_hasDerivAt_beta_…`) has `|g'β|≤c·⟨sharp⟩` (`le_of_tendsto` + eventually-{x,z}⊆vol n via `exhaust`). Axiom-free `[propext, Classical.choice, Quot.sound]`. Next: uniform-K consumer variant (`K=⟨sharp⟩·m^{2α}=const·dist`, α≥d−1 + m⁻ bounded) ⇒ uniform `m⁻^{2α+1}` Lipschitz ⇒ lower-envelope/A↑ ⇒ capstone. Reference: GJ §17.5 Theorem 17.5.1 proof, p. 312. (Issue #4320.) | | §17.5 | GJ Theorem 17.5.1 proof — PR-1j-prep: interval-uniform m⁻ lower bound | **Done (axiom-free; toward Thm 17.5.1)** | `IsingModel/Concrete/LatticeGraphCorrelation/Lemma_17_5_2/MassContinuityGlobalMassLowerIcc.lean`. `globalPseudoMassDist_ge_restrictedRate_beta2`: for `β∈Icc β₁ β₂` with `0<β₁`, `β₂·J·(2d)<1/2` (strict high-temp window), `globalPseudoMassDistRestrictedRate α d J β₂ ≤ m⁻(β)` — a single positive constant lower bound uniform over the interval. The prerequisite for the uniform convolution `C` (which `~(m⁻)^{−α}` blows up as `m⁻→0`). Proof: per-β `m⁻(β) ≥ RestrictedRate(β)` (`globalPseudoMassDistRestrictedRate_le_globalPseudoMassDist`); `RestrictedRate` antitone in β (`−log(B/(1−B))` via `div_le_div_iff₀`+`Real.log_le_log`, and `simonLiebRate=−log B`, both decreasing as `B=βJ2d` increases; `min_le_min`). Axiom-free `[propext, Classical.choice, Quot.sound]`. Next: m⁻ upper bound + uniform `C` (#4336 `Ct(mmin)`) + uniform-K rpow + consumer ⇒ uniform Lipschitz ⇒ lower-envelope/A↑ ⇒ capstone. Reference: GJ §17.5 Theorem 17.5.1 proof, p. 312. (Issue #4320.) | -| §17.5 | GJ Theorem 17.5.1 proof — PR-1j-prep: interval-uniform per-pair m⁻ upper bound | **Done (axiom-free; toward Thm 17.5.1)** | `IsingModel/Concrete/LatticeGraphCorrelation/Lemma_17_5_2/MassContinuityPairMassUpperIcc.lean`. `pseudoMassFromParamsAtPairDist_le_neg_log_tanh_beta1_on_Icc`: for a distinct pair `x≠z` and `β∈Icc β₁ β₂` with `0<β₁`, `Icc⊆ConvergenceRegion.window`, `pseudoMassFromParamsAtPairDist … ⟨J,0,β⟩ x z ≤ −log tanh(β₁·J)` — a single constant upper bound uniform over the interval (companion to the lower bound #4360; gives `Mmax` for the `m^{2α}` factor in the uniform Lipschitz constant). Proof: per-β `m⁻(x,z) ≤ −log tanh(βJ)` (faithful rate #4333 `pseudoMassG_dist_tanh_rate_le_correlationInfinite_cubic` + `pseudoMass_le_iff_pseudoMassG_le`); the faithful rate is antitone in β (`Real.tanh_strictMono` + `Real.log_le_log`). Axiom-free `[propext, Classical.choice, Quot.sound]`. **With #4360 (lower), the interval-uniform two-sided m⁻ bounds `mmin ≤ m⁻ ≤ Mmax` are now both available** (per-pair upper; global lower). Next: uniform `C` (#4336 `Ct(mmin)`) + uniform-K rpow + consumer ⇒ uniform Lipschitz ⇒ lower-envelope/A↑ ⇒ capstone. Reference: GJ §17.5 Theorem 17.5.1 proof, p. 312. (Issue #4320.) | +| §17.5 | GJ Theorem 17.5.1 proof — PR-1j-prep: interval-uniform per-pair m⁻ upper bound | **Done (axiom-free; toward Thm 17.5.1)** | `IsingModel/Concrete/LatticeGraphCorrelation/Lemma_17_5_2/MassContinuityPairMassUpperIcc.lean`. `pseudoMassFromParamsAtPairDist_le_neg_log_tanh_beta1_on_Icc`: for a distinct pair `x≠z` and `β∈Icc β₁ β₂` with `0<β₁`, `Icc⊆ConvergenceRegion.window`, `pseudoMassFromParamsAtPairDist … ⟨J,0,β⟩ x z ≤ −log tanh(β₁·J)` — a single constant upper bound uniform over the interval (companion to the lower bound #4360; gives `Mmax` for the `m^{2α}` factor in the uniform Lipschitz constant). Proof: per-β `m⁻(x,z) ≤ −log tanh(βJ)` (direct-path rate #4333 `pseudoMassG_dist_tanh_rate_le_correlationInfinite_cubic` + `pseudoMass_le_iff_pseudoMassG_le`); the direct-path rate is antitone in β (`Real.tanh_strictMono` + `Real.log_le_log`). Axiom-free `[propext, Classical.choice, Quot.sound]`. **With #4360 (lower), the interval-uniform two-sided m⁻ bounds `mmin ≤ m⁻ ≤ Mmax` are now both available** (per-pair upper; global lower). Next: uniform `C` (#4336 `Ct(mmin)`) + uniform-K rpow + consumer ⇒ uniform Lipschitz ⇒ lower-envelope/A↑ ⇒ capstone. Reference: GJ §17.5 Theorem 17.5.1 proof, p. 312. (Issue #4320.) | | §17.5 | GJ Theorem 17.5.1 proof — PR-1j-final: mass-uniform HLS convolution bound | **Done (axiom-free; toward Thm 17.5.1)** | `IsingModel/Concrete/LatticeGraphCorrelation/Lemma_17_5_2/MassContinuityConvolutionMassUniform.lean`. `tsum_mul_neighborFinset_sum_scaled_le_uniform`: for `d<2α<2d` and fixed `mmin>0`, `∃C>0, ∀ t≥mmin, ∀ x z, ∑'_u s_t(x,u)·∑_{v∼u}s_t(z,v) ≤ C·(1+d(x,z))^{−(2α−d)}` — the **same** `C` for every scale `t≥mmin`. The mass-uniform version of #4336, needed because the GJ p.312 Lipschitz uses the convolution at the β-varying `m⁻(β)` and the per-scale `Ct=max 1 (t^α)⁻¹·2^α` blows up as `t→0`. With `t≥mmin` (#4360), `Ct≤Ctmax=max 1 (mmin^α)⁻¹·2^α` (via `inv_anti₀` + `pow_le_pow_left₀`), so the per-kernel domination holds at the scale-independent `Ctmax`, giving `C=Ctmax²·C₀`. Same proof structure as #4336 with `Ctmax`. Axiom-free `[propext, Classical.choice, Quot.sound]`. Next: uniform-K rpow (`K=⟨sharp⟩·m^{2α}=const·dist`, two-sided m⁻ bounds #4360/#4361 + α≥d−1) + consumer feed ⇒ uniform Lipschitz ⇒ lower-envelope/A↑ ⇒ capstone. Reference: GJ §17.5 Theorem 17.5.1 proof, p. 312. (Issue #4320.) | | §17.5/§18 / FFS Ch 12 | Sharp `tanh`-coefficient lattice-mass lower bound (sharp-decay programme, brick 4 — programme complete) | **Done (axiom-free; toward true-mass continuity #4386)** | `Concrete/LatticeGraphCorrelation/SharpLatticeMassLowerBound.lean`. The infinite-volume completion of #4393. `correlationInfinite_simon_lieb_sharp`: infinite-volume sharp Simon–Lieb `⟨φ_iφ_j⟩_∞ ≤ tanh(βJ)·∑_{k∼i}⟨φ_kφ_j⟩_∞` (brick 2 through `correlationInfinite_eq_ciSup`; per-stage kernel dominated by the infinite-volume correlation, induced neighbours inject into `G`-neighbours). `correlationInfinite_latticeGraph_le_tanh_two_d_pow_of_dist_gt`: `⟨φ_iφ_j⟩_∞ ≤ (tanh βJ·2d)^{n}` for `n+1 ≤ dist` (induction via the one-step `…_le_of_neighbors_le_sharp`). `hasExponentialDecay_tanh_of_high_temp`: rate-`−log(tanh βJ·2d)` decay (`C = 1/(tanh βJ·2d)`). **Headline** `latticeMass_ge_neg_log_tanh_of_high_temp`: `ofReal(−log(tanh βJ·2d)) ≤ latticeMass(σ)` — sharper than `latticeMass_ge_neg_log_of_high_temp` (rate `−log(βJ·2d)`, since `tanh βJ < βJ`). Tightens the GJ §17.5 Lemma 17.5.2 sandwich constant; the residual `log(2d)` gap to the upper bound `−log tanh` needs the Ornstein–Zernike exact rate (#4386), so this does not by itself close Thm 17.5.1. Axiom-free `[propext, Classical.choice, Quot.sound]`. Reference: GJ §17.5/§18; FFS *Random Walks…* (1992) Ch 12; FV §3.7.3. (Issue #4393.) | | §18 / FFS Ch 12 | Sharp `tanh`-coefficient Simon–Lieb distance decay (sharp-decay programme, bricks 2–3) | **Done (axiom-free; toward sharp two-point decay #4393)** | `Inequalities/SharpSimonLiebNeighbor.lean`. **Brick 2** `correlation_inducedGraph_simon_lieb_neighbor_sharp`: the neighbour form `⟨σ_iσ_j⟩ ≤ tanh(βJ)·∑_{u∼i} K(j,u)` (`K = simonLiebKernel`), reindexing the brick-1 edge sum via `Finset.sum_bij'` (`correlation_symmDiff_eq_simonLiebKernel`). **Brick 3** `correlation_inducedGraph_le_tanh_pow_dist`: the **sharp exponential decay** `⟨σ_iσ_j⟩ ≤ (tanh(βJ)·D)^{dist(i,j)−1}` for a degree bound `D` and `0 < dist(i,j)` — sharper than `correlation_inducedGraph_le_pow_dist` (coefficient `β·J·D`), giving rate `−log(tanh(βJ)·D)` (with `D=2d` on `ℤ^d`: `−log(2d·tanh βJ)`). Proof: direct strong induction `correlation_inducedGraph_le_tanh_pow_of_lt_dist` (base `⟨⟩≤1`; step via brick 2 + `Adj.diff_dist_adj` neighbour-distance bound + `simonLiebKernel_of_ne` + `≤D` neighbours), mirroring `simonLiebIterate_le_pow_of_lt_dist` but consuming the sharp neighbour inequality directly. Axiom-free `[propext, Classical.choice, Quot.sound]`. Reference: GJ §18; FFS *Random Walks…* (1992) Ch 12; FV §3.7.3. (Issue #4393.) | @@ -1969,7 +1969,7 @@ inventory (2026-04-17). | §17.5 | GJ Theorem 17.5.1 proof — PR-1c: dart exp-cancellation + pseudoMassG profile-ratio algebra | **Done (axiom-free; PR #4337; toward Thm 17.5.1)** | `IsingModel/Concrete/LatticeGraphCorrelation/Lemma_17_5_2/MassContinuityDartRatio.lean`. Two per-dart building blocks of the GJ p.312 ratio: `exp_neg_scaled_dart_pair_le_exp` (edge analog of #4329: for adjacent `u∼v`, `exp(−t(d(x,u)+d(y,v)−d(x,y))) ≤ exp t` via the triangle through the edge, `d(x,y) ≤ d(x,u)+1+d(y,v)`), and `pseudoMassG_ratio_le` (profile-ratio algebra: `P(a)P(b)/P(c) = 2(1+(mc)^α)·s_a·s_b·e^{−m(a+b−c)} ≤ 2(1+(mc)^α)·s_a·s_b·e^m` for `m,a,b,c ≥ 0`, `s_r = 1/(1+(mr)^α)`, given the exp bound). Combined with #4335 (majorant/identity) + #4336 (dart scaled convolution) these give the per-dart correlation ratio and the dart-sum/c bound (PR-1d). Axiom-free. Reference: GJ §17.5 Theorem 17.5.1, p. 312. (Issue #4320.) | | §17.5 | GJ Theorem 17.5.1 proof — PR-1b: m⁻-scaled neighbour-shift (dart) HLS convolution | **Done (axiom-free; PR #4336; toward Thm 17.5.1)** | `IsingModel/Concrete/LatticeGraphCorrelation/Lemma_17_5_2/MassContinuityDartScaledHLS.lean`. `tsum_mul_neighborFinset_sum_scaled_le`: for `t>0`, `d/2<α0, ∀x z, ∑'_u 1/(1+(t·d(x,u))^α)·(∑_{v∼u}1/(1+(t·d(z,v))^α)) ≤ C·(1+d(x,z))^{−(2α−d)}` — the `t=m⁻` scaled, edge/dart form of the HLS convolution (the Ising β-derivative Lebowitz bound is a nearest-neighbour edge cross-sum, not GJ's site sum). Each scaled kernel reduces to `Ct·(1+d)^{−α}` (`one_div_one_add_M_t_pow_le_const_mul_one_div_one_add_pow_pow`), so the bound follows from the unscaled neighbour-shift convolution `tsum_mul_neighborFinset_sum_pow_neg_le` (#4327); `C = Ct²·C₄₃₂₇`. Axiom-free. This is the convolution at the heart of the GJ p.312 derivative-ratio bound; combined with the #4335 majorant + identity + triangle exp-cancellation it gives the dart-sum/c ratio. Reference: GJ §17.5 Theorem 17.5.1, p. 312. (Issue #4320.) | | §17.5 | GJ Theorem 17.5.1 proof — PR-1 foundations: system-mass correlation majorant + pseudo-mass identity | **Done (axiom-free; PR #4335; toward Thm 17.5.1)** | `IsingModel/Concrete/LatticeGraphCorrelation/Lemma_17_5_2/MassContinuityRatioBound.lean`. First ingredients of the genuine GJ §17.5 Theorem 17.5.1 (mass continuity) proof (pp.311–312), correcting the earlier mistaken 'blocked' assessment. `correlationInfinite_eq_pseudoMassG_pairDist`: the GJ (17.5.3) **defining identity** `⟨φ_x φ_y⟩ = pseudoMassG α (dist x y) (m⁻(x,y))` (denominator handled by identity, not majorized). `correlationInfinite_le_pseudoMassG_globalPseudoMassDist`: the GJ **system-mass majorant** `⟨φ_x φ_w⟩ ≤ pseudoMassG α (dist x w) (globalPseudoMassDist)` (each correlation = profile at its own per-pair mass; system mass ≤ per-pair via `globalPseudoMassDist_le_of_active`; `pseudoMassG_antitoneOn`). These feed the p.312 derivative-ratio bound (sharp HLS #4325–#4329 + triangle exp-cancellation), whose linear-in-dist scaling gives the A-uniform Lipschitz constant (K = const·dist), hence m⁻(σ) continuity and (Lemma 17.5.2 sandwich #4317) m(σ) continuity. Axiom-free `[propext, Classical.choice, Quot.sound]`. Roadmap (PR-1 ratio bound → PR-2 per-pair uniform Lipschitz → PR-3 uniform finite-region → PR-4 global continuity → PR-5 capstone) in #4320. Reference: GJ §17.5 Theorem 17.5.1, pp. 311–312. (Issue #4320.) | -| §17.5 | **UNCONDITIONAL finite-region Lipschitz of m⁻(σ,A)^{2α+1} on the convergence window** (GJ Lemma 17.5.2(a): continuity → Lipschitz, hypothesis-free) | **Done (axiom-free, UNCONDITIONAL; PR #4334)** | `IsingModel/Concrete/LatticeGraphCorrelation/Lemma_17_5_2/UnconditionalFiniteRegionLipschitz.lean`. **Removes the `hprofile` hypothesis from #4332**: `finiteRegionPseudoMassDist_pow_succ_lipschitz_on_window` — for a fixed bounded region `A` (≥1 distinct pair) and `Icc β₁ β₂ ⊆ ConvergenceRegion.window d J`, `∃ C>0, \|m⁻(σ₂,A)^{2α+1} − m⁻(σ₁,A)^{2α+1}\| ≤ C·(β₂−β₁)` **with no profile hypothesis**. Route: (i) rate-agnostic engine `pseudoMassFromParamsAtPair_pow_succ_lipschitz_on_window_of_ratio_lower` (extracts #4331's proof, taking the interval-uniform ratio lower bound `Lmin ≤ c/m^{2α}` as a hypothesis — numerator `B`, window provider, differentiability all rate-agnostic); (ii) general-rate `pseudoMassFromParamsAtPair_ratio_lower_of_pseudoMassG_le_corr` (rate-generalized #4330 via `pseudoMass_le_iff_pseudoMassG_le`); (iii) `pseudoMassFromParamsAtPairDist_pow_succ_lipschitz_on_window` — the **unconditional** per-pair distance interval Lipschitz, discharging `hprofile` at the faithful rate `−log tanh(βJ)` via #4333's `pseudoMassG_dist_tanh_rate_le_correlationInfinite_cubic`, with `Lmin = pseudoMassG α (dist) q₁/q₁^{2α}` (`q₁ = −log tanh(β₁J)`) interval-uniform by monotonicity of `q(β)=−log tanh(βJ)` (decreasing, via `Real.tanh_strictMono`) and `pseudoMassG_antitoneOn`; (iv) the finite `Finset.inf'` assembly (odd-power commutes with `inf'`, `inf'` of finitely-many Lipschitz via `choose!`+`Finset.sup'`+achieved infimum, as in #4332). Axiom-free `[propext, Classical.choice, Quot.sound]`. **The §17.5.1 finite-region Lipschitz is now unconditional** (the conditional #4330–#4332 are subsumed). The remaining open items are the *infinite-envelope* `globalPseudoMassDist` continuity (uniform-in-A, documented obstruction #4320) and the true-mass `latticeMass` continuity (transfer gap #4081). Reference: GJ §17.5 Theorem 17.5.1 / Lemma 17.5.2, pp. 311–312. (Issue #4320.) | +| §17.5 | **UNCONDITIONAL finite-region Lipschitz of m⁻(σ,A)^{2α+1} on the convergence window** (GJ Lemma 17.5.2(a): continuity → Lipschitz, hypothesis-free) | **Done (axiom-free, UNCONDITIONAL; PR #4334)** | `IsingModel/Concrete/LatticeGraphCorrelation/Lemma_17_5_2/UnconditionalFiniteRegionLipschitz.lean`. **Removes the `hprofile` hypothesis from #4332**: `finiteRegionPseudoMassDist_pow_succ_lipschitz_on_window` — for a fixed bounded region `A` (≥1 distinct pair) and `Icc β₁ β₂ ⊆ ConvergenceRegion.window d J`, `∃ C>0, \|m⁻(σ₂,A)^{2α+1} − m⁻(σ₁,A)^{2α+1}\| ≤ C·(β₂−β₁)` **with no profile hypothesis**. Route: (i) rate-agnostic engine `pseudoMassFromParamsAtPair_pow_succ_lipschitz_on_window_of_ratio_lower` (extracts #4331's proof, taking the interval-uniform ratio lower bound `Lmin ≤ c/m^{2α}` as a hypothesis — numerator `B`, window provider, differentiability all rate-agnostic); (ii) general-rate `pseudoMassFromParamsAtPair_ratio_lower_of_pseudoMassG_le_corr` (rate-generalized #4330 via `pseudoMass_le_iff_pseudoMassG_le`); (iii) `pseudoMassFromParamsAtPairDist_pow_succ_lipschitz_on_window` — the **unconditional** per-pair distance interval Lipschitz, supplying that ratio hypothesis from the **direct-path-rate** (`−log tanh(βJ)`) profile lower bound #4333 `pseudoMassG_dist_tanh_rate_le_correlationInfinite_cubic`, with `Lmin = pseudoMassG α (dist) q₁/q₁^{2α}` (`q₁ = −log tanh(β₁J)`) interval-uniform by monotonicity of `q(β)=−log tanh(βJ)` (decreasing, via `Real.tanh_strictMono`) and `pseudoMassG_antitoneOn`; (iv) the finite `Finset.inf'` assembly (odd-power commutes with `inf'`, `inf'` of finitely-many Lipschitz via `choose!`+`Finset.sup'`+achieved infimum, as in #4332). Axiom-free `[propext, Classical.choice, Quot.sound]`. **The §17.5.1 finite-region Lipschitz is now unconditional** (the conditional #4330–#4332 are subsumed). The remaining open items are the *infinite-envelope* `globalPseudoMassDist` continuity (uniform-in-A, documented obstruction #4320) and the true-mass `latticeMass` continuity (transfer gap #4081). Reference: GJ §17.5 Theorem 17.5.1 / Lemma 17.5.2, pp. 311–312. (Issue #4320.) | | §17.5 | Conditional finite-region Lipschitz of m⁻(σ,A)^{2α+1} on the convergence window (Lemma 17.5.2(a) continuity → Lipschitz) | **Done (axiom-free; PR #4332; subsumed by the unconditional #4334)** | `IsingModel/Concrete/LatticeGraphCorrelation/Lemma_17_5_2/FiniteRegionPseudoMassDistLipschitz.lean`. Upgrades the finite-region continuity (`finiteRegionPseudoMassDist_beta_continuousOn_high_temp`) to a **Lipschitz** estimate of the (2α+1)-power, for each *fixed* bounded region `A`. `finiteRegionPseudoMassDist_pow_succ_lipschitz_on_window_of_profile_lower`: for `Icc β₁ β₂ ⊆ ConvergenceRegion.window d J` and the faithful per-pair profile lower bounds (one per distinct pair of `A`), `∃ C>0, \|m⁻(σ₂,A)^{2α+1} − m⁻(σ₁,A)^{2α+1}\| ≤ C·(β₂−β₁)` (`m⁻(σ,A) = finiteRegionPseudoMassDist`). Route: the **bridge** `pseudoMassFromParamsAtPairDist_eq_atPair_cubic` (distance-radius = fixed-radius pseudo-mass at `r = dist`, cubic exhaustion making the `Fintype edgeSet` instances canonical — a general-`Λ` bridge is blocked by a `pseudoMassExt` `dite` defeq divergence on the synthesized-vs-passed instance mismatch, #4320); the **per-pair** distance Lipschitz `pseudoMassFromParamsAtPairDist_pow_succ_lipschitz_on_window_of_profile_lower` (= #4331 at ρ:=dist, constant (2α+1)K/dist); the **finite-region** assembly: (inf')^{2α+1} = inf'((·)^{2α+1}) (odd power monotone, `Finset.comp_inf'_eq_inf'_comp`), and inf' of finitely-many Lipschitz functions is Lipschitz with constant `Finset.sup'` of the per-pair constants (`choose!` + achieved-inf `Finset.exists_mem_eq_inf'` + `Finset.inf'_le`). Axiom-free `[propext, Classical.choice, Quot.sound]`. **Conditional/Partial:** per-pair `hprofile` faithful distance form (∀-displacement false, #4270); the constant is **per-`A`** — uniform-in-`A` / infinite-envelope `globalPseudoMassDist` continuity does **not** follow (per-pair Lipschitz constant (2α+1)K/dist uncontrolled as diam A→∞, #4320). Builds on #4330/#4331. Reference: GJ §17.5 Theorem 17.5.1 / Lemma 17.5.2, pp. 311–312. (Issue #4320.) | | §17.5 | Lipschitz continuity of (m⁻)^{2α+1} on interval (Step 134) | **Done** | `pseudoMass_pow_succ_lipschitz`: MVT applied to `β' ↦ (h β')^(2α+1)` — given derivative bound holds on [β₁,β₂], `|(h β₂)^(2α+1) - (h β₁)^(2α+1)| ≤ ↑(2α+1)*K/r*(β₂-β₁)`. Abstract Lipschitz continuity of GJ §17.5 Thm 17.5.1. (`IsingModel/PseudoMass.lean`, PR #950 Step 134.) | | §17.5 | Lipschitz derivative of (m⁻)^{2α+1} (Step 133) | **Done** | `pseudoMass_pow_succ_deriv_bound`: given hypotheses of Step 131b, derivative of `β ↦ (h β)^(2α+1)` has `|d| ≤ ↑(2α+1) * K / r`. Abstract derivative/Lipschitz core of GJ §17.5 Thm 17.5.1 proof. Chain rule + `pseudoMass_power_deriv_le`. (`IsingModel/PseudoMass.lean`, PR #949 Step 133.) |