continuous_no_isolated_zero_defect

proof body

Tactic-mode proof.

 329  intro x hx_pos hx ε hε
 330  -- Since defect = 0 implies x = 1, we work at x = 1
 331  have hx_eq_1 : x = 1 := (defect_zero_iff_one hx_pos).mp hx
 332  subst hx_eq_1
 333  -- Take z = 1 + min(ε/2, 1/2) to ensure z > 0 and close to 1
 334  let t := min (ε / 2) (1 / 2 : ℝ)
 335  have ht_pos : t > 0 := by positivity
 336  have ht_le_half : t ≤ 1 / 2 := min_le_right _ _
 337  use 1 + t
 338  constructor
 339  · linarith
 340  constructor
 341  · simp only [add_sub_cancel_left, abs_of_pos ht_pos]
 342    calc t ≤ ε / 2 := min_le_left _ _
 343      _ < ε := by linarith
 344  · -- defect(1 + t) = J(1 + t) = t²/(2(1+t)) for small t > 0
 345    -- For t ≤ min(ε/2, 1/2), we show this is less than ε
 346    simp only [defect, J]
 347    have ht_pos' : 1 + t > 0 := by linarith
 348    have hne : 1 + t ≠ 0 := ht_pos'.ne'
 349    -- Compute J(1+t) = ((1+t) + (1+t)⁻¹)/2 - 1 = t²/(2(1+t))
 350    have key : (1 + t + (1 + t)⁻¹) / 2 - 1 = t^2 / (2 * (1 + t)) := by
 351      field_simp
 352      ring
 353    rw [key]
 354    -- Now show t²/(2(1+t)) < ε
 355    have h1t_ge1 : 1 + t ≥ 1 := by linarith
 356    have h2 : 2 * (1 + t) ≥ 2 := by linarith
 357    have h3 : t^2 / (2 * (1 + t)) ≤ t^2 / 2 := by
 358      apply div_le_div_of_nonneg_left (sq_nonneg t) (by positivity)
 359      exact h2
 360    have ht_le_half : t ≤ 1/2 := ht_le_half
 361    have ht_le_eps2 : t ≤ ε / 2 := min_le_left _ _
 362    -- Case split: ε ≤ 1 vs ε > 1
 363    by_cases hε_le1 : ε ≤ 1
 364    · -- For ε ≤ 1, t ≤ ε/2, so t²/2 ≤ (ε/2)²/2 = ε²/8 < ε
 365      calc t^2 / (2 * (1 + t)) ≤ t^2 / 2 := h3
 366        _ ≤ (ε/2)^2 / 2 := by
 367          apply div_le_div_of_nonneg_right _ (by positivity)
 368          apply sq_le_sq'
 369          · linarith
 370          · exact ht_le_eps2
 371        _ = ε^2 / 8 := by ring
 372        _ < ε := by nlinarith
 373    · -- For ε > 1, t ≤ 1/2, so t²/2 ≤ 1/8 < 1 < ε
 374      push_neg at hε_le1
 375      calc t^2 / (2 * (1 + t)) ≤ t^2 / 2 := h3
 376        _ ≤ (1/2)^2 / 2 := by
 377          apply div_le_div_of_nonneg_right _ (by positivity)
 378          apply sq_le_sq'
 379          · linarith
 380          · exact ht_le_half
 381        _ = 1/8 := by norm_num
 382        _ < ε := by linarith
 383
 384/-- **Key Theorem**: In a continuous configuration space, no point is strictly isolated.
 385
 386    If defect(x) = 0 (x exists), then for any ε > 0, there exist points arbitrarily
 387    close to x with defect arbitrarily small. This means x cannot be "locked in" —
 388    there's always a low-cost escape route.
 389
 390    This is why continuous spaces don't support stable existence. -/