wave 12 of 16

IsingModel/AmbientLattice/Analyticity.lean

@@ -20,241 +20,30 @@ import IsingModel.AmbientLattice.AnalyticityLambdaSection186
 import IsingModel.AmbientLattice.AnalyticityLambdaCapstones
 
 /-!
-# Joint analyticity for AmbientLattice finite-volume Λ-restricted Ising
-
-Lifts the joint analyticity of `partitionFunction` and `freeEnergy` in
-`(β, J, h) ∈ ℝ × ℝ × ℝ` (Glimm-Jaffe §18.6 capstone, established in
-`IsingModel/ClusterExpansion.lean` via direct sum-of-exp analyticity)
-to the finite-volume Λ-restricted versions defined in
-`IsingModel/AmbientLattice/Defs.lean`. Each theorem is a thin wrapper
-around the corresponding theorem on `inducedGraph G Λ`.
+# Λ-restricted analyticity: aggregation point
+
+This module declares nothing — no definition, no theorem, no instance — so its imports
+serve re-export alone, and importing this path is what brings the whole generic
+`AnalyticityLambda*` development into scope at once; the `latticeGraph` specializations of
+it are downstream of these children and are not reachable from here. Every name reachable
+through it is declared in one of its imports: the ambient-lattice definitions, the
+base-layer cluster expansion, and the `AnalyticityLambda*` modules.
+
+What those imports develop is the Glimm-Jaffe §18.4-§18.6 cluster expansion, and the
+regularity that accompanies it, transported from a graph on a finite vertex type to the
+induced subgraph `inducedGraph G Λ` of an ambient `G : SimpleGraph V` on a finite volume
+`Λ : Finset V`. Two kinds of subject occur there. `partitionFunctionΛ`, `freeEnergyΛ`,
+`correlationΛ`, `magnetizationΛ` and `susceptibilityΛ` are Λ-layer definitions, each
+unfolding to its base-layer counterpart at `inducedGraph G Λ`. `polymerFreeEnergy`,
+`mayerPartialSum`, `mayerExpansionTerm`, `allPolymers` and `vdCompatiblePolymerFamilies`
+have no Λ-layer definition of their own and are applied to `inducedGraph G Λ` directly;
+there it is only the theorem names that carry a `_Λ` marker.
 -/
 
 namespace IsingModel
 namespace Ambient
 
 variable {V : Type*} [DecidableEq V]
 
