From e19c2c9f28aa25400df66112639650af11baf1cf Mon Sep 17 00:00:00 2001 From: allaun Date: Thu, 18 Jun 2026 15:32:01 -0500 Subject: [PATCH] =?UTF-8?q?fix(lean):=20complete=20N3L=5FEnergy.lean=20bui?= =?UTF-8?q?ld=20=E2=80=94=20fix=20rcases=20shadowing,=20fraction=20additio?= =?UTF-8?q?n,=20linarith=20with=20=E2=88=80=20quantifier?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit - Fix rcases (rfl|rfl|rfl) shadowing by using named patterns hl_i/hl_j/hl_m with rw - Fix fraction addition calc block: replace simp with field_simp + ring - Fix linarith failures: extract specific hm_i/hm_j/hm_m from ∀ hmass - 3 original sorries preserved (peak_integrable_over_R, signedArea_zero_implies_perpDist_zero, no_collinear_at_zero_energy) Build: 8587 jobs, 0 errors (lake build Semantics) --- .../lean/Semantics/Semantics.lean | 1 + .../lean/Semantics/Semantics/N3L_Energy.lean | 545 ++++++++++++++++++ 2 files changed, 546 insertions(+) create mode 100644 0-Core-Formalism/lean/Semantics/Semantics/N3L_Energy.lean diff --git a/0-Core-Formalism/lean/Semantics/Semantics.lean b/0-Core-Formalism/lean/Semantics/Semantics.lean index 9bea1fb6..f84bde99 100644 --- a/0-Core-Formalism/lean/Semantics/Semantics.lean +++ b/0-Core-Formalism/lean/Semantics/Semantics.lean @@ -213,6 +213,7 @@ import Semantics.CGAVersorAddress import Semantics.FAMMCoChain import Semantics.NKHodgeFAMM import Semantics.Goxel +import Semantics.N3L_Energy namespace Semantics diff --git a/0-Core-Formalism/lean/Semantics/Semantics/N3L_Energy.lean b/0-Core-Formalism/lean/Semantics/Semantics/N3L_Energy.lean new file mode 100644 index 00000000..302e5bfd --- /dev/null +++ b/0-Core-Formalism/lean/Semantics/Semantics/N3L_Energy.lean @@ -0,0 +1,545 @@ +/- + N3L_Energy.lean — No-Three-in-Line energy rigidity theorem + + Formalizes the energy-minimization approach to the + No-Three-in-Line problem in ℝ² with Gaussian ansatz. + + Main result: no_collinear_at_zero_energy + E = 0 (energy of all lines) ⇒ no three peaks collinear +-/ + +import Mathlib.Data.Real.Basic +import Mathlib.Analysis.SpecialFunctions.Exp +import Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral +import Mathlib.MeasureTheory.Integral.Bochner.Basic +import Mathlib.Data.Finset.Basic +import Mathlib.Tactic + +open Real MeasureTheory Finset + +namespace Semantics.N3L_Energy + +-- ═══════════════════════════════════════════════════════════════════════════ +-- §0 CORE DEFINITIONS +-- ═══════════════════════════════════════════════════════════════════════════ + +noncomputable def gaussian2D (σ m : ℝ) (x : ℝ × ℝ) : ℝ := + m / (2 * π * σ ^ 2) * Real.exp (-(x.1 ^ 2 + x.2 ^ 2) / (2 * σ ^ 2)) + +noncomputable def gaussianAnsatz_eval (σ : ℝ) {k : ℕ} + (positions : Fin k → ℝ × ℝ) (masses : Fin k → ℝ) (x : ℝ × ℝ) : ℝ := + (Finset.univ : Finset (Fin k)).sum (fun i => + gaussian2D σ (masses i) (x.1 - (positions i).1, x.2 - (positions i).2)) + +noncomputable def penalty (lam z : ℝ) : ℝ := + if z > 0 then lam * z ^ 2 else 0 + +noncomputable def σ_crit : ℝ := 3 / (2 * Real.sqrt (2 * π)) + +def signedArea (p₁ p₂ p₃ : ℝ × ℝ) : ℝ := + (p₂.1 - p₁.1) * (p₃.2 - p₁.2) - (p₃.1 - p₁.1) * (p₂.2 - p₁.2) + +def perpDistance (x₀ y₀ a b s t : ℝ) : ℝ := + |a * (t - y₀) - b * (s - x₀)| + +noncomputable def ansatzLineDensity (σ : ℝ) {k : ℕ} + (positions : Fin k → ℝ × ℝ) (masses : Fin k → ℝ) + (a b s t : ℝ) : ℝ := + ∫ τ : ℝ, gaussianAnsatz_eval σ positions masses (s + a * τ, t + b * τ) + +noncomputable def energy {ι : Type*} [Fintype ι] [DecidableEq ι] + (lam : ℝ) (densities : ι → ℝ) : ℝ := + Finset.univ.sum (fun i => penalty lam (densities i - 2)) + +-- ═══════════════════════════════════════════════════════════════════════════ +-- §1 GAUSSIAN INTEGRAL +-- ═══════════════════════════════════════════════════════════════════════════ + +lemma integral_comp_add_right_ℝ (f : ℝ → ℝ) (x₀ : ℝ) : + (∫ τ : ℝ, f (τ - x₀)) = (∫ u : ℝ, f u) := by + have hp : MeasurePreserving (fun τ : ℝ => τ - x₀) volume volume := by + simpa [sub_eq_add_neg] using measurePreserving_add_right volume (-x₀) + have hembed : MeasurableEmbedding (fun τ : ℝ => τ - x₀) := by + simpa [sub_eq_add_neg, add_comm] using measurableEmbedding_addLeft (-x₀) + simpa using (hp.integral_comp hembed f) + +theorem integral_gaussian_1d (σ : ℝ) (hσ : σ > 0) : + (∫ t : ℝ, Real.exp (-(t ^ 2 / (2 * σ ^ 2)))) = σ * Real.sqrt (2 * π) := by + have hg := integral_gaussian (1 / (2 * σ ^ 2)) + have h_eq : (∫ t : ℝ, Real.exp (-(t ^ 2 / (2 * σ ^ 2)))) = + (∫ t : ℝ, Real.exp (-(1 / (2 * σ ^ 2)) * t ^ 2)) := by + refine integral_congr_ae ?_ + filter_upwards with t; apply congrArg Real.exp; field_simp [hσ.ne.symm] + rw [h_eq, hg] + calc + Real.sqrt (π / (1 / (2 * σ ^ 2))) = Real.sqrt (π * (2 * σ ^ 2)) := by + field_simp [hσ.ne.symm] + _ = Real.sqrt ((σ ^ 2) * (2 * π)) := by + apply congrArg Real.sqrt; ring + _ = Real.sqrt (σ ^ 2) * Real.sqrt (2 * π) := by rw [Real.sqrt_mul (sq_nonneg σ)] + _ = σ * Real.sqrt (2 * π) := by rw [Real.sqrt_sq (le_of_lt hσ)] + +theorem integral_gaussian_1d_shifted (σ x₀ : ℝ) (hσ : σ > 0) : + (∫ t : ℝ, Real.exp (-(t - x₀) ^ 2 / (2 * σ ^ 2))) = σ * Real.sqrt (2 * π) := by + calc + (∫ t : ℝ, Real.exp (-(t - x₀) ^ 2 / (2 * σ ^ 2))) + = (∫ u : ℝ, Real.exp (-u ^ 2 / (2 * σ ^ 2))) := + integral_comp_add_right_ℝ (fun u : ℝ => Real.exp (-u ^ 2 / (2 * σ ^ 2))) x₀ + _ = (∫ t : ℝ, Real.exp (-(t ^ 2 / (2 * σ ^ 2)))) := by + refine integral_congr_ae ?_ + filter_upwards with t; field_simp [hσ.ne.symm] + _ = σ * Real.sqrt (2 * π) := integral_gaussian_1d σ hσ + +lemma exp_sum_of_sq (t d σ : ℝ) : + Real.exp (-(t ^ 2 + d ^ 2) / (2 * σ ^ 2)) = + Real.exp (-d ^ 2 / (2 * σ ^ 2)) * Real.exp (-t ^ 2 / (2 * σ ^ 2)) := by + rw [← Real.exp_add]; ring_nf + +theorem gaussian_line_integral_at_distance + (σ m d : ℝ) (hσ : σ > 0) (hm : m ≥ 0) : + (∫ τ : ℝ, gaussian2D σ m (τ, d)) = + m / (σ * Real.sqrt (2 * π)) * Real.exp (-d ^ 2 / (2 * σ ^ 2)) := by + unfold gaussian2D + calc + (∫ τ : ℝ, m / (2 * π * σ ^ 2) * Real.exp (-(τ ^ 2 + d ^ 2) / (2 * σ ^ 2))) + = m / (2 * π * σ ^ 2) * (∫ τ : ℝ, Real.exp (-(τ ^ 2 + d ^ 2) / (2 * σ ^ 2))) := by + rw [integral_const_mul] + _ = m / (2 * π * σ ^ 2) * (Real.exp (-d ^ 2 / (2 * σ ^ 2)) * + (∫ τ : ℝ, Real.exp (-τ ^ 2 / (2 * σ ^ 2)))) := by + calc + m / (2 * π * σ ^ 2) * (∫ τ : ℝ, Real.exp (-(τ ^ 2 + d ^ 2) / (2 * σ ^ 2))) + = m / (2 * π * σ ^ 2) * (∫ τ : ℝ, Real.exp (-d ^ 2 / (2 * σ ^ 2)) * + Real.exp (-τ ^ 2 / (2 * σ ^ 2))) := by + refine congrArg (fun t => m / (2 * π * σ ^ 2) * t) ?_ + refine integral_congr_ae ?_ + filter_upwards with τ; exact exp_sum_of_sq τ d σ + _ = m / (2 * π * σ ^ 2) * (Real.exp (-d ^ 2 / (2 * σ ^ 2)) * + (∫ τ : ℝ, Real.exp (-τ ^ 2 / (2 * σ ^ 2)))) := by + rw [integral_const_mul] + _ = m / (2 * π * σ ^ 2) * (Real.exp (-d ^ 2 / (2 * σ ^ 2)) * + (σ * Real.sqrt (2 * π))) := by + have h_gauss : (∫ τ : ℝ, Real.exp (-τ ^ 2 / (2 * σ ^ 2))) = σ * Real.sqrt (2 * π) := by + calc + (∫ τ : ℝ, Real.exp (-τ ^ 2 / (2 * σ ^ 2))) = (∫ τ : ℝ, Real.exp (-(τ ^ 2 / (2 * σ ^ 2)))) := by + refine integral_congr_ae ?_ + filter_upwards with τ; apply congrArg Real.exp; field_simp [hσ.ne.symm] + _ = σ * Real.sqrt (2 * π) := integral_gaussian_1d σ hσ + rw [h_gauss] + _ = m / (σ * Real.sqrt (2 * π)) * Real.exp (-d ^ 2 / (2 * σ ^ 2)) := by + have hs2pi_pos : Real.sqrt (2 * π) > 0 := by positivity + field_simp [hσ.ne.symm, hs2pi_pos.ne.symm] + calc + m * Real.sqrt (2 * π) ^ 2 = m * (2 * π) := by + rw [Real.sq_sqrt (show 0 ≤ 2 * π by positivity)] + _ = m * 2 * π := by ring + +theorem peak_contribution_on_axis + (σ m x₀ y₀ t : ℝ) (hσ : σ > 0) (hm : m ≥ 0) : + (∫ τ : ℝ, gaussian2D σ m (τ - x₀, t - y₀)) = + m / (σ * Real.sqrt (2 * π)) * Real.exp (-(t - y₀) ^ 2 / (2 * σ ^ 2)) := by + calc + (∫ τ : ℝ, gaussian2D σ m (τ - x₀, t - y₀)) + = (∫ u : ℝ, gaussian2D σ m (u, t - y₀)) := + integral_comp_add_right_ℝ (fun u : ℝ => gaussian2D σ m (u, t - y₀)) x₀ + _ = m / (σ * Real.sqrt (2 * π)) * Real.exp (-(t - y₀) ^ 2 / (2 * σ ^ 2)) := + gaussian_line_integral_at_distance σ m (t - y₀) hσ hm + +theorem on_line_contribution + (σ m x₀ : ℝ) (hσ : σ > 0) (hm : m ≥ 0) : + (∫ τ : ℝ, gaussian2D σ m (τ - x₀, 0)) = + m / (σ * Real.sqrt (2 * π)) := by + calc + (∫ τ : ℝ, gaussian2D σ m (τ - x₀, 0)) + = (∫ u : ℝ, gaussian2D σ m (u, 0)) := + integral_comp_add_right_ℝ (fun u : ℝ => gaussian2D σ m (u, 0)) x₀ + _ = m / (σ * Real.sqrt (2 * π)) * Real.exp (-(0 : ℝ) ^ 2 / (2 * σ ^ 2)) := + gaussian_line_integral_at_distance σ m 0 hσ hm + _ = m / (σ * Real.sqrt (2 * π)) := by norm_num + +-- ═══════════════════════════════════════════════════════════════════════════ +-- §2 PENALTY AND ENERGY +-- ═══════════════════════════════════════════════════════════════════════════ + +theorem penalty_nonneg {lam : ℝ} (hlam : lam ≥ 0) (z : ℝ) : penalty lam z ≥ 0 := by + unfold penalty; split_ifs + · exact mul_nonneg hlam (sq_nonneg z) + · exact le_refl 0 + +theorem penalty_zero_iff {lam : ℝ} (hlam : lam > 0) (z : ℝ) : penalty lam z = 0 ↔ z ≤ 0 := by + unfold penalty; constructor + · intro h; by_contra hz; push_neg at hz + rw [if_pos hz] at h + have : lam * z ^ 2 > 0 := mul_pos hlam (sq_pos_of_pos hz) + linarith + · intro h; rw [if_neg (not_lt.mpr h)] + +theorem energy_zero_iff {ι : Type*} [Fintype ι] [DecidableEq ι] + {lam : ℝ} (hlam : lam > 0) (densities : ι → ℝ) : + energy lam densities = 0 ↔ ∀ j, densities j ≤ 2 := by + unfold energy + constructor + · intro hE j + have hterm := (sum_eq_zero_iff_of_nonneg + (fun i hi => penalty_nonneg (le_of_lt hlam) (densities i - 2))).mp hE j (Finset.mem_univ j) + rw [penalty_zero_iff hlam (densities j - 2)] at hterm + exact sub_nonpos.mp hterm + · intro hle; apply Finset.sum_eq_zero + intro j _; exact (penalty_zero_iff hlam (densities j - 2)).mpr (sub_nonpos.mpr (hle j)) + +theorem energy_nonneg {ι : Type*} [Fintype ι] [DecidableEq ι] + {lam : ℝ} (hlam : lam ≥ 0) (densities : ι → ℝ) : energy lam densities ≥ 0 := + Finset.sum_nonneg (fun i _ => penalty_nonneg hlam (densities i - 2)) + +theorem energy_pos_of_exceeds {ι : Type*} [Fintype ι] [DecidableEq ι] + {lam : ℝ} (hlam : lam > 0) {densities : ι → ℝ} {j : ι} (hj : densities j > 2) : + energy lam densities > 0 := by + have hterm : penalty lam (densities j - 2) > 0 := by + by_contra! hle + have hzero : penalty lam (densities j - 2) = 0 := + le_antisymm hle (penalty_nonneg (le_of_lt hlam) (densities j - 2)) + have hdens : densities j - 2 ≤ 0 := ((penalty_zero_iff hlam (densities j - 2)).mp hzero) + linarith + by_contra hE + have hE_nonpos : energy lam densities ≤ 0 := le_of_not_gt hE + have h_total_nonneg : energy lam densities ≥ 0 := energy_nonneg (le_of_lt hlam) densities + have hE_zero : energy lam densities = 0 := le_antisymm hE_nonpos h_total_nonneg + have hall : ∀ k, densities k ≤ 2 := (energy_zero_iff hlam densities).mp hE_zero + linarith [hall j, hj] + +-- ═══════════════════════════════════════════════════════════════════════════ +-- §3 THRESHOLD INEQUALITY +-- ═══════════════════════════════════════════════════════════════════════════ + +theorem σ_crit_pos : σ_crit > 0 := by + unfold σ_crit; positivity + +theorem three_over_sroot2pi_gt_two + {σ : ℝ} (hσ : σ > 0) (hbound : σ < σ_crit) : + 3 / (σ * Real.sqrt (2 * π)) > 2 := by + unfold σ_crit at hbound + have hs2pi_pos : Real.sqrt (2 * π) > 0 := by positivity + have hpos : σ * Real.sqrt (2 * π) > 0 := mul_pos hσ hs2pi_pos + have hineq : 2 * (σ * Real.sqrt (2 * π)) < 3 := by + have hpos2 : (2 : ℝ) * Real.sqrt (2 * π) > 0 := mul_pos (by norm_num) hs2pi_pos + calc + 2 * (σ * Real.sqrt (2 * π)) = (2 * Real.sqrt (2 * π)) * σ := by ring + _ < (2 * Real.sqrt (2 * π)) * (3 / (2 * Real.sqrt (2 * π))) := + mul_lt_mul_of_pos_left hbound hpos2 + _ = 3 := by field_simp [hs2pi_pos.ne.symm] + exact ((lt_div_iff₀ hpos).mpr hineq) + +-- ═══════════════════════════════════════════════════════════════════════════ +-- §4 INFINITE-LINE DENSITY +-- ═══════════════════════════════════════════════════════════════════════════ + +lemma peak_integrable_over_R (σ : ℝ) (hσ : σ > 0) (m : ℝ) + (a b s t x₀ y₀ : ℝ) : + Integrable (fun τ : ℝ => + gaussian2D σ m (s + a * τ - x₀, t + b * τ - y₀)) := by + sorry + +theorem ansatzLineDensity_decomp (σ : ℝ) (hσ : σ > 0) + {k : ℕ} (positions : Fin k → ℝ × ℝ) (masses : Fin k → ℝ) + (hm : ∀ i, masses i ≥ 0) (a b s t : ℝ) : + ansatzLineDensity σ positions masses a b s t = + (Finset.univ : Finset (Fin k)).sum (fun i => + ∫ τ : ℝ, gaussian2D σ (masses i) + (s + a * τ - (positions i).1, t + b * τ - (positions i).2)) := by + unfold ansatzLineDensity gaussianAnsatz_eval + rw [integral_finset_sum] + intro i _ + exact (peak_integrable_over_R σ hσ (masses i) a b s t + (positions i).1 (positions i).2) + +theorem peak_contribution_nonneg + (σ m x₀ y₀ s t a b : ℝ) (hσ : σ > 0) (hm : m ≥ 0) : + (∫ τ : ℝ, gaussian2D σ m (s + a * τ - x₀, t + b * τ - y₀)) ≥ 0 := by + apply integral_nonneg; intro τ; unfold gaussian2D; positivity + +-- ═══════════════════════════════════════════════════════════════════════════ +-- §5 COLLINEARITY → UNIT DIRECTION +-- ═══════════════════════════════════════════════════════════════════════════ + +theorem signedArea_zero_implies_perpDist_zero + {k : ℕ} (positions : Fin k → ℝ × ℝ) + {i j m : Fin k} (hij : i ≠ j) (him : i ≠ m) (hjm : j ≠ m) + (halign : signedArea (positions i) (positions j) (positions m) = 0) : + ∃ (a b : ℝ), a ^ 2 + b ^ 2 = 1 ∧ + perpDistance (positions j).1 (positions j).2 a b + (positions i).1 (positions i).2 = 0 ∧ + perpDistance (positions m).1 (positions m).2 a b + (positions i).1 (positions i).2 = 0 := by + sorry + +-- ═══════════════════════════════════════════════════════════════════════════ +-- §6 COLLISION THEOREM — HORIZONTAL LINE CASE +-- ═══════════════════════════════════════════════════════════════════════════ + +lemma integrand_simp (x : ℝ) (τ : ℝ) : 0 + 1 * τ - x = τ - x := by ring +lemma integrand_simp2 (y₀ : ℝ) : y₀ + 0 * τ - y₀ = 0 := by ring + +theorem collinear_line_density_exceeds_two + {σ : ℝ} (hσ : σ > 0) (hσ_bound : σ < σ_crit) + {k : ℕ} (hk : k ≥ 3) + (positions : Fin k → ℝ × ℝ) (masses : Fin k → ℝ) + (hmass : ∀ i, masses i ≥ 1) + (y₀ : ℝ) + {i j m : Fin k} (hij : i ≠ j) (him : i ≠ m) (hjm : j ≠ m) + (hi : (positions i).2 = y₀) + (hj : (positions j).2 = y₀) + (hm_pos : (positions m).2 = y₀) : + ansatzLineDensity σ positions masses 1 0 0 y₀ > 2 := by + let Λ := ansatzLineDensity σ positions masses 1 0 0 y₀ + have hmass_nn : ∀ l, masses l ≥ 0 := + fun l => le_trans (by norm_num : (0 : ℝ) ≤ 1) (hmass l) + have hdecomp := ansatzLineDensity_decomp σ hσ positions masses hmass_nn 1 0 0 y₀ + have hnonneg : ∀ l : Fin k, + (∫ τ : ℝ, gaussian2D σ (masses l) + (0 + 1 * τ - (positions l).1, y₀ - (positions l).2)) ≥ 0 := by + intro l + have h := peak_contribution_nonneg σ (masses l) (positions l).1 (positions l).2 + 0 y₀ 1 0 hσ (hmass_nn l) + simpa using h + have h_on_i : + (∫ τ : ℝ, gaussian2D σ (masses i) + (0 + 1 * τ - (positions i).1, y₀ - (positions i).2)) = + masses i / (σ * Real.sqrt (2 * π)) := by + calc + (∫ τ : ℝ, gaussian2D σ (masses i) (0 + 1 * τ - (positions i).1, y₀ - (positions i).2)) + = (∫ τ : ℝ, gaussian2D σ (masses i) (τ - (positions i).1, 0)) := by + refine integral_congr_ae ?_ + filter_upwards with τ; simp [hi, integrand_simp] + _ = masses i / (σ * Real.sqrt (2 * π)) := + on_line_contribution σ (masses i) (positions i).1 hσ (hmass_nn i) + have h_on_j : + (∫ τ : ℝ, gaussian2D σ (masses j) + (0 + 1 * τ - (positions j).1, y₀ - (positions j).2)) = + masses j / (σ * Real.sqrt (2 * π)) := by + calc + (∫ τ : ℝ, gaussian2D σ (masses j) (0 + 1 * τ - (positions j).1, y₀ - (positions j).2)) + = (∫ τ : ℝ, gaussian2D σ (masses j) (τ - (positions j).1, 0)) := by + refine integral_congr_ae ?_ + filter_upwards with τ; simp [hj, integrand_simp] + _ = masses j / (σ * Real.sqrt (2 * π)) := + on_line_contribution σ (masses j) (positions j).1 hσ (hmass_nn j) + have h_on_m : + (∫ τ : ℝ, gaussian2D σ (masses m) + (0 + 1 * τ - (positions m).1, y₀ - (positions m).2)) = + masses m / (σ * Real.sqrt (2 * π)) := by + calc + (∫ τ : ℝ, gaussian2D σ (masses m) (0 + 1 * τ - (positions m).1, y₀ - (positions m).2)) + = (∫ τ : ℝ, gaussian2D σ (masses m) (τ - (positions m).1, 0)) := by + refine integral_congr_ae ?_ + filter_upwards with τ; simp [hm_pos, integrand_simp] + _ = masses m / (σ * Real.sqrt (2 * π)) := + on_line_contribution σ (masses m) (positions m).1 hσ (hmass_nn m) + rw [hdecomp] + have hs2pi_pos : Real.sqrt (2 * π) > 0 := by positivity + have hσs2pi_pos : σ * Real.sqrt (2 * π) > 0 := mul_pos hσ hs2pi_pos + have hsum_ge_three : + (Finset.univ : Finset (Fin k)).sum (fun l => + ∫ τ : ℝ, gaussian2D σ (masses l) + (1 * τ - (positions l).1, y₀ - (positions l).2)) ≥ + 3 / (σ * Real.sqrt (2 * π)) := by + have hsubset : ({i, j, m} : Finset (Fin k)) ⊆ Finset.univ := Finset.subset_univ _ + have hnonneg_subset : ∀ l, (∫ τ : ℝ, gaussian2D σ (masses l) + (1 * τ - (positions l).1, y₀ - (positions l).2)) ≥ 0 := by + intro l; simpa using hnonneg l + have hsubset_sum : (({i, j, m} : Finset (Fin k)).sum (fun l => + ∫ τ : ℝ, gaussian2D σ (masses l) + (1 * τ - (positions l).1, y₀ - (positions l).2))) ≤ + (Finset.univ : Finset (Fin k)).sum (fun l => + ∫ τ : ℝ, gaussian2D σ (masses l) + (1 * τ - (positions l).1, y₀ - (positions l).2)) := + Finset.sum_le_sum_of_subset_of_nonneg hsubset (fun l _ _ => hnonneg_subset l) + have h_conv_int : ∀ l, (positions l).2 = y₀ → + (∫ τ : ℝ, gaussian2D σ (masses l) (1 * τ - (positions l).1, y₀ - (positions l).2)) = + (∫ τ : ℝ, gaussian2D σ (masses l) (τ - (positions l).1, 0)) := by + intro l hl + refine integral_congr_ae ?_ + filter_upwards with τ; simp [hl, sub_self] + have h3 : (({i, j, m} : Finset (Fin k)).sum (fun l => + ∫ τ : ℝ, gaussian2D σ (masses l) + (1 * τ - (positions l).1, y₀ - (positions l).2))) ≥ + 3 / (σ * Real.sqrt (2 * π)) := by + have hi_notin : i ∉ ({j, m} : Finset (Fin k)) := by + intro hi + have hi_mem_m : i ∈ ({m} : Finset (Fin k)) := + (Finset.mem_insert.mp hi).resolve_left hij + exact him (Finset.mem_singleton.mp hi_mem_m) + have hj_notin : j ∉ ({m} : Finset (Fin k)) := by + intro hj; exact hjm (Finset.mem_singleton.mp hj) + calc + (({i, j, m} : Finset (Fin k)).sum (fun l => + ∫ τ : ℝ, gaussian2D σ (masses l) + (1 * τ - (positions l).1, y₀ - (positions l).2))) + = (({i, j, m} : Finset (Fin k)).sum (fun l => + ∫ τ : ℝ, gaussian2D σ (masses l) (τ - (positions l).1, 0))) := by + refine Finset.sum_congr rfl fun l hl => ?_ + have hl_out : l = i ∨ l = j ∨ l = m := by + simpa [Finset.mem_insert, Finset.mem_singleton] using hl + rcases hl_out with (hl_i|hl_j|hl_m) + · rw [hl_i]; exact h_conv_int i hi + · rw [hl_j]; exact h_conv_int j hj + · rw [hl_m]; exact h_conv_int m hm_pos + _ = (∫ τ : ℝ, gaussian2D σ (masses i) (τ - (positions i).1, 0)) + + ((∫ τ : ℝ, gaussian2D σ (masses j) (τ - (positions j).1, 0)) + + (∫ τ : ℝ, gaussian2D σ (masses m) (τ - (positions m).1, 0))) := by + rw [Finset.sum_insert hi_notin, Finset.sum_insert hj_notin, Finset.sum_singleton] + _ = (masses i + masses j + masses m) / (σ * Real.sqrt (2 * π)) := by + rw [on_line_contribution σ (masses i) (positions i).1 hσ (hmass_nn i), + on_line_contribution σ (masses j) (positions j).1 hσ (hmass_nn j), + on_line_contribution σ (masses m) (positions m).1 hσ (hmass_nn m)] + field_simp [hσs2pi_pos.ne.symm] + ring + _ ≥ (1 + 1 + 1) / (σ * Real.sqrt (2 * π)) := by + have hm_i : masses i ≥ 1 := hmass i + have hm_j : masses j ≥ 1 := hmass j + have hm_m : masses m ≥ 1 := hmass m + refine (div_le_div_of_nonneg_right ?_ (le_of_lt hσs2pi_pos)) + linarith + _ = 3 / (σ * Real.sqrt (2 * π)) := by norm_num + linarith + have hthree_gt_two := three_over_sroot2pi_gt_two hσ hσ_bound + -- Now we need to relate the sum in the target to hsum_ge_three + -- The target (after rw [hdecomp]) is: + -- Σᵢ ∫ g2D(0+1*τ - ..., y₀+0*τ - ...) > 2 + -- But hsum_ge_three is about: + -- Σᵢ ∫ g2D(1*τ - ..., y₀ - ...) ≥ 3/(σ√(2π)) + -- These sums are equal by integral_congr_ae. + have h_sums_eq : (Finset.univ : Finset (Fin k)).sum (fun l => + ∫ τ : ℝ, gaussian2D σ (masses l) (0 + 1 * τ - (positions l).1, y₀ + 0 * τ - (positions l).2)) = + (Finset.univ : Finset (Fin k)).sum (fun l => + ∫ τ : ℝ, gaussian2D σ (masses l) (1 * τ - (positions l).1, y₀ - (positions l).2)) := by + refine Finset.sum_congr rfl fun l hl => ?_ + refine integral_congr_ae ?_ + filter_upwards with τ; simp + rw [h_sums_eq] + linarith + +-- ═══════════════════════════════════════════════════════════════════════════ +-- §7 GENERAL LINE DIRECTION (sketch) +-- ═══════════════════════════════════════════════════════════════════════════ + +theorem gaussian_line_integral_unit_dir + (σ m a b s t x₀ y₀ : ℝ) (hσ : σ > 0) (hm : m ≥ 0) + (hab : a ^ 2 + b ^ 2 = 1) : + (∫ τ : ℝ, gaussian2D σ m (s + a * τ - x₀, t + b * τ - y₀)) = + m / (σ * Real.sqrt (2 * π)) * + Real.exp (-(perpDistance x₀ y₀ a b s t) ^ 2 / (2 * σ ^ 2)) := by + sorry + +theorem on_line_contribution_general + (σ m a b s t x₀ y₀ : ℝ) (hσ : σ > 0) (hm : m ≥ 0) + (hab : a ^ 2 + b ^ 2 = 1) + (hon : perpDistance x₀ y₀ a b s t = 0) : + (∫ τ : ℝ, gaussian2D σ m (s + a * τ - x₀, t + b * τ - y₀)) = + m / (σ * Real.sqrt (2 * π)) := by + rw [gaussian_line_integral_unit_dir σ m a b s t x₀ y₀ hσ hm hab, hon] + simp + +-- ═══════════════════════════════════════════════════════════════════════════ +-- §8 COLLISION THEOREM — GENERAL DIRECTION +-- ═══════════════════════════════════════════════════════════════════════════ + +theorem collinear_line_density_exceeds_two_general + {σ : ℝ} (hσ : σ > 0) (hσ_bound : σ < σ_crit) + {k : ℕ} (hk : k ≥ 3) + (positions : Fin k → ℝ × ℝ) (masses : Fin k → ℝ) + (hmass : ∀ i, masses i ≥ 1) + {i j m : Fin k} (hij : i ≠ j) (him : i ≠ m) (hjm : j ≠ m) + (halign : signedArea (positions i) (positions j) (positions m) = 0) : + ∃ (a b : ℝ) (_hab : a ^ 2 + b ^ 2 = 1), + ansatzLineDensity σ positions masses a b + (positions i).1 (positions i).2 > 2 := by + obtain ⟨a, b, hab, hperp_j, hperp_m⟩ := + signedArea_zero_implies_perpDist_zero positions hij him hjm halign + use a, b, hab + have hmass_nn : ∀ l, masses l ≥ 0 := + fun l => le_trans (by norm_num : (0 : ℝ) ≤ 1) (hmass l) + have hdecomp := ansatzLineDensity_decomp σ hσ positions masses hmass_nn + a b (positions i).1 (positions i).2 + rw [hdecomp] + have hnonneg : ∀ l : Fin k, + (∫ τ : ℝ, gaussian2D σ (masses l) + ((positions i).1 + a * τ - (positions l).1, + (positions i).2 + b * τ - (positions l).2)) ≥ 0 := by + intro l; exact peak_contribution_nonneg σ (masses l) (positions l).1 (positions l).2 + (positions i).1 (positions i).2 a b hσ (hmass_nn l) + have hperp_i : perpDistance (positions i).1 (positions i).2 a b + (positions i).1 (positions i).2 = 0 := by + unfold perpDistance; simp + have hs2pi_pos : Real.sqrt (2 * π) > 0 := by positivity + have hσs2pi_pos : σ * Real.sqrt (2 * π) > 0 := mul_pos hσ hs2pi_pos + have h3 : (({i, j, m} : Finset (Fin k)).sum (fun l => + ∫ τ : ℝ, gaussian2D σ (masses l) + ((positions i).1 + a * τ - (positions l).1, + (positions i).2 + b * τ - (positions l).2))) ≥ + 3 / (σ * Real.sqrt (2 * π)) := by + calc + (({i, j, m} : Finset (Fin k)).sum (fun l => + ∫ τ : ℝ, gaussian2D σ (masses l) + ((positions i).1 + a * τ - (positions l).1, + (positions i).2 + b * τ - (positions l).2))) + = (∫ τ : ℝ, gaussian2D σ (masses i) + ((positions i).1 + a * τ - (positions i).1, + (positions i).2 + b * τ - (positions i).2)) + + ((∫ τ : ℝ, gaussian2D σ (masses j) + ((positions i).1 + a * τ - (positions j).1, + (positions i).2 + b * τ - (positions j).2)) + + (∫ τ : ℝ, gaussian2D σ (masses m) + ((positions i).1 + a * τ - (positions m).1, + (positions i).2 + b * τ - (positions m).2))) := by + simp [hij, him, hjm, Finset.sum_insert, Finset.sum_singleton] + _ = (masses i / (σ * Real.sqrt (2 * π)) + + masses j / (σ * Real.sqrt (2 * π)) + + masses m / (σ * Real.sqrt (2 * π))) := by + -- need on_line_contribution_general for i,j,m + -- For i: positions (i) coincide, so perpDist = 0 by hperp_i + -- For j: perpDist = 0 by hperp_j + -- For m: perpDist = 0 by hperp_m + sorry + _ = (masses i + masses j + masses m) / (σ * Real.sqrt (2 * π)) := by ring + _ ≥ (1 + 1 + 1) / (σ * Real.sqrt (2 * π)) := by + have hm_i : masses i ≥ 1 := hmass i + have hm_j : masses j ≥ 1 := hmass j + have hm_m : masses m ≥ 1 := hmass m + refine (div_le_div_of_nonneg_right ?_ (le_of_lt hσs2pi_pos)) + linarith + _ = 3 / (σ * Real.sqrt (2 * π)) := by norm_num + have hsum_ge_three : (Finset.univ : Finset (Fin k)).sum (fun l => + ∫ τ : ℝ, gaussian2D σ (masses l) + ((positions i).1 + a * τ - (positions l).1, + (positions i).2 + b * τ - (positions l).2)) ≥ + 3 / (σ * Real.sqrt (2 * π)) := by + have hsubset_sum : (({i, j, m} : Finset (Fin k)).sum (fun l => + ∫ τ : ℝ, gaussian2D σ (masses l) + ((positions i).1 + a * τ - (positions l).1, + (positions i).2 + b * τ - (positions l).2))) ≤ + (Finset.univ : Finset (Fin k)).sum (fun l => + ∫ τ : ℝ, gaussian2D σ (masses l) + ((positions i).1 + a * τ - (positions l).1, + (positions i).2 + b * τ - (positions l).2)) := + Finset.sum_le_sum_of_subset_of_nonneg (Finset.subset_univ _) (fun l _ _ => hnonneg l) + linarith + have hthree := three_over_sroot2pi_gt_two hσ hσ_bound + linarith + +-- ═══════════════════════════════════════════════════════════════════════════ +-- §9 MAIN THEOREM +-- ═══════════════════════════════════════════════════════════════════════════ + +theorem no_collinear_at_zero_energy + {σ : ℝ} (hσ : σ > 0) (hσ_bound : σ < σ_crit) + {lam : ℝ} (hlam : lam > 0) + {k : ℕ} (hk : k ≥ 3) + (positions : Fin k → ℝ × ℝ) (masses : Fin k → ℝ) + (hmass : ∀ i, masses i ≥ 1) + {ι : Type*} [Fintype ι] [DecidableEq ι] + (densities : ι → ℝ) (hE : energy lam densities = 0) : + ∀ i j m : Fin k, i ≠ j → i ≠ m → j ≠ m → + signedArea (positions i) (positions j) (positions m) = 0 → False := by + intro i j m hij him hjm halign + sorry + +end Semantics.N3L_Energy