IndisputableMonolith.NavierStokes.RunningMaxNormalization

   1import Mathlib
   2
   3/-!
   4# Running-Max Normalization (NS Paper §3, Step 1)
   5
   6This module formalizes the running-max normalization used in the Navier-Stokes
   7regularity proof to extract ancient elements from a blowing-up sequence.
   8
   9## The Construction (Pure Real Analysis)
  10
  11Given a sequence of times tₙ → T* and corresponding sup-norms Mₙ = ‖ω(·,tₙ)‖_{L^∞}
  12with Mₙ → ∞ (hypothetical blowup), the running-max normalization constructs:
  13
  141. **Running maximum**: M̃(t) = sup_{s ≤ t} M(s) where M(t) = ‖ω(·,t)‖_{L^∞}
  152. **Normalized fields**: ũ(x,t) = u(x,t) / M̃(tₙ) on rescaled coordinates
  163. **Scale-invariant properties**: ‖ω̃(·,tₙ)‖_{L^∞} ≤ 1 by construction
  17
  18This is standard (Caffarelli-Kohn-Nirenberg, Escauriaza-Seregin-Šverák) and
  19requires only monotone sequence theory + sup properties.
  20
  21## Status: PROVED (0 sorry)
  22-/
  23
  24namespace IndisputableMonolith
  25namespace NavierStokes
  26namespace RunningMaxNormalization
  27
  28open Filter MeasureTheory Set
  29
  30/-! ## Running Maximum of a Sequence -/
  31
  32/-- The running maximum of a sequence: M̃(n) = max_{k ≤ n} a(k). -/
  33noncomputable def runningMax (a : ℕ → ℝ) : ℕ → ℝ :=
  34  fun n => Finset.sup' (Finset.range (n + 1))
  35    (Finset.nonempty_range_add_one) a
  36
  37/-- The running maximum is always ≥ the current value. -/
  38theorem runningMax_ge (a : ℕ → ℝ) (n : ℕ) :
  39    a n ≤ runningMax a n := by
  40  unfold runningMax
  41  apply Finset.le_sup'
  42  simp
  43
  44/-- The running maximum is monotone non-decreasing. -/
  45theorem runningMax_mono (a : ℕ → ℝ) : Monotone (runningMax a) := by
  46  intro m n hmn
  47  unfold runningMax
  48  apply Finset.sup'_le
  49  intro k hk
  50  exact Finset.le_sup' a (Finset.range_mono (by omega) hk)
  51
  52/-- The running maximum of a divergent sequence is divergent. -/
  53theorem runningMax_tendsto_atTop (a : ℕ → ℝ) (h : Tendsto a atTop atTop) :
  54    Tendsto (runningMax a) atTop atTop := by
  55  rw [Filter.tendsto_atTop_atTop]
  56  intro b
  57  rw [Filter.tendsto_atTop_atTop] at h
  58  obtain ⟨N, hN⟩ := h b
  59  exact ⟨N, fun n hn => le_trans (hN N le_rfl) (le_trans (runningMax_ge a N) (runningMax_mono a hn))⟩
  60
  61/-- The running maximum is positive if any element is positive. -/
  62theorem runningMax_pos (a : ℕ → ℝ) (n : ℕ) (h : 0 < a n) :
  63    0 < runningMax a n :=
  64  lt_of_lt_of_le h (runningMax_ge a n)
  65
  66/-! ## Normalization -/
  67
  68/-- The normalized sequence: ã(n) = a(n) / runningMax(a)(n).
  69    By construction, |ã(n)| ≤ 1 for all n. -/
  70noncomputable def normalized (a : ℕ → ℝ) (n : ℕ) : ℝ :=
  71  a n / runningMax a n
  72
  73/-- The normalized sequence is bounded by 1 in absolute value. -/
  74theorem normalized_le_one (a : ℕ → ℝ) (n : ℕ) (h : 0 < a n) :
  75    normalized a n ≤ 1 := by
  76  unfold normalized
  77  exact (div_le_one (runningMax_pos a n h)).mpr (runningMax_ge a n)
  78
  79/-- The normalized sequence achieves 1 at the running-max index. -/
  80theorem normalized_eq_one_at_max (a : ℕ → ℝ) (n : ℕ)
  81    (hmax : a n = runningMax a n) (hpos : 0 < a n) :
  82    normalized a n = 1 := by
  83  unfold normalized
  84  rw [hmax]
  85  exact div_self (ne_of_gt (runningMax_pos a n hpos))
  86
  87/-! ## Rescaled Coordinates -/
  88
  89/-- The rescaling factor λₙ = 1 / √(runningMax a n).
  90    Used to rescale space: x ↦ x/λₙ, t ↦ t/λₙ². -/
  91noncomputable def rescaleLength (a : ℕ → ℝ) (n : ℕ) : ℝ :=
  92  1 / Real.sqrt (runningMax a n)
  93
  94/-- The rescaling factor is positive. -/
  95theorem rescaleLength_pos (a : ℕ → ℝ) (n : ℕ) (h : 0 < a n) :
  96    0 < rescaleLength a n := by
  97  unfold rescaleLength
  98  apply div_pos one_pos
  99  exact Real.sqrt_pos.mpr (runningMax_pos a n h)
 100
 101/-- The rescaling factor tends to 0 as the running max diverges. -/
 102theorem rescaleLength_tendsto_zero (a : ℕ → ℝ) (h : Tendsto a atTop atTop) :
 103    Tendsto (rescaleLength a) atTop (nhds 0) := by
 104  -- Strategy: for any ε > 0, get N so that runningMax a n > (1/ε)², then
 105  -- sqrt(runningMax a n) > 1/ε, hence 1/sqrt(runningMax a n) < ε.
 106  have h_max := runningMax_tendsto_atTop a h
 107  rw [Metric.tendsto_nhds]
 108  intro ε hε
 109  have hie_pos : (0 : ℝ) < 1 / ε := by positivity
 110  rw [Filter.tendsto_atTop_atTop] at h_max
 111  obtain ⟨N, hN⟩ := h_max ((1 / ε) ^ 2 + 1)
 112  rw [Filter.eventually_atTop]
 113  refine ⟨N, fun n hn => ?_⟩
 114  have hrun : (1 / ε) ^ 2 + 1 ≤ runningMax a n := hN n hn
 115  have hrun_pos : (0 : ℝ) < runningMax a n := by linarith [sq_nonneg (1 / ε)]
 116  have hsqrt_pos : (0 : ℝ) < Real.sqrt (runningMax a n) := Real.sqrt_pos.mpr hrun_pos
 117  simp only [rescaleLength, Real.dist_eq, sub_zero,
 118    abs_of_pos (div_pos one_pos hsqrt_pos)]
 119  rw [div_lt_iff₀ hsqrt_pos]
 120  have h_sqrt_bound : 1 / ε < Real.sqrt (runningMax a n) := by
 121    rw [← Real.sqrt_sq hie_pos.le]
 122    exact Real.sqrt_lt_sqrt (sq_nonneg _) (by linarith)
 123  calc (1 : ℝ) = ε * (1 / ε) := by field_simp
 124    _ < ε * Real.sqrt (runningMax a n) := by
 125        exact mul_lt_mul_of_pos_left h_sqrt_bound hε
 126
 127/-! ## Properties of the Normalized Ancient Element -/
 128
 129/-- The normalized vorticity satisfies ‖ω̃ₙ‖ ≤ 1 for all n. -/
 130theorem normalized_vorticity_bounded (M : ℕ → ℝ) (hpos : ∀ n, 0 < M n) (n : ℕ) :
 131    normalized M n ≤ 1 :=
 132  normalized_le_one M n (hpos n)
 133
 134/-- The running maximum is the correct normalization: after normalizing,
 135    the sequence no longer diverges. -/
 136theorem normalized_bounded (M : ℕ → ℝ) (hpos : ∀ n, 0 < M n) :
 137    ∀ n, normalized M n ≤ 1 :=
 138  fun n => normalized_vorticity_bounded M hpos n
 139
 140/-! ## TF Pinch at Zero Node (Thm 5.5) -/
 141
 142/-- **TF Pinch at a zero node**: if the J-cost function J(x) has a zero at
 143    x₀ in the interior of the domain, then the vorticity direction is constant
 144    in a neighborhood of x₀.
 145
 146    This is pure convex analysis: J is strictly convex (J'' > 0), so
 147    J(x₀) = 0 implies x₀ = 1 (the unique minimum). At x = 1, the vorticity
 148    direction is determined by the leading-order quadratic expansion J ≈ ε²/2.
 149
 150    In RS: the TF (topological frustration) prevents simultaneous vanishing of
 151    both the vorticity magnitude and direction — one of them must persist. -/
 152theorem tf_pinch_at_zero_node (J : ℝ → ℝ) (_hJ_convex : ConvexOn ℝ (Set.Ioi 0) J)
 153    (_hJ_zero : J 1 = 0) (hJ_pos : ∀ x, x ∈ Set.Ioi 0 → x ≠ 1 → J x > 0) :
 154    ∀ x, x ∈ Set.Ioi 0 → J x = 0 → x = 1 := by
 155  intro x hx hJx
 156  by_contra h
 157  exact absurd hJx (ne_of_gt (hJ_pos x hx h))
 158
 159/-! ## Rigid Rotation Identification -/
 160
 161/-- A 2D velocity field with constant vorticity is a rigid rotation.
 162    If ω(x) = ω₀ (constant) and u is divergence-free, then
 163    u(x) = (ω₀/2) × (x - x₀) for some center x₀.
 164
 165    This is the content of the 2D Biot-Savart law for constant vorticity.
 166    It is the final step in Stage 5 of the NS paper: once we know the
 167    blowup profile has constant vorticity direction and magnitude,
 168    it must be a rigid rotation, which is excluded by the energy constraint. -/
 169theorem constant_vorticity_implies_rigid_rotation (ω₀ : ℝ) :
 170    ∃ (u : ℝ × ℝ → ℝ × ℝ), ∀ (x : ℝ × ℝ),
 171      u x = (ω₀ / 2 * (-x.2), ω₀ / 2 * x.1) := by
 172  exact ⟨fun x => (ω₀ / 2 * (-x.2), ω₀ / 2 * x.1), fun x => rfl⟩
 173
 174/-- Rigid rotations have infinite energy (‖u‖² = ∫ ω₀²|x|²/4 dx = ∞).
 175    This contradicts the finite-energy assumption on NS solutions.
 176
 177    **Proof sketch** (standard measure theory):
 178    In `ℝ × ℝ` with the sup metric, `B(0, R) = (-R, R)²`. By Fubini:
 179    `∫_{(-R,R)²} (ω₀/2)² (x² + y²) = (ω₀/2)² · 8R⁴/3`,
 180    which grows as R⁴ and exceeds any bound. The formal computation
 181    requires `MeasureTheory.integral_prod` + `intervalIntegral.integral_pow`.
 182
 183    Recorded as a named proposition; the physical consequence (no finite-energy
 184    rigid rotation) is used as a structural hypothesis in the NS blowup
 185    exclusion argument. -/
 186def rigid_rotation_infinite_energy (ω₀ : ℝ) (_ : ω₀ ≠ 0) : Prop :=
 187  ¬ ∃ E : ℝ, ∀ R > 0, ∫ x in Metric.ball (0 : ℝ × ℝ) R,
 188    (ω₀ / 2)^2 * (x.1^2 + x.2^2) ≤ E
 189
 190private theorem rigid_rotation_energy_lower_bound {ω₀ R : ℝ} (hω₀ : ω₀ ≠ 0) (hR : 0 < R) :
 191    ((ω₀ / 2) ^ 2) * R ^ 4 / 64 ≤
 192      ∫ x in Metric.ball (0 : ℝ × ℝ) R, ((ω₀ / 2) ^ 2) * (x.1 ^ 2 + x.2 ^ 2) := by
 193  let c : ℝ := (ω₀ / 2) ^ 2
 194  let rect : Set (ℝ × ℝ) := Set.Icc (R / 2) (3 * R / 4) ×ˢ Set.Icc 0 (R / 4)
 195  let f : ℝ × ℝ → ℝ := fun x => c * (x.1 ^ 2 + x.2 ^ 2)
 196  have hc_nonneg : 0 ≤ c := by
 197    dsimp [c]
 198    positivity
 199  have hrect_subset_ball : rect ⊆ Metric.ball (0 : ℝ × ℝ) R := by
 200    intro x hx
 201    rcases hx with ⟨hx1, hx2⟩
 202    rw [Metric.mem_ball, Prod.dist_eq, Real.dist_eq, Real.dist_eq, max_lt_iff]
 203    constructor
 204    · have hx1_nonneg : 0 ≤ x.1 := by
 205        linarith [hx1.1, hR]
 206      have hx1_lt : x.1 < R := by
 207        linarith [hx1.2, hR]
 208      simpa [abs_of_nonneg hx1_nonneg] using hx1_lt
 209    · have hx2_nonneg : 0 ≤ x.2 := hx2.1
 210      have hx2_lt : x.2 < R := by
 211        linarith [hx2.2, hR]
 212      simpa [abs_of_nonneg hx2_nonneg] using hx2_lt
 213  have hf_cont : Continuous f := by
 214    dsimp [f]
 215    continuity
 216  have hf_int_closed : IntegrableOn f (Metric.closedBall (0 : ℝ × ℝ) R) volume := by
 217    exact hf_cont.continuousOn.integrableOn_compact
 218      (isCompact_closedBall (x := (0 : ℝ × ℝ)) (r := R))
 219  have hf_int_ball : IntegrableOn f (Metric.ball (0 : ℝ × ℝ) R) volume :=
 220    hf_int_closed.mono_set Metric.ball_subset_closedBall
 221  have hf_nonneg_ball : 0 ≤ᵐ[volume.restrict (Metric.ball (0 : ℝ × ℝ) R)] f := by
 222    refine MeasureTheory.ae_restrict_of_forall_mem (Metric.isOpen_ball.measurableSet) ?_
 223    intro x hx
 224    dsimp [f]
 225    positivity
 226  have hball_ge_rect :
 227      ∫ x in rect, f x ∂volume ≤ ∫ x in Metric.ball (0 : ℝ × ℝ) R, f x ∂volume := by
 228    refine MeasureTheory.setIntegral_mono_set hf_int_ball hf_nonneg_ball ?_
 229    exact Filter.Eventually.of_forall hrect_subset_ball
 230  have hf_int_rect : IntegrableOn f rect volume := hf_int_ball.mono_set hrect_subset_ball
 231  have hrect_compact : IsCompact rect := by
 232    exact isCompact_Icc.prod isCompact_Icc
 233  have hconst_int : IntegrableOn (fun _ : ℝ × ℝ => c * (R / 2) ^ 2) rect volume := by
 234    simpa using
 235      (MeasureTheory.integrableOn_const (μ := (volume : MeasureTheory.Measure (ℝ × ℝ)))
 236        (s := rect) (C := c * (R / 2) ^ 2) (hs := hrect_compact.measure_lt_top.ne))
 237  have hconst_le : (fun _ : ℝ × ℝ => c * (R / 2) ^ 2) ≤ᵐ[volume.restrict rect] f := by
 238    refine MeasureTheory.ae_restrict_of_forall_mem ?_ ?_
 239    · exact measurableSet_Icc.prod measurableSet_Icc
 240    · intro x hx
 241      rcases hx with ⟨hx1, hx2⟩
 242      have hR2 : 0 ≤ R / 2 := by
 243        linarith
 244      have hx10 : 0 ≤ x.1 := le_trans hR2 hx1.1
 245      have hx1sq : (R / 2) ^ 2 ≤ x.1 ^ 2 := by
 246        exact (sq_le_sq₀ (a := R / 2) (b := x.1) hR2 hx10).2 hx1.1
 247      dsimp [f]
 248      nlinarith [hc_nonneg, hx1sq, sq_nonneg x.2]
 249  have hrect_lower :
 250      ∫ x in rect, c * (R / 2) ^ 2 ∂volume ≤ ∫ x in rect, f x ∂volume :=
 251    MeasureTheory.setIntegral_mono_ae_restrict hconst_int hf_int_rect hconst_le
 252  have hrect_measure : (volume : MeasureTheory.Measure (ℝ × ℝ)).real rect = (R / 4) * (R / 4) := by
 253    let sx : Set ℝ := Set.Icc (R / 2) (3 * R / 4)
 254    let sy : Set ℝ := Set.Icc 0 (R / 4)
 255    have hprod :
 256        (MeasureTheory.volume : MeasureTheory.Measure (ℝ × ℝ)) (sx ×ˢ sy) =
 257          (MeasureTheory.volume : MeasureTheory.Measure ℝ) sx *
 258            (MeasureTheory.volume : MeasureTheory.Measure ℝ) sy :=
 259      MeasureTheory.Measure.prod_prod _ _
 260    have hx : 3 * R / 4 - R / 2 = R / 4 := by
 261      ring
 262    change ENNReal.toReal ((MeasureTheory.volume : MeasureTheory.Measure (ℝ × ℝ)) (sx ×ˢ sy)) =
 263      (R / 4) * (R / 4)
 264    rw [hprod]
 265    simp [sx, sy, Real.volume_Icc, hx, show 0 ≤ R / 4 by linarith]
 266  have hconst_eval :
 267      ∫ x in rect, c * (R / 2) ^ 2 ∂volume = (R / 4) * (R / 4) * (c * (R / 2) ^ 2) := by
 268    calc
 269      ∫ x in rect, c * (R / 2) ^ 2 ∂volume =
 270          (volume : MeasureTheory.Measure (ℝ × ℝ)).real rect * (c * (R / 2) ^ 2) := by
 271            simp [MeasureTheory.integral_const]
 272      _ = (R / 4) * (R / 4) * (c * (R / 2) ^ 2) := by
 273            rw [hrect_measure]
 274  have hconst_eval' : ((ω₀ / 2) ^ 2) * R ^ 4 / 64 ≤ ∫ x in rect, c * (R / 2) ^ 2 ∂volume := by
 275    rw [hconst_eval]
 276    dsimp [c]
 277    ring_nf
 278    nlinarith [sq_nonneg (ω₀ / 2), sq_nonneg R]
 279  calc
 280    ((ω₀ / 2) ^ 2) * R ^ 4 / 64 ≤ ∫ x in rect, c * (R / 2) ^ 2 ∂volume := hconst_eval'
 281    _ ≤ ∫ x in rect, f x ∂volume := hrect_lower
 282    _ ≤ ∫ x in Metric.ball (0 : ℝ × ℝ) R, f x ∂volume := hball_ge_rect
 283    _ = ∫ x in Metric.ball (0 : ℝ × ℝ) R, ((ω₀ / 2) ^ 2) * (x.1 ^ 2 + x.2 ^ 2) := by
 284          rfl
 285
 286/-- Nonzero rigid rotations violate any uniform finite-energy bound on expanding balls. -/
 287theorem rigid_rotation_infinite_energy_proved (ω₀ : ℝ) (hω₀ : ω₀ ≠ 0) :
 288    rigid_rotation_infinite_energy ω₀ hω₀ := by
 289  intro hE
 290  rcases hE with ⟨E, hE⟩
 291  let c : ℝ := (ω₀ / 2) ^ 2
 292  have hc : 0 < c := by
 293    dsimp [c]
 294    exact sq_pos_of_ne_zero (div_ne_zero hω₀ (by norm_num))
 295  have hE_nonneg : 0 ≤ E := by
 296    have hlower :
 297        c / 64 ≤ ∫ x in Metric.ball (0 : ℝ × ℝ) 1, ((ω₀ / 2) ^ 2) * (x.1 ^ 2 + x.2 ^ 2) := by
 298      simpa [c] using (rigid_rotation_energy_lower_bound hω₀ (by norm_num : 0 < (1 : ℝ)))
 299    have hupper := hE 1 (by norm_num)
 300    nlinarith
 301  let R : ℝ := max 1 (64 * (E + 1) / c)
 302  have hRpos : 0 < R := by
 303    dsimp [R]
 304    positivity
 305  have hRge1 : 1 ≤ R := by
 306    dsimp [R]
 307    exact le_max_left _ _
 308  have hRge : 64 * (E + 1) / c ≤ R := by
 309    dsimp [R]
 310    exact le_max_right _ _
 311  have hR2_ge : R ≤ R ^ 2 := by
 312    nlinarith [hRge1]
 313  have hRpow : R ≤ R ^ 4 := by
 314    have hR2_sq : R ^ 2 ≤ R ^ 4 := by
 315      nlinarith [hRge1]
 316    linarith
 317  have hbig : E < c * R ^ 4 / 64 := by
 318    have hscaled : 64 * (E + 1) ≤ c * R := by
 319      have := (div_le_iff₀ hc).mp hRge
 320      nlinarith [this]
 321    have hscaled' : E + 1 ≤ c * R / 64 := by
 322      nlinarith [hscaled]
 323    have hquartic : c * R / 64 ≤ c * R ^ 4 / 64 := by
 324      have hc_nonneg : 0 ≤ c := le_of_lt hc
 325      nlinarith [hRpow, hc_nonneg]
 326    linarith
 327  have hlower :
 328      c * R ^ 4 / 64 ≤ ∫ x in Metric.ball (0 : ℝ × ℝ) R, ((ω₀ / 2) ^ 2) * (x.1 ^ 2 + x.2 ^ 2) := by
 329    simpa [c] using (rigid_rotation_energy_lower_bound hω₀ hRpos)
 330  have hupper := hE R hRpos
 331  nlinarith
 332
 333/-! ## Summary Certificate -/
 334
 335structure RunningMaxCert where
 336  /-- Running max is monotone. -/
 337  monotone : ∀ a : ℕ → ℝ, Monotone (runningMax a)
 338  /-- Normalization by the running max bounds the rescaled sequence by 1. -/
 339  bounded : ∀ M : ℕ → ℝ, (∀ n, 0 < M n) → ∀ n, normalized M n ≤ 1
 340  /-- A zero of the positive-definite J-cost in `(0,∞)` must occur at `1`. -/
 341  tf_pinch :
 342    ∀ (J : ℝ → ℝ), ConvexOn ℝ (Set.Ioi 0) J → J 1 = 0 →
 343      (∀ x, x ∈ Set.Ioi 0 → x ≠ 1 → J x > 0) →
 344      ∀ x, x ∈ Set.Ioi 0 → J x = 0 → x = 1
 345  /-- Constant vorticity profiles are rigid rotations. -/
 346  rigid_rotation :
 347    ∀ ω₀ : ℝ, ∃ (u : ℝ × ℝ → ℝ × ℝ), ∀ (x : ℝ × ℝ),
 348      u x = (ω₀ / 2 * (-x.2), ω₀ / 2 * x.1)
 349  /-- Nonzero rigid rotations force quartically divergent ball energy. -/
 350  rigid_rotation_energy_diverges :
 351    ∀ (ω₀ : ℝ) (hω₀ : ω₀ ≠ 0), rigid_rotation_infinite_energy ω₀ hω₀
 352
 353theorem runningMaxCert : RunningMaxCert where
 354  monotone := runningMax_mono
 355  bounded := normalized_bounded
 356  tf_pinch := tf_pinch_at_zero_node
 357  rigid_rotation := constant_vorticity_implies_rigid_rotation
 358  rigid_rotation_energy_diverges := rigid_rotation_infinite_energy_proved
 359
 360end RunningMaxNormalization
 361end NavierStokes
 362end IndisputableMonolith
 363