From df9083bc9592ff5b6e7da918279f16ca6caeb3f8 Mon Sep 17 00:00:00 2001 From: phasetr Date: Fri, 17 Jul 2026 01:10:36 +0900 Subject: [PATCH 1/3] chore(refactor): start dead decoration removal cycle Co-Authored-By: Claude Fable 5 From bd67891ed187e6f690da9f151ec839845bd7ad53 Mon Sep 17 00:00:00 2001 From: phasetr Date: Fri, 17 Jul 2026 02:00:04 +0900 Subject: [PATCH 2/3] refactor(pseudomass,ambient): remove 97 dead ref-0 interval/decoration lemmas Pure removal of unreferenced theorems flagged by the tier-2 dead-decl audit (finding H1). All 97 are plain theorems with no attributes and no surviving referrers (78 leaf ref-0 + 16 cascade-dead + 3 unused '_apply' unfold aliases). - PseudoMass/FromParamsBounds/Intervals.lean: whole file dead -> deleted, and its sole import dropped from PseudoMass/FromParamsBounds.lean (21 lemmas). - AmbientLattice/TruncatedFunctions/TwoPoint.lean: 14 truncated2Infinite_* bounds. - AmbientLattice/CorrelationInfinite/Bounds.lean: 13 correlationInfinite_* bounds. - PseudoMass/Ext.lean: 31 pseudoMassExt_*/neg_pseudoMassExt_* lemmas. - PseudoMass/Basic.lean: 15 pseudoMass_* lemmas. - Removed 3 unused unfold aliases: susceptibilityAlongExhaustion_apply, susceptibilityInfinite_apply, spontaneousMagnetization_apply. No mathematical content lost: every KEPT lemma still builds; no survivor proof edits needed. Build green (zero warnings), GKSTest passes, zero sorry. Co-Authored-By: Claude Fable 5 --- .../CorrelationInfinite/Bounds.lean | 120 ------- .../MagnetizationAlongExhaustion.lean | 11 - .../MagnetizationInfiniteSusceptibility.lean | 11 - .../SpontaneousMagnetization.lean | 9 - .../TruncatedFunctions/TwoPoint.lean | 132 ------- IsingModel/PseudoMass/Basic.lean | 140 -------- IsingModel/PseudoMass/Ext.lean | 252 ------------- IsingModel/PseudoMass/FromParamsBounds.lean | 5 +- .../FromParamsBounds/Intervals.lean | 331 ------------------ 9 files changed, 2 insertions(+), 1009 deletions(-) delete mode 100644 IsingModel/PseudoMass/FromParamsBounds/Intervals.lean diff --git a/IsingModel/AmbientLattice/CorrelationInfinite/Bounds.lean b/IsingModel/AmbientLattice/CorrelationInfinite/Bounds.lean index 1d12ff052..c53ab32e1 100644 --- a/IsingModel/AmbientLattice/CorrelationInfinite/Bounds.lean +++ b/IsingModel/AmbientLattice/CorrelationInfinite/Bounds.lean @@ -85,16 +85,6 @@ theorem correlationInfinite_lt_two have h := correlationInfinite_le_one G Λ p A linarith -/-- **`correlationInfinite ∈ Icc (-1) 1`** (unconditional): combines -`abs_correlationInfinite_le_one` lower and upper sides. -/ -theorem correlationInfinite_mem_Icc_neg_one_one - (G : SimpleGraph V) (Λ : Exhaustion V) - [∀ n, Fintype (inducedGraph G (Λ.volume n)).edgeSet] - (p : IsingParams ℝ) (A : Finset V) : - correlationInfinite G Λ p A ∈ Set.Icc (-1 : ℝ) 1 := - ⟨neg_one_le_correlationInfinite G Λ p A, - correlationInfinite_le_one G Λ p A⟩ - /-- **Nonnegativity** (ferromagnetic): `correlationInfinite ≥ 0`. Uses `Λ.exhaust`: pick `N` with `A ⊆ Λ.volume N`; then `correlationAlongExhaustion G Λ p A N ≥ 0` by GKS-I, and this is @@ -112,36 +102,6 @@ theorem correlationInfinite_nonneg exact correlationΛ_nonneg G (Λ.volume N) p hf _ exact hval.trans (le_ciSup (correlationAlongExhaustion_bddAbove G Λ p A) N) -/-- **`correlationInfinite ∈ Icc 0 1`** under ferromagnetic: combines -`correlationInfinite_nonneg` and `correlationInfinite_le_one`. -/ -theorem correlationInfinite_mem_Icc_zero_one - (G : SimpleGraph V) (Λ : Exhaustion V) - [∀ n, Fintype (inducedGraph G (Λ.volume n)).edgeSet] - (p : IsingParams ℝ) (hf : Ferromagnetic p) (A : Finset V) : - correlationInfinite G Λ p A ∈ Set.Icc (0 : ℝ) 1 := - ⟨correlationInfinite_nonneg G Λ p hf A, - correlationInfinite_le_one G Λ p A⟩ - -/-- **`correlationInfinite ∈ Icc 0 2`** under ferromagnetic: combines -`correlationInfinite_nonneg` and `correlationInfinite_le_one ≤ 2`. -/ -theorem correlationInfinite_mem_Icc_zero_two - (G : SimpleGraph V) (Λ : Exhaustion V) - [∀ n, Fintype (inducedGraph G (Λ.volume n)).edgeSet] - (p : IsingParams ℝ) (hf : Ferromagnetic p) (A : Finset V) : - correlationInfinite G Λ p A ∈ Set.Icc (0 : ℝ) 2 := by - have h := correlationInfinite_le_one G Λ p A - refine ⟨correlationInfinite_nonneg G Λ p hf A, ?_⟩ - linarith - -/-- **`correlationInfinite ∈ Ioc 0 1`** when positive under ferromagnetic. -/ -theorem correlationInfinite_mem_Ioc_zero_one_of_pos - (G : SimpleGraph V) (Λ : Exhaustion V) - [∀ n, Fintype (inducedGraph G (Λ.volume n)).edgeSet] - (p : IsingParams ℝ) (_hf : Ferromagnetic p) (A : Finset V) - (hpos : 0 < correlationInfinite G Λ p A) : - correlationInfinite G Λ p A ∈ Set.Ioc (0 : ℝ) 1 := - ⟨hpos, correlationInfinite_le_one G Λ p A⟩ - /-- **`correlationInfinite ∈ Ioo 0 2`** when positive under ferromagnetic. -/ theorem correlationInfinite_mem_Ioo_zero_two_of_pos (G : SimpleGraph V) (Λ : Exhaustion V) @@ -151,85 +111,5 @@ theorem correlationInfinite_mem_Ioo_zero_two_of_pos correlationInfinite G Λ p A ∈ Set.Ioo (0 : ℝ) 2 := ⟨hpos, correlationInfinite_lt_two G Λ p A⟩ -/-- **`correlationInfinite ∈ Ico 0 2`** under ferromagnetic. -/ -theorem correlationInfinite_mem_Ico_zero_two - (G : SimpleGraph V) (Λ : Exhaustion V) - [∀ n, Fintype (inducedGraph G (Λ.volume n)).edgeSet] - (p : IsingParams ℝ) (hf : Ferromagnetic p) (A : Finset V) : - correlationInfinite G Λ p A ∈ Set.Ico (0 : ℝ) 2 := - ⟨correlationInfinite_nonneg G Λ p hf A, - correlationInfinite_lt_two G Λ p A⟩ - -/-- **`correlationInfinite ∈ Iio 2`** (unconditional). -/ -theorem correlationInfinite_mem_Iio_two - (G : SimpleGraph V) (Λ : Exhaustion V) - [∀ n, Fintype (inducedGraph G (Λ.volume n)).edgeSet] - (p : IsingParams ℝ) (A : Finset V) : - correlationInfinite G Λ p A ∈ Set.Iio (2 : ℝ) := - correlationInfinite_lt_two G Λ p A - -/-- **`correlationInfinite ∈ Iic 1`** (unconditional). -/ -theorem correlationInfinite_mem_Iic_one - (G : SimpleGraph V) (Λ : Exhaustion V) - [∀ n, Fintype (inducedGraph G (Λ.volume n)).edgeSet] - (p : IsingParams ℝ) (A : Finset V) : - correlationInfinite G Λ p A ∈ Set.Iic (1 : ℝ) := - correlationInfinite_le_one G Λ p A - -/-- **`correlationInfinite ∈ Ici 0`** under ferromagnetic. -/ -theorem correlationInfinite_mem_Ici_zero - (G : SimpleGraph V) (Λ : Exhaustion V) - [∀ n, Fintype (inducedGraph G (Λ.volume n)).edgeSet] - (p : IsingParams ℝ) (hf : Ferromagnetic p) (A : Finset V) : - correlationInfinite G Λ p A ∈ Set.Ici (0 : ℝ) := - correlationInfinite_nonneg G Λ p hf A - -/-- **`correlationInfinite ∉ Iio 0`** under ferromagnetic. -/ -theorem correlationInfinite_not_mem_Iio_zero - (G : SimpleGraph V) (Λ : Exhaustion V) - [∀ n, Fintype (inducedGraph G (Λ.volume n)).edgeSet] - (p : IsingParams ℝ) (hf : Ferromagnetic p) (A : Finset V) : - correlationInfinite G Λ p A ∉ Set.Iio (0 : ℝ) := - not_lt.mpr (correlationInfinite_nonneg G Λ p hf A) - -/-- **`correlationInfinite ∉ Ioi 1`** (unconditional): direct from -`correlationInfinite_le_one`. -/ -theorem correlationInfinite_not_mem_Ioi_one - (G : SimpleGraph V) (Λ : Exhaustion V) - [∀ n, Fintype (inducedGraph G (Λ.volume n)).edgeSet] - (p : IsingParams ℝ) (A : Finset V) : - correlationInfinite G Λ p A ∉ Set.Ioi (1 : ℝ) := - not_lt.mpr (correlationInfinite_le_one G Λ p A) - -/-- **`0 < correlationInfinite ↔ correlationInfinite ≠ 0`** under -ferromagnetic: standard nonneg → pos iff ne_zero pattern. -/ -theorem correlationInfinite_pos_iff_ne_zero - (G : SimpleGraph V) (Λ : Exhaustion V) - [∀ n, Fintype (inducedGraph G (Λ.volume n)).edgeSet] - (p : IsingParams ℝ) (hf : Ferromagnetic p) (A : Finset V) : - 0 < correlationInfinite G Λ p A ↔ correlationInfinite G Λ p A ≠ 0 := - (correlationInfinite_nonneg G Λ p hf A).lt_iff_ne.trans - ⟨fun h => h.symm, fun h => h.symm⟩ - -/-- **`correlationInfinite ≤ 0 ↔ correlationInfinite = 0`** under -ferromagnetic: combines nonneg with antisymmetry. -/ -theorem correlationInfinite_le_zero_iff_eq_zero - (G : SimpleGraph V) (Λ : Exhaustion V) - [∀ n, Fintype (inducedGraph G (Λ.volume n)).edgeSet] - (p : IsingParams ℝ) (hf : Ferromagnetic p) (A : Finset V) : - correlationInfinite G Λ p A ≤ 0 ↔ correlationInfinite G Λ p A = 0 := by - refine ⟨?_, fun h => le_of_eq h⟩ - intro hle - exact le_antisymm hle (correlationInfinite_nonneg G Λ p hf A) - -/-- **`¬(correlationInfinite < 0)`** under ferromagnetic: direct -from `correlationInfinite_nonneg`. -/ -theorem correlationInfinite_not_lt_zero - (G : SimpleGraph V) (Λ : Exhaustion V) - [∀ n, Fintype (inducedGraph G (Λ.volume n)).edgeSet] - (p : IsingParams ℝ) (hf : Ferromagnetic p) (A : Finset V) : - ¬ (correlationInfinite G Λ p A < 0) := - not_lt.mpr (correlationInfinite_nonneg G Λ p hf A) - end Ambient end IsingModel diff --git a/IsingModel/AmbientLattice/MagnetizationAlongExhaustion.lean b/IsingModel/AmbientLattice/MagnetizationAlongExhaustion.lean index dcc7d9407..d6fa3dafa 100644 --- a/IsingModel/AmbientLattice/MagnetizationAlongExhaustion.lean +++ b/IsingModel/AmbientLattice/MagnetizationAlongExhaustion.lean @@ -129,17 +129,6 @@ noncomputable def susceptibilityAlongExhaustion susceptibilityΛ G (Λ.volume n) p ⟨i, h⟩ else 0 -/-- **Unfolding of `susceptibilityAlongExhaustion`**: by definition the -stagewise value is the dependent `if`-expression over membership. -/ -theorem susceptibilityAlongExhaustion_apply - (G : SimpleGraph V) (Λ : Exhaustion V) - [∀ n, Fintype (inducedGraph G (Λ.volume n)).edgeSet] - (p : IsingParams ℝ) (i : V) (n : ℕ) : - susceptibilityAlongExhaustion G Λ p i n - = if h : i ∈ Λ.volume n then - susceptibilityΛ G (Λ.volume n) p ⟨i, h⟩ - else 0 := rfl - /-- **Unfolding of `susceptibilityAlongExhaustion` when `i ∈ Λ.volume n`**: the stagewise value equals `susceptibilityΛ` at the lifted subtype site. -/ theorem susceptibilityAlongExhaustion_of_mem diff --git a/IsingModel/AmbientLattice/MagnetizationInfiniteSusceptibility.lean b/IsingModel/AmbientLattice/MagnetizationInfiniteSusceptibility.lean index c1dfa4844..0b86ebdfa 100644 --- a/IsingModel/AmbientLattice/MagnetizationInfiniteSusceptibility.lean +++ b/IsingModel/AmbientLattice/MagnetizationInfiniteSusceptibility.lean @@ -54,17 +54,6 @@ theorem susceptibilityInfinite_eq_ciSup susceptibilityInfinite G Λ p i = ⨆ n, susceptibilityAlongExhaustion G Λ p i n := rfl -/-- **Unfolding of `susceptibilityInfinite`**: -`susceptibilityInfinite G Λ p i = ⨆ n, susceptibilityAlongExhaustion G Λ p i n`, -by definition. (Alias of `susceptibilityInfinite_eq_ciSup` for uniformity -with `magnetizationInfinite_apply`.) -/ -theorem susceptibilityInfinite_apply - (G : SimpleGraph V) (Λ : Exhaustion V) - [∀ n, Fintype (inducedGraph G (Λ.volume n)).edgeSet] - (p : IsingParams ℝ) (i : V) : - susceptibilityInfinite G Λ p i - = ⨆ n, susceptibilityAlongExhaustion G Λ p i n := rfl - /-- **Nonnegativity of `susceptibilityInfinite`** under ferromagnetism: `0 ≤ susceptibilityInfinite G Λ p i`. diff --git a/IsingModel/AmbientLattice/SpontaneousMagnetization.lean b/IsingModel/AmbientLattice/SpontaneousMagnetization.lean index 057fef539..04c4536d5 100644 --- a/IsingModel/AmbientLattice/SpontaneousMagnetization.lean +++ b/IsingModel/AmbientLattice/SpontaneousMagnetization.lean @@ -210,15 +210,6 @@ noncomputable def spontaneousMagnetization (J β : ℝ) (i : V) : ℝ := spontaneousCorrelation G Λ J β {i} -/-- **Unfolding of `spontaneousMagnetization`**: -`spontaneousMagnetization G Λ J β i = spontaneousCorrelation G Λ J β {i}`. -/ -theorem spontaneousMagnetization_apply - (G : SimpleGraph V) (Λ : Exhaustion V) - [∀ n, Fintype (inducedGraph G (Λ.volume n)).edgeSet] - (J β : ℝ) (i : V) : - spontaneousMagnetization G Λ J β i = spontaneousCorrelation G Λ J β {i} := - rfl - /-- **Agreement at singletons**: `spontaneousCorrelation` on `{i}` equals `spontaneousMagnetization`. Holds by definition. -/ theorem spontaneousCorrelation_singleton_eq_spontaneousMagnetization diff --git a/IsingModel/AmbientLattice/TruncatedFunctions/TwoPoint.lean b/IsingModel/AmbientLattice/TruncatedFunctions/TwoPoint.lean index f16a99318..2b679b023 100644 --- a/IsingModel/AmbientLattice/TruncatedFunctions/TwoPoint.lean +++ b/IsingModel/AmbientLattice/TruncatedFunctions/TwoPoint.lean @@ -245,138 +245,6 @@ theorem truncated2Infinite_sq_le_one pow_le_pow_left₀ (abs_nonneg _) h 2 simpa [sq_abs] using this -/-- **`truncated2Infinite < 2`** for ferromagnetic `p`: direct from -`truncated2Infinite ≤ 1 < 2`. Useful for `Ioo 0 2` membership when -combining with strict positivity. -/ -theorem truncated2Infinite_lt_two - (G : SimpleGraph V) (Λ : Exhaustion V) - [∀ n, Fintype (inducedGraph G (Λ.volume n)).edgeSet] - (p : IsingParams ℝ) (hf : Ferromagnetic p) (i j : V) : - truncated2Infinite G Λ p i j < 2 := by - have h := truncated2Infinite_le_one G Λ p hf i j - linarith - -/-- **`truncated2Infinite ∈ Ioo 0 2`** when `0 < truncated2`** under -ferromagnetic: combines `_lt_two` (PR #1728 candidate) with the -strict positivity hypothesis. -/ -theorem truncated2Infinite_mem_Ioo_zero_two_of_pos - (G : SimpleGraph V) (Λ : Exhaustion V) - [∀ n, Fintype (inducedGraph G (Λ.volume n)).edgeSet] - (p : IsingParams ℝ) (hf : Ferromagnetic p) (i j : V) - (hpos : 0 < truncated2Infinite G Λ p i j) : - truncated2Infinite G Λ p i j ∈ Set.Ioo (0 : ℝ) 2 := - ⟨hpos, truncated2Infinite_lt_two G Λ p hf i j⟩ - -/-- **`truncated2Infinite ∈ Icc 0 1`** for ferromagnetic `p`: combines -`truncated2Infinite_nonneg` and `truncated2Infinite_le_one`. -/ -theorem truncated2Infinite_mem_Icc_zero_one - (G : SimpleGraph V) (Λ : Exhaustion V) - [∀ n, Fintype (inducedGraph G (Λ.volume n)).edgeSet] - (p : IsingParams ℝ) (hf : Ferromagnetic p) (i j : V) : - truncated2Infinite G Λ p i j ∈ Set.Icc (0 : ℝ) 1 := - ⟨truncated2Infinite_nonneg G Λ p hf i j, - truncated2Infinite_le_one G Λ p hf i j⟩ - -/-- **`truncated2Infinite ∈ Ioc 0 1`** when `0 < truncated2` under -ferromagnetic: strict positivity + ≤ 1. -/ -theorem truncated2Infinite_mem_Ioc_zero_one_of_pos - (G : SimpleGraph V) (Λ : Exhaustion V) - [∀ n, Fintype (inducedGraph G (Λ.volume n)).edgeSet] - (p : IsingParams ℝ) (hf : Ferromagnetic p) (i j : V) - (hpos : 0 < truncated2Infinite G Λ p i j) : - truncated2Infinite G Λ p i j ∈ Set.Ioc (0 : ℝ) 1 := - ⟨hpos, truncated2Infinite_le_one G Λ p hf i j⟩ - -/-- **`truncated2Infinite ∈ Ico 0 2`** under ferromagnetic. -/ -theorem truncated2Infinite_mem_Ico_zero_two - (G : SimpleGraph V) (Λ : Exhaustion V) - [∀ n, Fintype (inducedGraph G (Λ.volume n)).edgeSet] - (p : IsingParams ℝ) (hf : Ferromagnetic p) (i j : V) : - truncated2Infinite G Λ p i j ∈ Set.Ico (0 : ℝ) 2 := - ⟨truncated2Infinite_nonneg G Λ p hf i j, - truncated2Infinite_lt_two G Λ p hf i j⟩ - -/-- **`truncated2Infinite ∈ Iio 2`** under ferromagnetic. -/ -theorem truncated2Infinite_mem_Iio_two - (G : SimpleGraph V) (Λ : Exhaustion V) - [∀ n, Fintype (inducedGraph G (Λ.volume n)).edgeSet] - (p : IsingParams ℝ) (hf : Ferromagnetic p) (i j : V) : - truncated2Infinite G Λ p i j ∈ Set.Iio (2 : ℝ) := - truncated2Infinite_lt_two G Λ p hf i j - -/-- **`truncated2Infinite ∈ Iic 1`** under ferromagnetic. -/ -theorem truncated2Infinite_mem_Iic_one - (G : SimpleGraph V) (Λ : Exhaustion V) - [∀ n, Fintype (inducedGraph G (Λ.volume n)).edgeSet] - (p : IsingParams ℝ) (hf : Ferromagnetic p) (i j : V) : - truncated2Infinite G Λ p i j ∈ Set.Iic (1 : ℝ) := - truncated2Infinite_le_one G Λ p hf i j - -/-- **`truncated2Infinite ∈ Ici 0`** under ferromagnetic. -/ -theorem truncated2Infinite_mem_Ici_zero - (G : SimpleGraph V) (Λ : Exhaustion V) - [∀ n, Fintype (inducedGraph G (Λ.volume n)).edgeSet] - (p : IsingParams ℝ) (hf : Ferromagnetic p) (i j : V) : - truncated2Infinite G Λ p i j ∈ Set.Ici (0 : ℝ) := - truncated2Infinite_nonneg G Λ p hf i j - -/-- **`truncated2Infinite ∉ Iio 0`** under ferromagnetic. -/ -theorem truncated2Infinite_not_mem_Iio_zero - (G : SimpleGraph V) (Λ : Exhaustion V) - [∀ n, Fintype (inducedGraph G (Λ.volume n)).edgeSet] - (p : IsingParams ℝ) (hf : Ferromagnetic p) (i j : V) : - truncated2Infinite G Λ p i j ∉ Set.Iio (0 : ℝ) := - not_lt.mpr (truncated2Infinite_nonneg G Λ p hf i j) - -/-- **`truncated2Infinite ∉ Ioi 1`** under ferromagnetic. -/ -theorem truncated2Infinite_not_mem_Ioi_one - (G : SimpleGraph V) (Λ : Exhaustion V) - [∀ n, Fintype (inducedGraph G (Λ.volume n)).edgeSet] - (p : IsingParams ℝ) (hf : Ferromagnetic p) (i j : V) : - truncated2Infinite G Λ p i j ∉ Set.Ioi (1 : ℝ) := - not_lt.mpr (truncated2Infinite_le_one G Λ p hf i j) - -/-- **`truncated2Infinite ∉ Ioi 2`** under ferromagnetic: stronger than -`_lt_two`. -/ -theorem truncated2Infinite_not_mem_Ioi_two - (G : SimpleGraph V) (Λ : Exhaustion V) - [∀ n, Fintype (inducedGraph G (Λ.volume n)).edgeSet] - (p : IsingParams ℝ) (hf : Ferromagnetic p) (i j : V) : - truncated2Infinite G Λ p i j ∉ Set.Ioi (2 : ℝ) := by - intro h_lt - rw [Set.mem_Ioi] at h_lt - have h := truncated2Infinite_le_one G Λ p hf i j - linarith - -/-- **`0 < truncated2Infinite ↔ truncated2Infinite ≠ 0`** under -ferromagnetic: standard nonneg → pos iff ne_zero pattern. -/ -theorem truncated2Infinite_pos_iff_ne_zero - (G : SimpleGraph V) (Λ : Exhaustion V) - [∀ n, Fintype (inducedGraph G (Λ.volume n)).edgeSet] - (p : IsingParams ℝ) (hf : Ferromagnetic p) (i j : V) : - 0 < truncated2Infinite G Λ p i j ↔ truncated2Infinite G Λ p i j ≠ 0 := - (truncated2Infinite_nonneg G Λ p hf i j).lt_iff_ne.trans - ⟨fun h => h.symm, fun h => h.symm⟩ - -/-- **`truncated2Infinite ≤ 0 ↔ truncated2Infinite = 0`** under -ferromagnetic: combines nonneg with antisymmetry. -/ -theorem truncated2Infinite_le_zero_iff_eq_zero - (G : SimpleGraph V) (Λ : Exhaustion V) - [∀ n, Fintype (inducedGraph G (Λ.volume n)).edgeSet] - (p : IsingParams ℝ) (hf : Ferromagnetic p) (i j : V) : - truncated2Infinite G Λ p i j ≤ 0 ↔ truncated2Infinite G Λ p i j = 0 := by - refine ⟨?_, fun h => le_of_eq h⟩ - intro hle - exact le_antisymm hle (truncated2Infinite_nonneg G Λ p hf i j) - -/-- **`¬(truncated2Infinite < 0)`** under ferromagnetic. -/ -theorem truncated2Infinite_not_lt_zero - (G : SimpleGraph V) (Λ : Exhaustion V) - [∀ n, Fintype (inducedGraph G (Λ.volume n)).edgeSet] - (p : IsingParams ℝ) (hf : Ferromagnetic p) (i j : V) : - ¬ (truncated2Infinite G Λ p i j < 0) := - not_lt.mpr (truncated2Infinite_nonneg G Λ p hf i j) - /-- **Exhaustion-independence of `truncated2Infinite`**: the value does not depend on the choice of exhaustion. Follows from `correlationInfinite_indep_exhaustion` applied to each of the three diff --git a/IsingModel/PseudoMass/Basic.lean b/IsingModel/PseudoMass/Basic.lean index c6288e791..00cb202dc 100644 --- a/IsingModel/PseudoMass/Basic.lean +++ b/IsingModel/PseudoMass/Basic.lean @@ -75,18 +75,6 @@ theorem pseudoMass_le_log_two_div {α : ℕ} (hα : 1 ≤ α) {r : ℝ} (hr : 0 rw [le_div_iff₀ hr] linarith -/-- **`pseudoMass(c) · r ≤ log(2/c)`**: multiplied form of -`pseudoMass_le_log_two_div`, useful when `r` appears as a factor -(e.g., `pm·d(x,z)` decay rates). Direct from the divided form -multiplied through by `r > 0`. -/ -theorem pseudoMass_mul_r_le_log_two_div {α : ℕ} (hα : 1 ≤ α) {r : ℝ} - (hr : 0 < r) {c : ℝ} (hc : c ∈ Ioo 0 2) : - pseudoMass hα hr hc * r ≤ Real.log (2 / c) := by - have h := pseudoMass_le_log_two_div hα hr hc - rw [le_div_iff₀ hr] at h - exact h - - /-- Characterisation of the pseudo-mass: `pseudoMass = t ↔ pseudoMassG α r t = c` for `t ≥ 0`. -/ theorem pseudoMass_eq_iff {α : ℕ} (hα : 1 ≤ α) {r : ℝ} (hr : 0 < r) {c : ℝ} @@ -312,44 +300,6 @@ theorem pseudoMass_lt_log_two_div {α : ℕ} (hα : 1 ≤ α) {r : ℝ} (hr : 0 rw [lt_div_iff₀ hr] linarith -/-- **`pseudoMass(c) · r < log(2/c)`**: strict multiplied form of -`pseudoMass_lt_log_two_div`. -/ -theorem pseudoMass_mul_r_lt_log_two_div {α : ℕ} (hα : 1 ≤ α) {r : ℝ} - (hr : 0 < r) {c : ℝ} (hc : c ∈ Ioo 0 2) : - pseudoMass hα hr hc * r < Real.log (2 / c) := by - have h := pseudoMass_lt_log_two_div hα hr hc - rw [lt_div_iff₀ hr] at h - exact h - -/-- **`pseudoMass(c) ∈ Ioo 0 (log(2/c)/r)`**: bundles -`pseudoMass_pos` and `pseudoMass_lt_log_two_div` into one Ioo -membership statement. -/ -theorem pseudoMass_mem_Ioo_zero_log_two_div {α : ℕ} (hα : 1 ≤ α) {r : ℝ} - (hr : 0 < r) {c : ℝ} (hc : c ∈ Ioo 0 2) : - pseudoMass hα hr hc ∈ Set.Ioo (0 : ℝ) (Real.log (2 / c) / r) := - ⟨pseudoMass_pos hα hr hc, - pseudoMass_lt_log_two_div hα hr hc⟩ - -/-- **`pseudoMass(c) ∈ Ioo 0 ((2-c)/(c·r))`**: bundle of `pos` and -strict sharper `(2-c)/(c·r)` upper bound. -/ -theorem pseudoMass_mem_Ioo_zero_two_sub_div {α : ℕ} (hα : 1 ≤ α) {r : ℝ} - (hr : 0 < r) {c : ℝ} (hc : c ∈ Ioo 0 2) : - pseudoMass hα hr hc ∈ Set.Ioo (0 : ℝ) ((2 - c) / (c * r)) := - ⟨pseudoMass_pos hα hr hc, - pseudoMass_lt_two_sub_div_mul_r hα hr hc⟩ - -/-- **`pseudoMass(c) ∈ Iio (log(2/c)/r)`**: trivial via `_lt_log_two_div`. -/ -theorem pseudoMass_mem_Iio_log_two_div {α : ℕ} (hα : 1 ≤ α) {r : ℝ} - (hr : 0 < r) {c : ℝ} (hc : c ∈ Ioo 0 2) : - pseudoMass hα hr hc ∈ Set.Iio (Real.log (2 / c) / r) := - pseudoMass_lt_log_two_div hα hr hc - -/-- **`pseudoMass(c) ∈ Iio ((2-c)/(c·r))`**: trivial via `_lt_two_sub_div_mul_r`. -/ -theorem pseudoMass_mem_Iio_two_sub_div {α : ℕ} (hα : 1 ≤ α) {r : ℝ} - (hr : 0 < r) {c : ℝ} (hc : c ∈ Ioo 0 2) : - pseudoMass hα hr hc ∈ Set.Iio ((2 - c) / (c * r)) := - pseudoMass_lt_two_sub_div_mul_r hα hr hc - /-- The pseudo-mass is strictly decreasing in `c`: larger correlation value means smaller pseudo-mass (slower decay). -/ theorem pseudoMass_strictAnti {α : ℕ} (hα : 1 ≤ α) {r : ℝ} (hr : 0 < r) @@ -374,33 +324,6 @@ theorem pseudoMass_strictAnti {α : ℕ} (hα : 1 ≤ α) {r : ℝ} (hr : 0 < r) rw [heq, h₂] at h₁ linarith -/-- **`pseudoMass(c) ≠ 0`** for `c ∈ Ioo 0 2`: direct from -`pseudoMass_pos`. -/ -theorem pseudoMass_ne_zero {α : ℕ} (hα : 1 ≤ α) {r : ℝ} (hr : 0 < r) {c : ℝ} - (hc : c ∈ Ioo 0 2) : - pseudoMass hα hr hc ≠ 0 := - (pseudoMass_pos hα hr hc).ne' - -/-- **`pseudoMass(c) ∈ Set.Ioi 0`** for `c ∈ Ioo 0 2`: direct from -`pseudoMass_pos`. -/ -theorem pseudoMass_mem_Ioi_zero {α : ℕ} (hα : 1 ≤ α) {r : ℝ} (hr : 0 < r) {c : ℝ} - (hc : c ∈ Ioo 0 2) : - pseudoMass hα hr hc ∈ Set.Ioi (0 : ℝ) := - pseudoMass_pos hα hr hc - -/-- **`pseudoMass(c) ∈ Set.Ici 0`** for `c ∈ Ioo 0 2`: direct from -`pseudoMass_nonneg`. -/ -theorem pseudoMass_mem_Ici_zero {α : ℕ} (hα : 1 ≤ α) {r : ℝ} (hr : 0 < r) {c : ℝ} - (hc : c ∈ Ioo 0 2) : - pseudoMass hα hr hc ∈ Set.Ici (0 : ℝ) := - pseudoMass_nonneg hα hr hc - -/-- **`pseudoMass(c) ∉ Set.Iio 0`** for `c ∈ Ioo 0 2`: direct from `pos`. -/ -theorem pseudoMass_not_mem_Iio_zero {α : ℕ} (hα : 1 ≤ α) {r : ℝ} (hr : 0 < r) - {c : ℝ} (hc : c ∈ Ioo 0 2) : - pseudoMass hα hr hc ∉ Set.Iio (0 : ℝ) := - not_lt.mpr (pseudoMass_nonneg hα hr hc) - /-- **Implicit definition: `pseudoMass(c) ≤ t ↔ pseudoMassG α r t ≤ c`** for `t ≥ 0` and `c ∈ Ioo 0 2`: characterizes pseudoMass(c) as the unique threshold by the anti-monotone defining equation `g(pseudoMass(c)) = c`. -/ @@ -415,18 +338,6 @@ theorem pseudoMass_le_iff_pseudoMassG_le {α : ℕ} (hα : 1 ≤ α) {r : ℝ} rw [hspec] at hG_iff exact hG_iff.symm -/-- **Implicit definition strict version**: `pseudoMass(c) < t ↔ pseudoMassG α r t < c`. -/ -theorem pseudoMass_lt_iff_pseudoMassG_lt {α : ℕ} (hα : 1 ≤ α) {r : ℝ} - (hr : 0 < r) {c : ℝ} (hc : c ∈ Ioo 0 2) {t : ℝ} (ht : 0 ≤ t) : - pseudoMass hα hr hc < t ↔ pseudoMassG α r t < c := by - have hspec : pseudoMassG α r (pseudoMass hα hr hc) = c := pseudoMass_spec hα hr hc - have hpm_nn : 0 ≤ pseudoMass hα hr hc := pseudoMass_nonneg hα hr hc - have hG_iff : pseudoMassG α r t < pseudoMassG α r (pseudoMass hα hr hc) ↔ - pseudoMass hα hr hc < t := - pseudoMassG_lt_iff hα hr hpm_nn ht - rw [hspec] at hG_iff - exact hG_iff.symm - /-- **Implicit definition: `t ≤ pseudoMass(c) ↔ c ≤ pseudoMassG α r t`** (reverse). -/ theorem pseudoMass_ge_iff_pseudoMassG_ge {α : ℕ} (hα : 1 ≤ α) {r : ℝ} (hr : 0 < r) {c : ℝ} (hc : c ∈ Ioo 0 2) {t : ℝ} (ht : 0 ≤ t) : @@ -439,18 +350,6 @@ theorem pseudoMass_ge_iff_pseudoMassG_ge {α : ℕ} (hα : 1 ≤ α) {r : ℝ} rw [hspec] at hG_iff exact hG_iff.symm -/-- **Implicit definition strict reverse**: `t < pseudoMass(c) ↔ c < pseudoMassG α r t`. -/ -theorem pseudoMass_gt_iff_pseudoMassG_gt {α : ℕ} (hα : 1 ≤ α) {r : ℝ} - (hr : 0 < r) {c : ℝ} (hc : c ∈ Ioo 0 2) {t : ℝ} (ht : 0 ≤ t) : - t < pseudoMass hα hr hc ↔ c < pseudoMassG α r t := by - have hspec : pseudoMassG α r (pseudoMass hα hr hc) = c := pseudoMass_spec hα hr hc - have hpm_nn : 0 ≤ pseudoMass hα hr hc := pseudoMass_nonneg hα hr hc - have hG_iff : pseudoMassG α r (pseudoMass hα hr hc) < pseudoMassG α r t ↔ - t < pseudoMass hα hr hc := - pseudoMassG_lt_iff hα hr ht hpm_nn - rw [hspec] at hG_iff - exact hG_iff.symm - /-- **`pseudoMass` is antitone (non-strict)**: corollary of `pseudoMass_strictAnti` weakened to `≤`. Useful when the strict inequality is unnecessarily strong (e.g., bound chains). -/ @@ -462,43 +361,4 @@ theorem pseudoMass_antitone {α : ℕ} (hα : 1 ≤ α) {r : ℝ} (hr : 0 < r) · subst heq exact le_refl _ -/-- **`pseudoMass(c₂) < pseudoMass(c₁) ↔ c₁ < c₂`**: iff form of -`pseudoMass_strictAnti`. -/ -theorem pseudoMass_lt_iff {α : ℕ} (hα : 1 ≤ α) {r : ℝ} (hr : 0 < r) - {c₁ c₂ : ℝ} (hc₁ : c₁ ∈ Ioo 0 2) (hc₂ : c₂ ∈ Ioo 0 2) : - pseudoMass hα hr hc₂ < pseudoMass hα hr hc₁ ↔ c₁ < c₂ := by - refine ⟨?_, fun h => pseudoMass_strictAnti hα hr hc₁ hc₂ h⟩ - intro hlt - by_contra h_neg - have h_neg' : c₂ ≤ c₁ := not_lt.mp h_neg - have := pseudoMass_antitone hα hr hc₂ hc₁ h_neg' - linarith - -/-- **`pseudoMass(c₂) ≤ pseudoMass(c₁) ↔ c₁ ≤ c₂`**: iff form of -`pseudoMass_antitone`. -/ -theorem pseudoMass_le_iff {α : ℕ} (hα : 1 ≤ α) {r : ℝ} (hr : 0 < r) - {c₁ c₂ : ℝ} (hc₁ : c₁ ∈ Ioo 0 2) (hc₂ : c₂ ∈ Ioo 0 2) : - pseudoMass hα hr hc₂ ≤ pseudoMass hα hr hc₁ ↔ c₁ ≤ c₂ := by - refine ⟨?_, fun h => pseudoMass_antitone hα hr hc₁ hc₂ h⟩ - intro hle - by_contra h_neg - have h_neg' : c₂ < c₁ := not_le.mp h_neg - have := pseudoMass_strictAnti hα hr hc₂ hc₁ h_neg' - linarith - -/-- **`pseudoMass(c₂) = pseudoMass(c₁) ↔ c₁ = c₂`**: equality iff -via antisymmetry. -/ -theorem pseudoMass_eq_iff_eq {α : ℕ} (hα : 1 ≤ α) {r : ℝ} (hr : 0 < r) - {c₁ c₂ : ℝ} (hc₁ : c₁ ∈ Ioo 0 2) (hc₂ : c₂ ∈ Ioo 0 2) : - pseudoMass hα hr hc₂ = pseudoMass hα hr hc₁ ↔ c₁ = c₂ := by - refine ⟨?_, ?_⟩ - · intro heq - have h1 := (pseudoMass_le_iff hα hr hc₁ hc₂).mp heq.le - have h2 := (pseudoMass_le_iff hα hr hc₂ hc₁).mp heq.ge - linarith - · intro heq_c - subst heq_c - rfl - - end IsingModel diff --git a/IsingModel/PseudoMass/Ext.lean b/IsingModel/PseudoMass/Ext.lean index 9ab4fb8fb..33308cfb4 100644 --- a/IsingModel/PseudoMass/Ext.lean +++ b/IsingModel/PseudoMass/Ext.lean @@ -66,78 +66,6 @@ theorem pseudoMassExt_pos_of_mem {α : ℕ} (hα : 1 ≤ α) {r : ℝ} (hr : 0 < rw [pseudoMassExt_of_mem hα hr hc] exact pseudoMass_pos hα hr hc -/-- **`pseudoMassExt c ≠ 0`** for `c ∈ Ioo 0 2`. -/ -theorem pseudoMassExt_ne_zero_of_mem {α : ℕ} (hα : 1 ≤ α) {r : ℝ} (hr : 0 < r) - {c : ℝ} (hc : c ∈ Set.Ioo 0 2) : - pseudoMassExt hα hr c ≠ 0 := - (pseudoMassExt_pos_of_mem hα hr hc).ne' - -/-- **`pseudoMassExt c ∈ Set.Ici 0`** (always): direct from -`pseudoMassExt_nonneg`. -/ -theorem pseudoMassExt_mem_Ici_zero {α : ℕ} (hα : 1 ≤ α) {r : ℝ} (hr : 0 < r) - (c : ℝ) : - pseudoMassExt hα hr c ∈ Set.Ici (0 : ℝ) := - pseudoMassExt_nonneg hα hr c - -/-- **`pseudoMassExt c ∈ Set.Ioi 0`** for `c ∈ Ioo 0 2`. -/ -theorem pseudoMassExt_mem_Ioi_zero_of_mem {α : ℕ} (hα : 1 ≤ α) {r : ℝ} - (hr : 0 < r) {c : ℝ} (hc : c ∈ Set.Ioo 0 2) : - pseudoMassExt hα hr c ∈ Set.Ioi (0 : ℝ) := - pseudoMassExt_pos_of_mem hα hr hc - - -/-- **`pseudoMassExt c ∈ Set.Ioo 0 (log(2/c)/r)`** for `c ∈ Ioo 0 2`: -combine pos with strict log upper bound. -/ -theorem pseudoMassExt_mem_Ioo_zero_log_two_div {α : ℕ} (hα : 1 ≤ α) {r : ℝ} - (hr : 0 < r) {c : ℝ} (hc : c ∈ Set.Ioo 0 2) : - pseudoMassExt hα hr c ∈ Set.Ioo (0 : ℝ) (Real.log (2 / c) / r) := by - rw [pseudoMassExt_of_mem hα hr hc] - exact pseudoMass_mem_Ioo_zero_log_two_div hα hr hc - -/-- **`pseudoMassExt c ∈ Set.Ioo 0 ((2-c)/(c·r))`** for `c ∈ Ioo 0 2`. -/ -theorem pseudoMassExt_mem_Ioo_zero_two_sub_div {α : ℕ} (hα : 1 ≤ α) {r : ℝ} - (hr : 0 < r) {c : ℝ} (hc : c ∈ Set.Ioo 0 2) : - pseudoMassExt hα hr c ∈ Set.Ioo (0 : ℝ) ((2 - c) / (c * r)) := by - rw [pseudoMassExt_of_mem hα hr hc] - exact pseudoMass_mem_Ioo_zero_two_sub_div hα hr hc - -/-- **`pseudoMassExt c ∈ Set.Iio (log(2/c)/r)`** for `c ∈ Ioo 0 2`. -/ -theorem pseudoMassExt_mem_Iio_log_two_div {α : ℕ} (hα : 1 ≤ α) {r : ℝ} - (hr : 0 < r) {c : ℝ} (hc : c ∈ Set.Ioo 0 2) : - pseudoMassExt hα hr c ∈ Set.Iio (Real.log (2 / c) / r) := by - rw [pseudoMassExt_of_mem hα hr hc] - exact pseudoMass_mem_Iio_log_two_div hα hr hc - -/-- **`pseudoMassExt c ∈ Set.Iio ((2-c)/(c·r))`** for `c ∈ Ioo 0 2`. -/ -theorem pseudoMassExt_mem_Iio_two_sub_div {α : ℕ} (hα : 1 ≤ α) {r : ℝ} - (hr : 0 < r) {c : ℝ} (hc : c ∈ Set.Ioo 0 2) : - pseudoMassExt hα hr c ∈ Set.Iio ((2 - c) / (c * r)) := by - rw [pseudoMassExt_of_mem hα hr hc] - exact pseudoMass_mem_Iio_two_sub_div hα hr hc - -/-- **`0 < pseudoMassExt c ↔ pseudoMassExt c ≠ 0`**: standard -nonneg → pos iff ne_zero pattern (`pseudoMassExt_nonneg`). -/ -theorem pseudoMassExt_pos_iff_ne_zero {α : ℕ} (hα : 1 ≤ α) {r : ℝ} - (hr : 0 < r) (c : ℝ) : - 0 < pseudoMassExt hα hr c ↔ pseudoMassExt hα hr c ≠ 0 := - (pseudoMassExt_nonneg hα hr c).lt_iff_ne.trans - ⟨fun h => h.symm, fun h => h.symm⟩ - -/-- **`¬(pseudoMassExt c < 0)`**: trivial via nonneg. -/ -theorem pseudoMassExt_not_lt_zero {α : ℕ} (hα : 1 ≤ α) {r : ℝ} - (hr : 0 < r) (c : ℝ) : - ¬ (pseudoMassExt hα hr c < 0) := - not_lt.mpr (pseudoMassExt_nonneg hα hr c) - -/-- **`pseudoMassExt c ≤ 0 ↔ pseudoMassExt c = 0`**: trivial via -nonneg + antisymmetry. -/ -theorem pseudoMassExt_le_zero_iff_eq_zero {α : ℕ} (hα : 1 ≤ α) {r : ℝ} - (hr : 0 < r) (c : ℝ) : - pseudoMassExt hα hr c ≤ 0 ↔ pseudoMassExt hα hr c = 0 := by - refine ⟨?_, fun h => le_of_eq h⟩ - intro hle - exact le_antisymm hle (pseudoMassExt_nonneg hα hr c) - /-- **`pseudoMassExt` `ContinuousAt c₀ ∈ Ioo 0 2`**: re-statement of `pseudoMass_continuousAt` using the named definition. -/ theorem pseudoMassExt_continuousAt {α : ℕ} (hα : 1 ≤ α) {r : ℝ} (hr : 0 < r) @@ -163,11 +91,6 @@ theorem pseudoMassExt_differentiableAt {α : ℕ} (hα : 1 ≤ α) {r : ℝ} (hr DifferentiableAt ℝ (pseudoMassExt hα hr) c₀ := pseudoMass_differentiableAt hα hr hc₀ -/-- **`pseudoMassExt` `DifferentiableOn (Ioo 0 2)`**. -/ -theorem pseudoMassExt_differentiableOn {α : ℕ} (hα : 1 ≤ α) {r : ℝ} (hr : 0 < r) : - DifferentiableOn ℝ (pseudoMassExt hα hr) (Set.Ioo 0 2) := - pseudoMass_differentiableOn hα hr - /-- **`pseudoMassExt` strict anti on `Ioo 0 2`**: lifted from `pseudoMass_strictAnti`. -/ theorem pseudoMassExt_strictAntiOn {α : ℕ} (hα : 1 ≤ α) {r : ℝ} (hr : 0 < r) : @@ -182,101 +105,6 @@ theorem pseudoMassExt_antitoneOn {α : ℕ} (hα : 1 ≤ α) {r : ℝ} (hr : 0 < AntitoneOn (pseudoMassExt hα hr) (Set.Ioo 0 2) := (pseudoMassExt_strictAntiOn hα hr).antitoneOn -/-- **`-pseudoMassExt` is `StrictMonoOn (Ioo 0 2)`**: dual of -`pseudoMassExt_strictAntiOn`. -/ -theorem neg_pseudoMassExt_strictMonoOn {α : ℕ} (hα : 1 ≤ α) {r : ℝ} (hr : 0 < r) : - StrictMonoOn (fun c => -pseudoMassExt hα hr c) (Set.Ioo 0 2) := by - intro c₁ hc₁ c₂ hc₂ h - have hgt : pseudoMassExt hα hr c₂ < pseudoMassExt hα hr c₁ := - pseudoMassExt_strictAntiOn hα hr hc₁ hc₂ h - linarith - -/-- **`-pseudoMassExt` is `MonotoneOn (Ioo 0 2)`**: non-strict. -/ -theorem neg_pseudoMassExt_monotoneOn {α : ℕ} (hα : 1 ≤ α) {r : ℝ} (hr : 0 < r) : - MonotoneOn (fun c => -pseudoMassExt hα hr c) (Set.Ioo 0 2) := - (neg_pseudoMassExt_strictMonoOn hα hr).monotoneOn - - -/-- **`pseudoMassExt(c₂) < pseudoMassExt(c₁) ↔ c₁ < c₂`** for both -in `Ioo 0 2`: iff form of `pseudoMassExt_strictAntiOn`. -/ -theorem pseudoMassExt_lt_iff {α : ℕ} (hα : 1 ≤ α) {r : ℝ} (hr : 0 < r) - {c₁ c₂ : ℝ} (hc₁ : c₁ ∈ Set.Ioo 0 2) (hc₂ : c₂ ∈ Set.Ioo 0 2) : - pseudoMassExt hα hr c₂ < pseudoMassExt hα hr c₁ ↔ c₁ < c₂ := by - rw [pseudoMassExt_of_mem hα hr hc₁, pseudoMassExt_of_mem hα hr hc₂] - exact pseudoMass_lt_iff hα hr hc₁ hc₂ - -/-- **`pseudoMassExt(c₂) ≤ pseudoMassExt(c₁) ↔ c₁ ≤ c₂`** for both -in `Ioo 0 2`. -/ -theorem pseudoMassExt_le_iff {α : ℕ} (hα : 1 ≤ α) {r : ℝ} (hr : 0 < r) - {c₁ c₂ : ℝ} (hc₁ : c₁ ∈ Set.Ioo 0 2) (hc₂ : c₂ ∈ Set.Ioo 0 2) : - pseudoMassExt hα hr c₂ ≤ pseudoMassExt hα hr c₁ ↔ c₁ ≤ c₂ := by - rw [pseudoMassExt_of_mem hα hr hc₁, pseudoMassExt_of_mem hα hr hc₂] - exact pseudoMass_le_iff hα hr hc₁ hc₂ - -/-- **`pseudoMassExt(c₂) = pseudoMassExt(c₁) ↔ c₁ = c₂`** for both -in `Ioo 0 2`. -/ -theorem pseudoMassExt_eq_iff_of_mem {α : ℕ} (hα : 1 ≤ α) {r : ℝ} (hr : 0 < r) - {c₁ c₂ : ℝ} (hc₁ : c₁ ∈ Set.Ioo 0 2) (hc₂ : c₂ ∈ Set.Ioo 0 2) : - pseudoMassExt hα hr c₂ = pseudoMassExt hα hr c₁ ↔ c₁ = c₂ := by - rw [pseudoMassExt_of_mem hα hr hc₁, pseudoMassExt_of_mem hα hr hc₂] - exact pseudoMass_eq_iff_eq hα hr hc₁ hc₂ - -/-- **`pseudoMassExt` strictly anti on `Ioo 0 1`** (sub-interval of -`Ioo 0 2`): convenient when working with `tanh^2 ∈ [0, 1)` regime. -/ -theorem pseudoMassExt_strictAntiOn_Ioo_zero_one - {α : ℕ} (hα : 1 ≤ α) {r : ℝ} (hr : 0 < r) : - StrictAntiOn (pseudoMassExt hα hr) (Set.Ioo 0 1) := by - intro c₁ hc₁ c₂ hc₂ h - have hc₁_in : c₁ ∈ Set.Ioo (0 : ℝ) 2 := ⟨hc₁.1, by linarith [hc₁.2]⟩ - have hc₂_in : c₂ ∈ Set.Ioo (0 : ℝ) 2 := ⟨hc₂.1, by linarith [hc₂.2]⟩ - exact pseudoMassExt_strictAntiOn hα hr hc₁_in hc₂_in h - -/-- **`pseudoMassExt` antitone on `Ioo 0 1`** (sub-interval form). -/ -theorem pseudoMassExt_antitoneOn_Ioo_zero_one - {α : ℕ} (hα : 1 ≤ α) {r : ℝ} (hr : 0 < r) : - AntitoneOn (pseudoMassExt hα hr) (Set.Ioo 0 1) := - (pseudoMassExt_strictAntiOn_Ioo_zero_one hα hr).antitoneOn - -/-- **`-pseudoMassExt` is `StrictMonoOn (Ioo 0 1)`**: sub-interval. -/ -theorem neg_pseudoMassExt_strictMonoOn_Ioo_zero_one - {α : ℕ} (hα : 1 ≤ α) {r : ℝ} (hr : 0 < r) : - StrictMonoOn (fun c => -pseudoMassExt hα hr c) (Set.Ioo 0 1) := by - intro c₁ hc₁ c₂ hc₂ h - have hgt : pseudoMassExt hα hr c₂ < pseudoMassExt hα hr c₁ := - pseudoMassExt_strictAntiOn_Ioo_zero_one hα hr hc₁ hc₂ h - linarith - -/-- **`pseudoMassExt` strictly anti on `Ioc 0 1`** (boundary-inclusive -sub-interval): `Ioc 0 1 ⊂ Ioo 0 2` since `1 < 2`. -/ -theorem pseudoMassExt_strictAntiOn_Ioc_zero_one - {α : ℕ} (hα : 1 ≤ α) {r : ℝ} (hr : 0 < r) : - StrictAntiOn (pseudoMassExt hα hr) (Set.Ioc 0 1) := by - intro c₁ hc₁ c₂ hc₂ h - have hc₁_in : c₁ ∈ Set.Ioo (0 : ℝ) 2 := ⟨hc₁.1, by linarith [hc₁.2]⟩ - have hc₂_in : c₂ ∈ Set.Ioo (0 : ℝ) 2 := ⟨hc₂.1, by linarith [hc₂.2]⟩ - exact pseudoMassExt_strictAntiOn hα hr hc₁_in hc₂_in h - -/-- **`pseudoMassExt` antitone on `Ioc 0 1`**. -/ -theorem pseudoMassExt_antitoneOn_Ioc_zero_one - {α : ℕ} (hα : 1 ≤ α) {r : ℝ} (hr : 0 < r) : - AntitoneOn (pseudoMassExt hα hr) (Set.Ioc 0 1) := - (pseudoMassExt_strictAntiOn_Ioc_zero_one hα hr).antitoneOn - -/-- **`-pseudoMassExt` is `StrictMonoOn (Ioc 0 1)`**. -/ -theorem neg_pseudoMassExt_strictMonoOn_Ioc_zero_one - {α : ℕ} (hα : 1 ≤ α) {r : ℝ} (hr : 0 < r) : - StrictMonoOn (fun c => -pseudoMassExt hα hr c) (Set.Ioc 0 1) := by - intro c₁ hc₁ c₂ hc₂ h - have hgt : pseudoMassExt hα hr c₂ < pseudoMassExt hα hr c₁ := - pseudoMassExt_strictAntiOn_Ioc_zero_one hα hr hc₁ hc₂ h - linarith - -/-- **`-pseudoMassExt` is `MonotoneOn (Ioc 0 1)`**. -/ -theorem neg_pseudoMassExt_monotoneOn_Ioc_zero_one - {α : ℕ} (hα : 1 ≤ α) {r : ℝ} (hr : 0 < r) : - MonotoneOn (fun c => -pseudoMassExt hα hr c) (Set.Ioc 0 1) := - (neg_pseudoMassExt_strictMonoOn_Ioc_zero_one hα hr).monotoneOn - /-- **`pseudoMassExt(tanh(t)^2)` `ContinuousAt` for `0 < t`**: composition of continuous functions. `tanh` is continuous, squaring is continuous, `pseudoMassExt` is continuous at `tanh(t)^2 ∈ Ioo 0 1 ⊂ Ioo 0 2`. -/ @@ -334,46 +162,6 @@ theorem pseudoMassExt_tanh_sq_differentiableAt_pos change DifferentiableAt ℝ ((pseudoMassExt hα hr) ∘ (fun s : ℝ => Real.tanh s ^ 2)) t exact DifferentiableAt.comp t h_outer_diff h_inner_diff -/-- **`pseudoMassExt(tanh(t)^2)` strictly anti in `t` on `Ioi 0`**: -the composition of the strictly increasing `t ↦ tanh(t)^2` (mapping -`Ioi 0` into `Ioo 0 1`) with the strictly anti `pseudoMassExt` -(restricted to `Ioo 0 1`) is strictly anti. Useful for §17.5 §J=0 -slice analysis where the bridge is `pseudoMassExt(tanh(β·h)^2)` -parametrised by the product `β·h`. -/ -theorem pseudoMassExt_tanh_sq_strictAntiOn_Ioi_zero - {α : ℕ} (hα : 1 ≤ α) {r : ℝ} (hr : 0 < r) : - StrictAntiOn (fun t : ℝ => pseudoMassExt hα hr (Real.tanh t ^ 2)) - (Set.Ioi 0) := by - intro t₁ ht₁ t₂ ht₂ hlt - simp only [Set.mem_Ioi] at ht₁ ht₂ - have htanh_pos₁ : 0 < Real.tanh t₁ := by - rw [Real.tanh_eq_sinh_div_cosh] - exact div_pos (Real.sinh_pos_iff.mpr ht₁) (Real.cosh_pos _) - have htanh_pos₂ : 0 < Real.tanh t₂ := by - rw [Real.tanh_eq_sinh_div_cosh] - exact div_pos (Real.sinh_pos_iff.mpr ht₂) (Real.cosh_pos _) - have htanh_lt₁ : Real.tanh t₁ < 1 := lt_of_abs_lt (Real.abs_tanh_lt_one _) - have htanh_lt₂ : Real.tanh t₂ < 1 := lt_of_abs_lt (Real.abs_tanh_lt_one _) - have htanh_mono : Real.tanh t₁ < Real.tanh t₂ := Real.tanh_strictMono hlt - have hsq_lt : Real.tanh t₁ ^ 2 < Real.tanh t₂ ^ 2 := by - have h1 : Real.tanh t₁ ^ 2 = Real.tanh t₁ * Real.tanh t₁ := sq _ - have h2 : Real.tanh t₂ ^ 2 = Real.tanh t₂ * Real.tanh t₂ := sq _ - rw [h1, h2] - exact mul_lt_mul' htanh_mono.le htanh_mono htanh_pos₁.le htanh_pos₂ - have hmem₁ : Real.tanh t₁ ^ 2 ∈ Set.Ioo (0 : ℝ) 1 := by - refine ⟨by positivity, ?_⟩ - nlinarith - have hmem₂ : Real.tanh t₂ ^ 2 ∈ Set.Ioo (0 : ℝ) 1 := by - refine ⟨by positivity, ?_⟩ - nlinarith - exact pseudoMassExt_strictAntiOn_Ioo_zero_one hα hr hmem₁ hmem₂ hsq_lt - -/-- **`pseudoMassExt` continuous on `Ioo 0 2`**: lifted from -`pseudoMass_continuousOn`. -/ -theorem pseudoMassExt_continuousOn {α : ℕ} (hα : 1 ≤ α) {r : ℝ} (hr : 0 < r) : - ContinuousOn (pseudoMassExt hα hr) (Set.Ioo 0 2) := - pseudoMass_continuousOn hα hr - /-- **`pseudoMassExt c = 0 ↔ c ∉ Ioo 0 2`**: characterisation. The forward direction uses `pseudoMass_pos` (positive on `Ioo 0 2`) to contradict `pseudoMassExt = 0` when `c ∈ Ioo 0 2`. -/ @@ -396,44 +184,4 @@ theorem pseudoMassExt_pos_iff {α : ℕ} (hα : 1 ≤ α) {r : ℝ} (hr : 0 < r) rw [pseudoMassExt_of_not_mem hα hr hnotmem] at h_pos exact lt_irrefl 0 h_pos -/-- **`pseudoMassExt c ∈ Set.Ioi 0 ↔ c ∈ Ioo 0 2`**: combines positivity -iff with mem reformulation. -/ -theorem pseudoMassExt_mem_Ioi_iff_mem {α : ℕ} (hα : 1 ≤ α) {r : ℝ} - (hr : 0 < r) (c : ℝ) : - pseudoMassExt hα hr c ∈ Set.Ioi (0 : ℝ) ↔ c ∈ Set.Ioo (0 : ℝ) 2 := - pseudoMassExt_pos_iff hα hr c - -/-- **`pseudoMassExt c ∈ Set.Iio 0` is False**: `pseudoMassExt` is nonneg. -/ -theorem pseudoMassExt_not_mem_Iio_zero {α : ℕ} (hα : 1 ≤ α) {r : ℝ} - (hr : 0 < r) (c : ℝ) : - pseudoMassExt hα hr c ∉ Set.Iio (0 : ℝ) := - not_lt.mpr (pseudoMassExt_nonneg hα hr c) - -/-- **`pseudoMassExt 0 = 0`**: zero is not in `Ioo 0 2` (open interval). -/ -theorem pseudoMassExt_zero {α : ℕ} (hα : 1 ≤ α) {r : ℝ} (hr : 0 < r) : - pseudoMassExt hα hr 0 = 0 := - pseudoMassExt_of_not_mem hα hr (by simp [Set.mem_Ioo]) - -/-- **`pseudoMassExt 2 = 0`**: 2 is not in `Ioo 0 2` (open interval). -/ -theorem pseudoMassExt_two {α : ℕ} (hα : 1 ≤ α) {r : ℝ} (hr : 0 < r) : - pseudoMassExt hα hr 2 = 0 := - pseudoMassExt_of_not_mem hα hr (by simp [Set.mem_Ioo]) - -/-- **`pseudoMassExt` of a negative value = 0**. -/ -theorem pseudoMassExt_of_nonpos {α : ℕ} (hα : 1 ≤ α) {r : ℝ} (hr : 0 < r) - {c : ℝ} (hc : c ≤ 0) : - pseudoMassExt hα hr c = 0 := by - apply pseudoMassExt_of_not_mem - intro hmem - exact lt_irrefl 0 (lt_of_lt_of_le hmem.1 hc) - -/-- **`pseudoMassExt` of a value ≥ 2 = 0**. -/ -theorem pseudoMassExt_of_two_le {α : ℕ} (hα : 1 ≤ α) {r : ℝ} (hr : 0 < r) - {c : ℝ} (hc : 2 ≤ c) : - pseudoMassExt hα hr c = 0 := by - apply pseudoMassExt_of_not_mem - intro hmem - exact lt_irrefl 2 (lt_of_le_of_lt hc hmem.2) - - end IsingModel diff --git a/IsingModel/PseudoMass/FromParamsBounds.lean b/IsingModel/PseudoMass/FromParamsBounds.lean index 9e1cb0e86..3f366939a 100644 --- a/IsingModel/PseudoMass/FromParamsBounds.lean +++ b/IsingModel/PseudoMass/FromParamsBounds.lean @@ -1,7 +1,6 @@ -import IsingModel.PseudoMass.FromParamsBounds.Intervals - /-! # Pseudo-Mass Parameter Bounds -This compatibility module re-exports the split pseudo-mass parameter bound layer. +This compatibility module is retained as a stable import path in the +pseudo-mass parameter bound layer. -/ diff --git a/IsingModel/PseudoMass/FromParamsBounds/Intervals.lean b/IsingModel/PseudoMass/FromParamsBounds/Intervals.lean deleted file mode 100644 index 8e9677ae4..000000000 --- a/IsingModel/PseudoMass/FromParamsBounds/Intervals.lean +++ /dev/null @@ -1,331 +0,0 @@ -import IsingModel.PseudoMass.FromParamsBounds.JZeroComparisons - -/-! -# Pseudo-Mass Parameter Intervals - -This module is part of the split `IsingModel.PseudoMass.FromParamsBounds` development. --/ - -namespace IsingModel - -open Set Real Filter - -/-- **`pseudoMassFromParamsAtPair_at_h_zero pos iff truncated2 ≠ 0`**: -combines `_at_h_zero_pos_iff` (PR #1670, pos iff truncated2 > 0) with -`truncated2Infinite_pos_iff_ne_zero` (PR #1748). -/ -theorem pseudoMassFromParamsAtPair_at_h_zero_pos_iff_ne_zero - {α : ℕ} (hα : 1 ≤ α) {r : ℝ} (hr : 0 < r) (d : ℕ) - (Λ : Ambient.Exhaustion (Fin d → ℤ)) - [∀ n, Fintype (Ambient.inducedGraph (IsingModel.latticeGraph d) - (Λ.volume n)).edgeSet] - {J β : ℝ} (hJ : 0 ≤ J) (hβ : 0 < β) (x z : Fin d → ℤ) : - 0 < pseudoMassFromParamsAtPair hα hr d Λ - (⟨J, 0, β⟩ : IsingParams ℝ) x z ↔ - Ambient.truncated2Infinite (IsingModel.latticeGraph d) Λ - (⟨J, 0, β⟩ : IsingParams ℝ) x z ≠ 0 := by - have hf : Ferromagnetic (⟨J, 0, β⟩ : IsingParams ℝ) := - ⟨hJ, le_refl 0, hβ⟩ - rw [pseudoMassFromParamsAtPair_at_h_zero_pos_iff hα hr d Λ hJ hβ x z] - exact Ambient.truncated2Infinite_pos_iff_ne_zero - (IsingModel.latticeGraph d) Λ (⟨J, 0, β⟩ : IsingParams ℝ) hf x z - -/-- **`0 < pseudoMassFromParamsAtPair ↔ pseudoMassFromParamsAtPair ≠ 0`**: -trivial via `pseudoMassFromParamsAtPair_nonneg`. -/ -theorem pseudoMassFromParamsAtPair_pos_iff_ne_zero - {α : ℕ} (hα : 1 ≤ α) {r : ℝ} (hr : 0 < r) (d : ℕ) - (Λ : Ambient.Exhaustion (Fin d → ℤ)) - [∀ n, Fintype (Ambient.inducedGraph (IsingModel.latticeGraph d) - (Λ.volume n)).edgeSet] - (p : IsingParams ℝ) (x z : Fin d → ℤ) : - 0 < pseudoMassFromParamsAtPair hα hr d Λ p x z ↔ - pseudoMassFromParamsAtPair hα hr d Λ p x z ≠ 0 := - (pseudoMassFromParamsAtPair_nonneg hα hr d Λ p x z).lt_iff_ne.trans - ⟨fun h => h.symm, fun h => h.symm⟩ - -/-- **At `h = 0`, `pseudoMassFromParamsAtPair ∈ Ioo 0 ((2-truncated2)/(truncated2·r))`**: -sharper Ioo membership at h=0 using `(2-c)/(c·r)`. -/ -theorem pseudoMassFromParamsAtPair_at_h_zero_mem_Ioo_zero_two_sub_div - {α : ℕ} (hα : 1 ≤ α) {r : ℝ} (hr : 0 < r) (d : ℕ) - (Λ : Ambient.Exhaustion (Fin d → ℤ)) - [∀ n, Fintype (Ambient.inducedGraph (IsingModel.latticeGraph d) - (Λ.volume n)).edgeSet] - (J β : ℝ) (x z : Fin d → ℤ) - (htrunc : Ambient.truncated2Infinite (IsingModel.latticeGraph d) Λ - (⟨J, 0, β⟩ : IsingParams ℝ) x z ∈ Set.Ioo (0 : ℝ) 2) : - pseudoMassFromParamsAtPair hα hr d Λ (⟨J, 0, β⟩ : IsingParams ℝ) x z ∈ - Set.Ioo (0 : ℝ) - ((2 - Ambient.truncated2Infinite (IsingModel.latticeGraph d) Λ - (⟨J, 0, β⟩ : IsingParams ℝ) x z) / - (Ambient.truncated2Infinite (IsingModel.latticeGraph d) Λ - (⟨J, 0, β⟩ : IsingParams ℝ) x z * r)) := - ⟨pseudoMassFromParamsAtPair_at_h_zero_pos_of_truncated2_mem - hα hr d Λ J β x z htrunc, - pseudoMassFromParamsAtPair_at_h_zero_lt_two_sub_div_mul_r - hα hr d Λ J β x z htrunc⟩ - -/-- **At `J = 0` distinct, `pseudoMassFromParamsAtPair ∈ Ioo 0 ((2-tanh^2)/(tanh^2·r))`**. -/ -theorem pseudoMassFromParamsAtPair_at_J_zero_distinct_mem_Ioo_zero_two_sub_div - {α : ℕ} (hα : 1 ≤ α) {r : ℝ} (hr : 0 < r) (d : ℕ) - (Λ : Ambient.Exhaustion (Fin d → ℤ)) - [∀ n, Fintype (Ambient.inducedGraph (IsingModel.latticeGraph d) - (Λ.volume n)).edgeSet] - {h β : ℝ} (hh : 0 < h) (hβ : 0 < β) {x z : Fin d → ℤ} (hxz : x ≠ z) : - pseudoMassFromParamsAtPair hα hr d Λ (⟨0, h, β⟩ : IsingParams ℝ) x z ∈ - Set.Ioo (0 : ℝ) ((2 - Real.tanh (β * h) ^ 2) / (Real.tanh (β * h) ^ 2 * r)) := - ⟨pseudoMassFromParamsAtPair_pos_at_J_zero hα hr d Λ hh hβ hxz, - pseudoMassFromParamsAtPair_at_J_zero_distinct_lt_two_sub_tanh_sq - hα hr d Λ hh hβ hxz⟩ - -/-- **`¬(pseudoMassFromParamsAtPair < 0)`**: trivial via nonneg. -/ -theorem pseudoMassFromParamsAtPair_not_lt_zero - {α : ℕ} (hα : 1 ≤ α) {r : ℝ} (hr : 0 < r) (d : ℕ) - (Λ : Ambient.Exhaustion (Fin d → ℤ)) - [∀ n, Fintype (Ambient.inducedGraph (IsingModel.latticeGraph d) - (Λ.volume n)).edgeSet] - (p : IsingParams ℝ) (x z : Fin d → ℤ) : - ¬ (pseudoMassFromParamsAtPair hα hr d Λ p x z < 0) := - not_lt.mpr (pseudoMassFromParamsAtPair_nonneg hα hr d Λ p x z) - -/-- **`pseudoMassFromParamsAtPair ≤ 0 ↔ pseudoMassFromParamsAtPair = 0`**: -trivial via nonneg + antisymmetry. -/ -theorem pseudoMassFromParamsAtPair_le_zero_iff_eq_zero - {α : ℕ} (hα : 1 ≤ α) {r : ℝ} (hr : 0 < r) (d : ℕ) - (Λ : Ambient.Exhaustion (Fin d → ℤ)) - [∀ n, Fintype (Ambient.inducedGraph (IsingModel.latticeGraph d) - (Λ.volume n)).edgeSet] - (p : IsingParams ℝ) (x z : Fin d → ℤ) : - pseudoMassFromParamsAtPair hα hr d Λ p x z ≤ 0 ↔ - pseudoMassFromParamsAtPair hα hr d Λ p x z = 0 := by - refine ⟨?_, fun h => le_of_eq h⟩ - intro hle - exact le_antisymm hle (pseudoMassFromParamsAtPair_nonneg hα hr d Λ p x z) - -/-- **`pseudoMassFromParamsAtPair < pseudoMassExt(c) ↔ c < correlation`** when both -in `Ioo 0 2`: iff form using the bridge identity. -/ -theorem pseudoMassFromParamsAtPair_lt_pseudoMassExt_iff_lt_corr - {α : ℕ} (hα : 1 ≤ α) {r : ℝ} (hr : 0 < r) (d : ℕ) - (Λ : Ambient.Exhaustion (Fin d → ℤ)) - [∀ n, Fintype (Ambient.inducedGraph (IsingModel.latticeGraph d) - (Λ.volume n)).edgeSet] - (p : IsingParams ℝ) (x z : Fin d → ℤ) - {c : ℝ} (hc : c ∈ Set.Ioo (0 : ℝ) 2) - (hcorr : Ambient.correlationInfinite (IsingModel.latticeGraph d) Λ p {x, z} - ∈ Set.Ioo (0 : ℝ) 2) : - pseudoMassFromParamsAtPair hα hr d Λ p x z < - pseudoMassExt hα hr c ↔ - c < Ambient.correlationInfinite (IsingModel.latticeGraph d) Λ p {x, z} := by - unfold pseudoMassFromParamsAtPair - exact pseudoMassExt_lt_iff hα hr hc hcorr - -/-- **`pseudoMassExt(c) < pseudoMassFromParamsAtPair ↔ correlation < c`**: companion. -/ -theorem pseudoMassFromParamsAtPair_gt_pseudoMassExt_iff_corr_lt - {α : ℕ} (hα : 1 ≤ α) {r : ℝ} (hr : 0 < r) (d : ℕ) - (Λ : Ambient.Exhaustion (Fin d → ℤ)) - [∀ n, Fintype (Ambient.inducedGraph (IsingModel.latticeGraph d) - (Λ.volume n)).edgeSet] - (p : IsingParams ℝ) (x z : Fin d → ℤ) - {c : ℝ} (hc : c ∈ Set.Ioo (0 : ℝ) 2) - (hcorr : Ambient.correlationInfinite (IsingModel.latticeGraph d) Λ p {x, z} - ∈ Set.Ioo (0 : ℝ) 2) : - pseudoMassExt hα hr c < - pseudoMassFromParamsAtPair hα hr d Λ p x z ↔ - Ambient.correlationInfinite (IsingModel.latticeGraph d) Λ p {x, z} < c := by - unfold pseudoMassFromParamsAtPair - exact pseudoMassExt_lt_iff hα hr hcorr hc - -/-- **`pseudoMassFromParamsAtPair ≤ pseudoMassExt(c) ↔ c ≤ correlation`**: -non-strict iff form. -/ -theorem pseudoMassFromParamsAtPair_le_pseudoMassExt_iff_le_corr - {α : ℕ} (hα : 1 ≤ α) {r : ℝ} (hr : 0 < r) (d : ℕ) - (Λ : Ambient.Exhaustion (Fin d → ℤ)) - [∀ n, Fintype (Ambient.inducedGraph (IsingModel.latticeGraph d) - (Λ.volume n)).edgeSet] - (p : IsingParams ℝ) (x z : Fin d → ℤ) - {c : ℝ} (hc : c ∈ Set.Ioo (0 : ℝ) 2) - (hcorr : Ambient.correlationInfinite (IsingModel.latticeGraph d) Λ p {x, z} - ∈ Set.Ioo (0 : ℝ) 2) : - pseudoMassFromParamsAtPair hα hr d Λ p x z ≤ - pseudoMassExt hα hr c ↔ - c ≤ Ambient.correlationInfinite (IsingModel.latticeGraph d) Λ p {x, z} := by - unfold pseudoMassFromParamsAtPair - exact pseudoMassExt_le_iff hα hr hc hcorr - -/-- **`pseudoMassExt(c) ≤ pseudoMassFromParamsAtPair ↔ correlation ≤ c`**. -/ -theorem pseudoMassFromParamsAtPair_ge_pseudoMassExt_iff_corr_le - {α : ℕ} (hα : 1 ≤ α) {r : ℝ} (hr : 0 < r) (d : ℕ) - (Λ : Ambient.Exhaustion (Fin d → ℤ)) - [∀ n, Fintype (Ambient.inducedGraph (IsingModel.latticeGraph d) - (Λ.volume n)).edgeSet] - (p : IsingParams ℝ) (x z : Fin d → ℤ) - {c : ℝ} (hc : c ∈ Set.Ioo (0 : ℝ) 2) - (hcorr : Ambient.correlationInfinite (IsingModel.latticeGraph d) Λ p {x, z} - ∈ Set.Ioo (0 : ℝ) 2) : - pseudoMassExt hα hr c ≤ - pseudoMassFromParamsAtPair hα hr d Λ p x z ↔ - Ambient.correlationInfinite (IsingModel.latticeGraph d) Λ p {x, z} ≤ c := by - unfold pseudoMassFromParamsAtPair - exact pseudoMassExt_le_iff hα hr hcorr hc - -/-- **`pseudoMassFromParamsAtPair = pseudoMassExt(c) ↔ correlation = c`**: -equality iff. -/ -theorem pseudoMassFromParamsAtPair_eq_pseudoMassExt_iff_corr_eq - {α : ℕ} (hα : 1 ≤ α) {r : ℝ} (hr : 0 < r) (d : ℕ) - (Λ : Ambient.Exhaustion (Fin d → ℤ)) - [∀ n, Fintype (Ambient.inducedGraph (IsingModel.latticeGraph d) - (Λ.volume n)).edgeSet] - (p : IsingParams ℝ) (x z : Fin d → ℤ) - {c : ℝ} (hc : c ∈ Set.Ioo (0 : ℝ) 2) - (hcorr : Ambient.correlationInfinite (IsingModel.latticeGraph d) Λ p {x, z} - ∈ Set.Ioo (0 : ℝ) 2) : - pseudoMassFromParamsAtPair hα hr d Λ p x z = - pseudoMassExt hα hr c ↔ - Ambient.correlationInfinite (IsingModel.latticeGraph d) Λ p {x, z} = c := by - unfold pseudoMassFromParamsAtPair - rw [pseudoMassExt_eq_iff_of_mem hα hr hc hcorr] - exact eq_comm - -/-- **Λ-uniform `pseudoMass(1)` lower bound at h=0**: combines -`_at_h_zero_ge_pseudoMass_one` (PR #1725) with `_indep_exhaustion` -(PR #1666) to make the lower bound explicitly Λ-independent. For any -two exhaustions Λ, Λ', the bridge values are equal (under ferromagnetic), -and both bounded below by `pseudoMass(1)`. -/ -theorem pseudoMassFromParamsAtPair_at_h_zero_ge_pseudoMass_one_uniform - {α : ℕ} (hα : 1 ≤ α) {r : ℝ} (hr : 0 < r) (d : ℕ) - (Λ Λ' : Ambient.Exhaustion (Fin d → ℤ)) - [∀ n, Fintype (Ambient.inducedGraph (IsingModel.latticeGraph d) - (Λ.volume n)).edgeSet] - [∀ n, Fintype (Ambient.inducedGraph (IsingModel.latticeGraph d) - (Λ'.volume n)).edgeSet] - {J β : ℝ} (hJ : 0 ≤ J) (hβ : 0 < β) (x z : Fin d → ℤ) - (htrunc_pos : 0 < Ambient.truncated2Infinite (IsingModel.latticeGraph d) Λ - (⟨J, 0, β⟩ : IsingParams ℝ) x z) : - pseudoMass hα hr (show (1 : ℝ) ∈ Set.Ioo 0 2 from - ⟨zero_lt_one, one_lt_two⟩) ≤ - pseudoMassFromParamsAtPair hα hr d Λ' (⟨J, 0, β⟩ : IsingParams ℝ) x z := by - have hf : Ferromagnetic (⟨J, 0, β⟩ : IsingParams ℝ) := - ⟨hJ, le_refl 0, hβ⟩ - rw [← pseudoMassFromParamsAtPair_indep_exhaustion hα hr d Λ Λ' - (⟨J, 0, β⟩ : IsingParams ℝ) hf x z] - exact pseudoMassFromParamsAtPair_at_h_zero_ge_pseudoMass_one - hα hr d Λ hJ hβ x z htrunc_pos - -/-- **`pseudoMassFromParamsAtPair ∈ Ici 0`** (always): direct from -nonneg. -/ -theorem pseudoMassFromParamsAtPair_mem_Ici_zero - {α : ℕ} (hα : 1 ≤ α) {r : ℝ} (hr : 0 < r) (d : ℕ) - (Λ : Ambient.Exhaustion (Fin d → ℤ)) - [∀ n, Fintype (Ambient.inducedGraph (IsingModel.latticeGraph d) - (Λ.volume n)).edgeSet] - (p : IsingParams ℝ) (x z : Fin d → ℤ) : - pseudoMassFromParamsAtPair hα hr d Λ p x z ∈ Set.Ici (0 : ℝ) := - pseudoMassFromParamsAtPair_nonneg hα hr d Λ p x z - -/-- **At `J = 0` distinct, `pseudoMassFromParamsAtPair ∈ Ioo 0 (log(2/tanh^2)/r)`**: -J=0 analog of `_at_h_zero_mem_Ioo_log_two_div`. -/ -theorem pseudoMassFromParamsAtPair_at_J_zero_distinct_mem_Ioo_zero_log_two_div - {α : ℕ} (hα : 1 ≤ α) {r : ℝ} (hr : 0 < r) (d : ℕ) - (Λ : Ambient.Exhaustion (Fin d → ℤ)) - [∀ n, Fintype (Ambient.inducedGraph (IsingModel.latticeGraph d) - (Λ.volume n)).edgeSet] - {h β : ℝ} (hh : 0 < h) (hβ : 0 < β) {x z : Fin d → ℤ} (hxz : x ≠ z) : - pseudoMassFromParamsAtPair hα hr d Λ (⟨0, h, β⟩ : IsingParams ℝ) x z ∈ - Set.Ioo (0 : ℝ) (Real.log (2 / Real.tanh (β * h) ^ 2) / r) := - ⟨pseudoMassFromParamsAtPair_pos_at_J_zero hα hr d Λ hh hβ hxz, - pseudoMassFromParamsAtPair_at_J_zero_distinct_lt_log_two_div_tanh_sq - hα hr d Λ hh hβ hxz⟩ - -/-- **At `h = 0` with `truncated2 ∈ Ioo 0 2`, -`pseudoMassFromParamsAtPair_at_h_zero ∈ Ioo 0 (log(2/truncated2)/r)`**: -bundles `_pos_of_truncated2_mem` (PR #1679) + `_lt_log_two_div_truncated2` -(PR #1707). -/ -theorem pseudoMassFromParamsAtPair_at_h_zero_mem_Ioo_zero_log_two_div - {α : ℕ} (hα : 1 ≤ α) {r : ℝ} (hr : 0 < r) (d : ℕ) - (Λ : Ambient.Exhaustion (Fin d → ℤ)) - [∀ n, Fintype (Ambient.inducedGraph (IsingModel.latticeGraph d) - (Λ.volume n)).edgeSet] - (J β : ℝ) (x z : Fin d → ℤ) - (htrunc : Ambient.truncated2Infinite (IsingModel.latticeGraph d) Λ - (⟨J, 0, β⟩ : IsingParams ℝ) x z ∈ Set.Ioo (0 : ℝ) 2) : - pseudoMassFromParamsAtPair hα hr d Λ (⟨J, 0, β⟩ : IsingParams ℝ) x z ∈ - Set.Ioo (0 : ℝ) - (Real.log (2 / Ambient.truncated2Infinite (IsingModel.latticeGraph d) Λ - (⟨J, 0, β⟩ : IsingParams ℝ) x z) / r) := - ⟨pseudoMassFromParamsAtPair_at_h_zero_pos_of_truncated2_mem - hα hr d Λ J β x z htrunc, - pseudoMassFromParamsAtPair_at_h_zero_lt_log_two_div_truncated2 - hα hr d Λ J β x z htrunc⟩ - -/-- **At `h = 0` with `truncated2 ∈ Ioo 0 2`, -`pseudoMassFromParamsAtPair_at_h_zero ∈ Iio (log(2/truncated2)/r)`**. -/ -theorem pseudoMassFromParamsAtPair_at_h_zero_mem_Iio_log_two_div - {α : ℕ} (hα : 1 ≤ α) {r : ℝ} (hr : 0 < r) (d : ℕ) - (Λ : Ambient.Exhaustion (Fin d → ℤ)) - [∀ n, Fintype (Ambient.inducedGraph (IsingModel.latticeGraph d) - (Λ.volume n)).edgeSet] - (J β : ℝ) (x z : Fin d → ℤ) - (htrunc : Ambient.truncated2Infinite (IsingModel.latticeGraph d) Λ - (⟨J, 0, β⟩ : IsingParams ℝ) x z ∈ Set.Ioo (0 : ℝ) 2) : - pseudoMassFromParamsAtPair hα hr d Λ (⟨J, 0, β⟩ : IsingParams ℝ) x z ∈ - Set.Iio (Real.log (2 / Ambient.truncated2Infinite (IsingModel.latticeGraph d) Λ - (⟨J, 0, β⟩ : IsingParams ℝ) x z) / r) := - pseudoMassFromParamsAtPair_at_h_zero_lt_log_two_div_truncated2 - hα hr d Λ J β x z htrunc - -/-- **At `h = 0`, `pseudoMassFromParamsAtPair ∈ Ici 0`**: trivial. -/ -theorem pseudoMassFromParamsAtPair_at_h_zero_mem_Ici_zero - {α : ℕ} (hα : 1 ≤ α) {r : ℝ} (hr : 0 < r) (d : ℕ) - (Λ : Ambient.Exhaustion (Fin d → ℤ)) - [∀ n, Fintype (Ambient.inducedGraph (IsingModel.latticeGraph d) - (Λ.volume n)).edgeSet] - (J β : ℝ) (x z : Fin d → ℤ) : - pseudoMassFromParamsAtPair hα hr d Λ (⟨J, 0, β⟩ : IsingParams ℝ) x z ∈ - Set.Ici (0 : ℝ) := - pseudoMassFromParamsAtPair_nonneg hα hr d Λ _ x z - -/-- **At `J = 0` distinct, `pseudoMassFromParamsAtPair ∈ Iio (log(2/tanh^2)/r)`**. -/ -theorem pseudoMassFromParamsAtPair_at_J_zero_distinct_mem_Iio_log_two_div - {α : ℕ} (hα : 1 ≤ α) {r : ℝ} (hr : 0 < r) (d : ℕ) - (Λ : Ambient.Exhaustion (Fin d → ℤ)) - [∀ n, Fintype (Ambient.inducedGraph (IsingModel.latticeGraph d) - (Λ.volume n)).edgeSet] - {h β : ℝ} (hh : 0 < h) (hβ : 0 < β) {x z : Fin d → ℤ} (hxz : x ≠ z) : - pseudoMassFromParamsAtPair hα hr d Λ (⟨0, h, β⟩ : IsingParams ℝ) x z ∈ - Set.Iio (Real.log (2 / Real.tanh (β * h) ^ 2) / r) := - pseudoMassFromParamsAtPair_at_J_zero_distinct_lt_log_two_div_tanh_sq - hα hr d Λ hh hβ hxz - -/-- **At `J = 0` distinct, `pseudoMassFromParamsAtPair ∈ Iio ((2-tanh^2)/(tanh^2·r))`**. -/ -theorem pseudoMassFromParamsAtPair_at_J_zero_distinct_mem_Iio_two_sub_tanh_sq - {α : ℕ} (hα : 1 ≤ α) {r : ℝ} (hr : 0 < r) (d : ℕ) - (Λ : Ambient.Exhaustion (Fin d → ℤ)) - [∀ n, Fintype (Ambient.inducedGraph (IsingModel.latticeGraph d) - (Λ.volume n)).edgeSet] - {h β : ℝ} (hh : 0 < h) (hβ : 0 < β) {x z : Fin d → ℤ} (hxz : x ≠ z) : - pseudoMassFromParamsAtPair hα hr d Λ (⟨0, h, β⟩ : IsingParams ℝ) x z ∈ - Set.Iio ((2 - Real.tanh (β * h) ^ 2) / (Real.tanh (β * h) ^ 2 * r)) := - pseudoMassFromParamsAtPair_at_J_zero_distinct_lt_two_sub_tanh_sq - hα hr d Λ hh hβ hxz - -/-- **`pseudoMassFromParamsAtPair ∈ Ioi 0`** when corr ∈ Ioo 0 2: -/ -theorem pseudoMassFromParamsAtPair_mem_Ioi_zero_of_corr_mem - {α : ℕ} (hα : 1 ≤ α) {r : ℝ} (hr : 0 < r) (d : ℕ) - (Λ : Ambient.Exhaustion (Fin d → ℤ)) - [∀ n, Fintype (Ambient.inducedGraph (IsingModel.latticeGraph d) - (Λ.volume n)).edgeSet] - (p : IsingParams ℝ) (x z : Fin d → ℤ) - (hcorr : Ambient.correlationInfinite (IsingModel.latticeGraph d) Λ p {x, z} - ∈ Set.Ioo (0 : ℝ) 2) : - pseudoMassFromParamsAtPair hα hr d Λ p x z ∈ Set.Ioi (0 : ℝ) := - pseudoMassFromParamsAtPair_pos_of_corr_mem hα hr d Λ p x z hcorr - -/-- **`pseudoMassFromParamsAtPair ∉ Iio 0`**: trivial. -/ -theorem pseudoMassFromParamsAtPair_not_mem_Iio_zero - {α : ℕ} (hα : 1 ≤ α) {r : ℝ} (hr : 0 < r) (d : ℕ) - (Λ : Ambient.Exhaustion (Fin d → ℤ)) - [∀ n, Fintype (Ambient.inducedGraph (IsingModel.latticeGraph d) - (Λ.volume n)).edgeSet] - (p : IsingParams ℝ) (x z : Fin d → ℤ) : - pseudoMassFromParamsAtPair hα hr d Λ p x z ∉ Set.Iio (0 : ℝ) := - not_lt.mpr (pseudoMassFromParamsAtPair_nonneg hα hr d Λ p x z) - -end IsingModel From 4c1145b6b836d5cf0c8b0b851654396278a06ee7 Mon Sep 17 00:00:00 2001 From: phasetr Date: Fri, 17 Jul 2026 02:00:10 +0900 Subject: [PATCH 3/3] refactor(transfermatrix): drop redundant Mathlib.Tactic umbrella import Import hygiene (tier-2 audit finding M2): CycleGraphLink no longer needs the full `import Mathlib.Tactic` umbrella; the tactics it uses are provided by the existing SimpleGraph.Circulant/.Finite imports. The sibling WalkSum candidate (Mathlib.Tactic.Positivity) was checked and REVERTED -- positivity is genuinely used there. Build green (zero warnings), GKSTest passes. Co-Authored-By: Claude Fable 5 --- IsingModel/TransferMatrix/CycleGraphLink.lean | 1 - 1 file changed, 1 deletion(-) diff --git a/IsingModel/TransferMatrix/CycleGraphLink.lean b/IsingModel/TransferMatrix/CycleGraphLink.lean index 0bde91d06..3ebe2ab49 100644 --- a/IsingModel/TransferMatrix/CycleGraphLink.lean +++ b/IsingModel/TransferMatrix/CycleGraphLink.lean @@ -1,6 +1,5 @@ import Mathlib.Combinatorics.SimpleGraph.Circulant import Mathlib.Combinatorics.SimpleGraph.Finite -import Mathlib.Tactic import IsingModel.GibbsMeasure import IsingModel.Hamiltonian