IndisputableMonolith.NavierStokes.RM2U.Core

   1import Mathlib
   2
   3/-!
   4# RM2U.Core (spec layer)
   5
   6This module is the Lean-side **spec** for the RM2U “tail/tightness” gate in
   7`navier-dec-12-rewrite.tex`, refactored into a 1D radial coefficient problem.
   8
   9Key idea:
  10- Fix a time `t` and a spherical direction/test field parameter `b`.
  11- Work with the resulting scalar radial coefficient `A(r)` for `r ≥ 1`.
  12- The RM2U obstruction can be expressed through a **boundary / tail-flux term**
  13  `(-A(r)) * (A'(r) * r^2)` as `r → ∞`.
  14
  15All analytic identities are proved in `RM2U.EnergyIdentity` by reusing
  16`IndisputableMonolith.NavierStokes.SkewHarmGate`.
  17-/
  18
  19namespace IndisputableMonolith
  20namespace NavierStokes
  21namespace RM2U
  22
  23open scoped Topology Interval
  24open Filter MeasureTheory Set
  25
  26/-- Boundary term / tail-flux term appearing in the radial integration-by-parts identity:
  27
  28`B(r) := (-A(r)) * (A'(r) * r^2)`.
  29
  30This matches `SkewHarmGate.Radial.zeroSkewAtInfinity_of_integrable`.
  31-/
  32noncomputable def tailFlux (A A' : ℝ → ℝ) (r : ℝ) : ℝ :=
  33  (-A r) * ((A' r) * (r ^ 2))
  34
  35/-- “Tail flux vanishes at infinity”: the boundary term tends to `0` as `r → ∞`. -/
  36def TailFluxVanish (A A' : ℝ → ℝ) : Prop :=
  37  Tendsto (fun r : ℝ => tailFlux A A' r) atTop (𝓝 0)
  38
  39/-- Abstract profile for a fixed time-slice RM2U coefficient, with derivative data. -/
  40structure RM2URadialProfile where
  41  A : ℝ → ℝ
  42  A' : ℝ → ℝ
  43  A'' : ℝ → ℝ
  44  hA : ∀ x ∈ Set.Ioi (1 : ℝ), HasDerivAt A (A' x) x
  45  hA' : ∀ x ∈ Set.Ioi (1 : ℝ), HasDerivAt A' (A'' x) x
  46
  47namespace RM2URadialProfile
  48
  49/-- The boundary term associated to a profile. -/
  50noncomputable def boundaryTerm (P : RM2URadialProfile) : ℝ → ℝ :=
  51  fun r => tailFlux P.A P.A' r
  52
  53/-- Convenience: `TailFluxVanish` for a profile. -/
  54def tailFluxVanish (P : RM2URadialProfile) : Prop :=
  55  TailFluxVanish P.A P.A'
  56
  57end RM2URadialProfile
  58
  59/-- A concrete analytic target implied by UEWE and used to close RM2U in the manuscript:
  60integrability of the \(\ell=2\) coefficient and its derivative with the `r^2` weight. -/
  61def CoerciveL2Bound (P : RM2URadialProfile) : Prop :=
  62  IntegrableOn (fun r : ℝ => (P.A r) ^ 2) (Set.Ioi (1 : ℝ)) volume
  63    ∧ IntegrableOn (fun r : ℝ => (P.A' r) ^ 2 * (r ^ 2)) (Set.Ioi (1 : ℝ)) volume
  64
  65/-- The log-critical shell moment integrability (the RM2 obstruction in the manuscript):
  66`A(r)/r ∈ L¹((1,∞), dr)`. -/
  67def LogCriticalMomentFinite (A : ℝ → ℝ) : Prop :=
  68  IntegrableOn (fun r : ℝ => A r / r) (Set.Ioi (1 : ℝ)) volume
  69
  70end RM2U
  71end NavierStokes
  72end IndisputableMonolith
  73