-
-/-! ## Moved: Λ-level joint analyticity wrappers
-
-The 10 Λ-level joint analyticity wrappers (partitionFunctionΛ +
-freeEnergyΛ + correlationΛ AnalyticAt / AnalyticOnNhd / Continuous /
-Differentiable joint) now live in
-`IsingModel.AmbientLattice.AnalyticityLambdaJoint`.
-The earlier import path is preserved by re-importing the new child.
--/
-
-
-
-/-! ## Moved: magnetizationΛ + susceptibilityΛ analyticity wrappers
-
-The 14 magnetizationΛ + susceptibilityΛ + correlationΛ
-continuousAt/differentiableAt/analyticAt/analyticOnNhd joint wrappers
-now live in
-`IsingModel.AmbientLattice.AnalyticityLambdaMagSuscep`.
-The earlier import path is preserved by re-importing the new child.
--/
-
-
-/-! ## Moved: Λ partitionFunction per-direction regularity wrappers
-
-The 6 partitionFunctionΛ per-direction Continuous / Differentiable
-wrappers at general h now live in
-`IsingModel.AmbientLattice.AnalyticityLambdaPerDirection`.
-The earlier import path is preserved by re-importing the new child.
--/
-
-/-! ## §18.4-§18.5 polymerFreeEnergy / vdSum / ε wrappers (now split)
-
-The Λ-layer wrappers for the §18.4-§18.5 polymerFreeEnergy /
-vdPolymerFamilies_sum / mayerPartialSum / mayerExpansionTerm /
-ε(t) / log_vdPolymerFamilies_sum / Mayer identity / strict-mono /
-iff family bundles originally lived inline below this header. They
-have been refactored out into narrow child modules
-(`AnalyticityLambdaPolymer`, `AnalyticityLambdaSandwich`,
-`AnalyticityLambdaPolymerBounds`, `AnalyticityLambdaMayer`,
-`AnalyticityLambdaVdPolymer`, `AnalyticityLambdaMayerIdentity`,
-`AnalyticityLambdaBasicIdentities`,
-`AnalyticityLambdaMayerPfeEdgeBounds`,
-`AnalyticityLambdaMayerRecurrenceEpsilon`,
-`AnalyticityLambdaEpsilonIff`, ...) re-imported at the top of this
-file, so the earlier import path is preserved while the per-PR
-narrow Moved doc blocks below list the exact destinations. -/
-
-/-! ## Moved: polymerFreeEnergy_Λ basic wrappers
-
-The 16 §18.4 polymerFreeEnergy_Λ / vdPolymerFamilies_sum_Λ / mayer*_Λ
-basic wrappers now live in
-`IsingModel.AmbientLattice.AnalyticityLambdaPolymer`.
-The earlier import path is preserved by re-importing the new child.
--/
-
-
-
-/-! ## Moved: polymerFreeEnergy_Λ sandwich + hasSum wrappers
-
-The 10 §18.4 / §18.5 polymerFreeEnergy_Λ high_temp_sandwich, tanh
-sandwich, hasSum_via_log, and vdPolymerFamilies_sum_Λ sandwich wrappers
-(with ferromagnetic variants) now live in
-`IsingModel.AmbientLattice.AnalyticityLambdaSandwich`.
-The earlier import path is preserved by re-importing the new child.
--/
-
-
-/-! ## Moved: Λ regularity wrappers
-
-The 10 Λ-layer freeEnergyΛ correction + polymerFreeEnergy_Λ
-continuous/differentiable + tanh analyticAt/analyticOnNhd wrappers
-now live in
-`IsingModel.AmbientLattice.AnalyticityLambdaRegularity`.
-The earlier import path is preserved by re-importing the new child.
--/
-
-
-/-! ## Moved: polymerFreeEnergy_Λ bounds wrappers
-
-The 12 Λ-layer polymerFreeEnergy_Λ nonneg / bounds / monotone / eq_zero
-/ tanh sandwich / tanh double bound wrappers now live in
-`IsingModel.AmbientLattice.AnalyticityLambdaPolymerBounds`.
-The earlier import path is preserved by re-importing the new child.
--/
-
-
-/-! ## Moved: mayer wrappers
-
-The 23 §18.6 mayerPartialSum_Λ + mayerExpansionTerm_Λ
-continuous/differentiable/analyticAt/analyticOnNhd wrappers (raw and
-tanh-composed variants) now live in
-`IsingModel.AmbientLattice.AnalyticityLambdaMayer`.
-The earlier import path is preserved by re-importing the new child.
--/
-
-/-! ## Moved: vdPolymerFamilies_sum + log_vdPolymerFamilies_sum wrappers
-
-The 14 §18.5-18.6 vdPolymerFamilies_sum_Λ + log_vdPolymerFamilies_sum_Λ
-continuous / differentiable / analyticAt / hasDerivAt wrappers
-(raw and tanh-composed variants) now live in
-`IsingModel.AmbientLattice.AnalyticityLambdaVdPolymer`.
-The earlier import path is preserved by re-importing the new child.
--/
-
-/-! ## Moved: §18.5 Mayer identity edge-case wrappers
-
-The 19 §18.5 Λ-layer Mayer identity / polymerFreeEnergy =
-mayerPartialSum edge-case wrappers (parameter slices `t = 0`, `β·J =
-0`, `β = 0`, `J = 0`; polymer_free_energy form; mayerPartialSum 0 ≤
-polymerFreeEnergy bounds; no-polymer / trivial / edgeless induced
-graphs) now live in
-`IsingModel.AmbientLattice.AnalyticityLambdaMayerIdentity`. The
-earlier import path is preserved by re-importing the new child.
--/
-
-/-! ## Moved: §18.5 basic identities + bounds + iff wrappers
-
-The 17 §18.5 Λ-layer wrappers covering `at_zero` / `at_one` basic
-identities, tanh iff characterizations, the bound family
-(`le_two_pow`, `le_one_plus_tanh_pow`, `one_le_vdPolymerFamilies_sum_Λ`),
-and generic-`t` bounds + `_eq_one_add` decomposition now live in
-`IsingModel.AmbientLattice.AnalyticityLambdaBasicIdentities`. The
-earlier import path is preserved by re-importing the new child.
--/
-
-/-! ## Moved: §18.5 Mayer expansion + polymerFreeEnergy bound wrappers
-
-The 17 §18.5 Λ-layer wrappers covering Mayer expansion edge-cases
-(`n = 2`, `_two_filter`, `mayerPartialSum at N = 2`,
-`_eq_zero_of_no_polymers`, `_eq_zero_of_edgeFinset_empty`,
-`mayerExpansionTerm_abs_le`), polymerFreeEnergy at_zero / at_one +
-analyticAt + analyticOnNhd_Ici_zero + sandwich_of_nonneg, and
-polymerFreeEnergy tanh-bound + ferromagnetic + hasDerivAt +
-`_eq_log_one_add_eps` now live in
-`IsingModel.AmbientLattice.AnalyticityLambdaMayerPfeEdgeBounds`. The
-earlier import path is preserved by re-importing the new child.
--/
-
-/-! ## Moved: §18.5 Mayer recurrence + ε infrastructure wrappers
-
-The 12 §18.5 Λ-layer wrappers covering Mayer recurrence
-(`mayerPartialSum_Λ_succ`,
-`mayerExpansionTerm_Λ_eq_mayerPartialSum_diff`),
-`polymerFreeEnergy_Λ_hasSum_via_log` / `_hasSum_via_log_eventually`,
-`vdPolymerFamilies_sum_Λ_minus_one_tendsto_zero`, Mayer term sign at
-`n = 1, 2` (`mayerExpansionTerm_Λ_one_nonneg_of_nonneg`,
-`_two_nonpos_of_nonneg`), `vdPolymerFamilies_sum_Λ_minus_one_{at_zero,
-continuous, analyticAt, lt_one_eventually}`, and
-`allPolymers_Λ_eq_empty_of_edgeFinset_empty` now live in
-`IsingModel.AmbientLattice.AnalyticityLambdaMayerRecurrenceEpsilon`.
-The earlier import path is preserved by re-importing the new child.
--/
-
-/-! ## Moved: §18.5 ε(t) positivity-iff + strict-mono wrappers
-
-The 16 §18.5 Λ-layer wrappers covering ε(t) / polymerFreeEnergy
-positivity / zero iff family (`_minus_one_{pos_iff, eq_zero_iff,
-tanh_pos_iff, tanh_eq_zero_iff}`, `polymerFreeEnergy_Λ_tanh_{pos_iff,
-eq_zero_iff}`) and strict-mono / strict-pos under polymers ≠ ∅
-(`_lt_of_lt`, `_strictMonoOn`, `_pos_of_t_pos`, `_gt_one_of_t_pos`,
-`_minus_one_pos_of_t_pos`, `_tanh_pos_of_tanh_pos`,
-`_tanh_gt_one_of_tanh_pos`, `_minus_one_tanh_pos_of_tanh_pos`,
-`_strictMonoOn_Ioi_zero`, both for `polymerFreeEnergy_Λ` and
-`vdPolymerFamilies_sum_Λ`) now live in
-`IsingModel.AmbientLattice.AnalyticityLambdaEpsilonIff`. The earlier
-import path is preserved by re-importing the new child.
--/
-
-
-/-! ## Moved: §18.5 tanh ferromagnetic iff wrappers
-
-The 9 §18.5 Λ-layer wrappers covering
-`polymerFreeEnergy_Λ_tanh_{lt_eps_iff_eps_pos,
-eq_zero_iff_eps_eq_zero, pos_iff_eps_pos, pos_iff, eq_zero_iff,
-lt_pow_sub_one_of_eps_pos, lt_eps_of_eps_pos}_ferro` and
-`vdPolymerFamilies_sum_Λ_tanh_{gt_one_iff, eq_one_iff}_ferro`
-(under `0 ≤ β`, `0 ≤ J`) now live in
-`IsingModel.AmbientLattice.AnalyticityLambdaTanhFerroIff`. The
-earlier import path is preserved by re-importing the new child.
--/
-
-
-/-! ## Moved: §18.5 polymerFreeEnergy sharpening + vdSum sandwich wrappers
-
-The 21 §18.5 Λ-layer wrappers covering polymerFreeEnergy tanh
-sharpening (non-ferromagnetic) + β/J strict-mono, ε(t) nonneg +
-non-tanh polymerFreeEnergy sharpening, and vdSum sandwich/monotone
-+ ε bound + pFE(tanh) bound + `log 2` (covering Λ-direct
-`polymerFreeEnergy_Λ_tanh_*` sharpening, β/J strict-mono under
-`polymers_nonempty`, `vdPolymerFamilies_sum_Λ_minus_one` nonneg
-and pow_at_zero, non-tanh `polymerFreeEnergy_Λ` sharpening,
-`vdPolymerFamilies_sum_Λ` sandwich/monotone/`minus_one_le`, and
-`polymerFreeEnergy_Λ_tanh_{le_eps, le_pow_sub_one, lt_log_two}`)
-now live in
-`IsingModel.AmbientLattice.AnalyticityLambdaPfeSharpening`. The
-earlier import path is preserved by re-importing the new child.
--/
-
-
-/-! ## Moved: §18.6 partitionFunction + freeEnergy regularity wrappers
-
-The 23 §18.6 Λ-layer wrappers covering partitionFunctionΛ regularity
-at `h = 0`, freeEnergyΛ per-direction analyticity, and
-partitionFunction joint + general-h analyticity now live in
-`IsingModel.AmbientLattice.AnalyticityLambdaSection186`. The earlier
-import path is preserved by re-importing the new child.
--/
-
-
-/-! ## Moved: §18.4-§18.6 capstones + Mayer filter-connected wrappers
-
-The 11 Λ-layer wrappers covering §18.4-§18.6 capstones
-(partitionFunctionΛ high_temp_expansion, freeEnergyΛ
-decomposition, freeEnergy = log 2 at β·J = 0,
-mayerPartialSum_one_at_one) and §18.5 Mayer filter-connected /
-ε^n / mayerPartialSum_analyticOnNhd now live in
-`IsingModel.AmbientLattice.AnalyticityLambdaCapstones`. The earlier
-import path is preserved by re-importing the new child.
--/
-
-
 end Ambient
 end IsingModel

IsingModel/AmbientLattice/AnalyticityLambdaBasicIdentities.lean

@@ -2,18 +2,40 @@ import IsingModel.AmbientLattice.Defs.Core
 import IsingModel.ClusterExpansion.StrictPositivity.IffCharacterisations
 
 /-!
-# AmbientLattice/Analyticity basic identities + bounds + iff wrappers
-
-Narrow child module for 17 §18.5 Λ-layer wrappers covering basic
-`at_zero` / `at_one` identities for `vdPolymerFamilies_sum`,
-`mayerPartialSum`, and `mayerExpansionTerm`; tanh iff characterizations
-for `vdPolymerFamilies_sum_Λ` (`tanh_gt_one_iff`, `tanh_eq_one_iff`);
-the bound family
-(`le_two_pow`, `le_one_plus_tanh_pow`, `one_le_vdPolymerFamilies_sum_Λ`);
-and generic-`t` bounds + `_eq_one_add` decomposition
-(`ge_one_of_nonneg`, `le_one_plus_pow_of_nonneg`, `pos_of_nonneg`,
-`eq_one_add`). The theorem names are unchanged from the former
-`Analyticity` declarations.
+# Values, decomposition and elementary bounds of the polymer sum (§18.5)
+
+Statements for an ambient graph `G : SimpleGraph V` and a finite volume `Λ : Finset V`, read
+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, so a
+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_Λ`.
+
+Special values are recorded at literal arguments substituted into the statement: `Ξ 0 = 1`,
+`Ξ 1 = (vdCompatiblePolymerFamilies (inducedGraph G Λ)).card`,
+`mayerPartialSum (inducedGraph G Λ) N 0 = 0` and
+`mayerExpansionTerm (inducedGraph G Λ) n 0 = 0` at a literal activity `0`, and at low order
+`mayerPartialSum … 0 t = 0`, `mayerExpansionTerm … 0 t = 0`, with both
+`mayerPartialSum … 1 t` and `mayerExpansionTerm … 1 t` equal to
+`∑ P ∈ allPolymers (inducedGraph G Λ), t ^ P.card`. The decomposition `Ξ t = 1 + ε t`, which
+isolates the empty family, holds for every real `t` and needs no hypothesis.
+
+At a nonnegative activity, `Ξ t` is strictly positive, at least `1`, and at most
+`(1 + t) ^ E.card`. At the physical activity `Real.tanh (β * J)` under `0 ≤ β * J` the same
+bounds appear as `1 ≤ Ξ (tanh (β * J))`, `Ξ (tanh (β * J)) ≤ (1 + tanh (β * J)) ^ E.card`
+and the cruder `Ξ (tanh (β * J)) ≤ 2 ^ E.card`.
+
+Where `Ξ` sits relative to `1` is settled exactly there, and the two cases are
+complementary: `1 < Ξ (tanh (β * J))` precisely when `0 < Real.tanh (β * J)` and
+`(allPolymers (inducedGraph G Λ)).Nonempty`, and `Ξ (tanh (β * J)) = 1` precisely when
+`Real.tanh (β * J) = 0` or `allPolymers (inducedGraph G Λ) = ∅`.
+
+Every statement takes exactly two instance binders, `DecidableEq V` and
+`Fintype (inducedGraph G Λ).edgeSet`. The Prop-valued hypotheses occurring anywhere in the
+file are exactly `0 ≤ t` and `0 ≤ β * J`; the special values and the `1 + ε t` decomposition
+carry neither.
 -/
 
 namespace IsingModel

IsingModel/AmbientLattice/AnalyticityLambdaCapstones.lean

@@ -3,22 +3,47 @@ import IsingModel.ClusterExpansion.AlternatingCompleteGraph.MayerConnectedFilter
 import IsingModel.ClusterExpansion.StrictPositivity.CycleSeven
 
 /-!
-# AmbientLattice/Analyticity §18.4-§18.6 capstones + Mayer filter-connected wrappers
-
-Narrow child module for 11 Λ-layer wrappers covering:
-
-- §18.4-§18.6 capstones: `partitionFunctionΛ_high_temp_expansion_h_zero_polymer_family`
-  (Z formula), `_closed_evenSubgraphs` (FV (3.45) form),
-  `freeEnergyΛ_eq_polymerFreeEnergy` / `_ferromagnetic` (§18.6 decomposition),
-  `freeEnergyΛ_eq_log_two_at_betaJ_zero`, `mayerPartialSum_Λ_one_at_one`.
-- §18.5 Mayer filter-connected / ε^n / mayerPartialSum_analyticOnNhd:
-  `mayerPartialSum_Λ_analyticOnNhd`,
-  `vdPolymerFamilies_sum_Λ_minus_one_pow`,
-  `mayerExpansionTerm_Λ_filter_connected_{zero, one}`,
-  `mayerExpansionTerm_Λ_two_filter_connected_eq_incompat`.
-
-The theorem names are unchanged from the former `Analyticity`
-declarations.
+# High-temperature expansion and free-energy decomposition on a finite volume (§18.4-§18.6)
+
+Statements for an ambient graph `G : SimpleGraph V` and a finite volume `Λ : Finset V`, at
+the zero field, read on the induced subgraph `inducedGraph G Λ`. The polymer sum
+`∑ Γ ∈ vdCompatiblePolymerFamilies (inducedGraph G Λ), ∏ P ∈ Γ, t ^ P.card` has no
+definition of its own, so the statements that use it — the polymer-sum form of the
+high-temperature closed form, and the power identity for the same sum with its empty family
+removed — carry the summation written out, as does the even-subgraph closed form for its own
+sum over `evenSubgraphs (inducedGraph G Λ)`. The free-energy statements are phrased through
+`freeEnergyΛ`, and through `polymerFreeEnergy` where the decomposition needs it; of the Mayer
+statements, those about the partial sum are phrased through `mayerPartialSum`, while the
+connectedness-filter identities are phrased through `Fintype.piFinset`, `allPolymers` and
+`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`.
+
+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
+`Real.tanh (β * J)`, and again with the polymer sum replaced by
+`∑ X ∈ evenSubgraphs (inducedGraph G Λ), Real.tanh (β * J) ^ X.card`. Dividing by the volume
+turns this into the free-energy decomposition
+`freeEnergyΛ G Λ ⟨J, 0, β⟩ = Real.log 2 + E.card / Fintype.card ↑Λ * Real.log (cosh (β * J))
++ polymerFreeEnergy (inducedGraph G Λ) (tanh (β * J)) / Fintype.card ↑Λ`, stated once under
+`0 ≤ β * J` and once under the ferromagnetic pair `0 ≤ J`, `0 < β`; both also assume
+`Λ.Nonempty`, which is what makes the division by `Fintype.card ↑Λ` meaningful. When
+`β * J = 0` the last two terms vanish and the free energy is exactly `Real.log 2`, again
+under `Λ.Nonempty`.
+
+The remaining statements are about the Mayer series. `mayerPartialSum (inducedGraph G Λ)` is
+`AnalyticOnNhd ℝ` in the activity over `Set.univ`, with no restriction on the activity, and
+at order `1` and activity `1` it equals `(allPolymers (inducedGraph G Λ)).card`. The `n`-th
+power of the polymer sum over `… .erase ∅` expands as a sum over `Fintype.piFinset`
+sequences of nonempty families. Filtering length-`n` polymer sequences by connectedness of
+`polymerSeqIncompatibilityGraph` leaves `∅` at `n = 0`, the whole `Fintype.piFinset` at
+`n = 1`, and at `n = 2` exactly the pairs satisfying `PolymersIncompatible`.
+
+Every statement takes exactly two instance binders, `DecidableEq V` and
+`Fintype (inducedGraph G Λ).edgeSet`. The Prop-valued hypotheses that occur anywhere in the
+file are exactly `0 ≤ β * J`, `β * J = 0`, `0 ≤ J`, `0 < β` and `Λ.Nonempty`; the two
+closed-form expansions and every Mayer statement carry none of them.
 -/
 
 namespace IsingModel