IndisputableMonolith.NavierStokes.DiscreteVorticity

   1import Mathlib
   2import IndisputableMonolith.NavierStokes.PhiLadderCutoff
   3
   4/-!
   5# Discrete Vorticity Bookkeeping
   6
   7This module packages the discrete objects needed for the J-cost monotonicity
   8program. The emphasis is on exact bookkeeping:
   9
  10- finite vorticity fields on a lattice window,
  11- total / RMS / normalized amplitudes,
  12- transport / viscous / stretching contribution fields,
  13- exact decomposition of the J-cost derivative into those three pieces.
  14
  15The hard PDE inequalities are intentionally separated from this bookkeeping
  16surface so they can be added one lemma at a time.
  17-/
  18
  19namespace IndisputableMonolith
  20namespace NavierStokes
  21namespace DiscreteVorticity
  22
  23open PhiLadderCutoff
  24
  25noncomputable section
  26
  27/-- A finite discrete vorticity field on a lattice window of `siteCount` sites. -/
  28structure State (siteCount : ℕ) where
  29  omega : Fin siteCount → ℝ
  30
  31/-- Sum of a scalar field over the finite lattice window. -/
  32def total {siteCount : ℕ} (f : Fin siteCount → ℝ) : ℝ :=
  33  ∑ i : Fin siteCount, f i
  34
  35/-- RMS square of a scalar field. -/
  36def rmsSq {siteCount : ℕ} (f : Fin siteCount → ℝ) : ℝ :=
  37  total (fun i => (f i) ^ 2) / siteCount
  38
  39/-- RMS amplitude of a scalar field. -/
  40def rms {siteCount : ℕ} (f : Fin siteCount → ℝ) : ℝ :=
  41  Real.sqrt (rmsSq f)
  42
  43/-- Pointwise normalized amplitude relative to the RMS scale. -/
  44def normalizedAmplitude {siteCount : ℕ} (f : Fin siteCount → ℝ) (i : Fin siteCount) : ℝ :=
  45  |f i| / rms f
  46
  47/-- The total J-cost of a discrete vorticity field relative to its RMS scale. -/
  48def totalJcost {siteCount : ℕ} (f : Fin siteCount → ℝ) : ℝ :=
  49  total (fun i => Jcost (normalizedAmplitude f i))
  50
  51/-- Contribution fields appearing in the J-cost derivative identity. -/
  52structure ContributionFields (siteCount : ℕ) where
  53  transport : Fin siteCount → ℝ
  54  viscous : Fin siteCount → ℝ
  55  stretching : Fin siteCount → ℝ
  56
  57/-- Total contributions of the three pieces. -/
  58def totalTransport {siteCount : ℕ} (c : ContributionFields siteCount) : ℝ :=
  59  total c.transport
  60
  61def totalViscous {siteCount : ℕ} (c : ContributionFields siteCount) : ℝ :=
  62  total c.viscous
  63
  64def totalStretching {siteCount : ℕ} (c : ContributionFields siteCount) : ℝ :=
  65  total c.stretching
  66
  67/-- Data recording an exact J-cost derivative split. -/
  68structure EvolutionIdentity (siteCount : ℕ) where
  69  contributions : ContributionFields siteCount
  70  dJdt : ℝ
  71  split :
  72    dJdt = totalTransport contributions
  73      + totalViscous contributions
  74      + totalStretching contributions
  75
  76/-- If the transport contribution has zero total, it cancels exactly. -/
  77theorem transport_term_cancels {siteCount : ℕ} (c : ContributionFields siteCount)
  78    (htransport : totalTransport c = 0) :
  79    totalTransport c = 0 := htransport
  80
  81/-- If every viscous contribution is nonpositive, then the total viscous term is
  82nonpositive. -/
  83theorem viscous_term_dissipative {siteCount : ℕ} (c : ContributionFields siteCount)
  84    (hvisc : ∀ i : Fin siteCount, c.viscous i ≤ 0) :
  85    totalViscous c ≤ 0 := by
  86  unfold totalViscous total
  87  exact Finset.sum_nonpos (fun i _ => hvisc i)
  88
  89/-- If every stretching contribution is nonnegative, then the total stretching
  90term is nonnegative. -/
  91theorem stretching_term_nonneg {siteCount : ℕ} (c : ContributionFields siteCount)
  92    (hstretch : ∀ i : Fin siteCount, 0 ≤ c.stretching i) :
  93    0 ≤ totalStretching c := by
  94  unfold totalStretching total
  95  exact Finset.sum_nonneg (fun i _ => hstretch i)
  96
  97/-- A pointwise transport field with zero entries has zero total. -/
  98theorem zero_transport_cancels {siteCount : ℕ} (c : ContributionFields siteCount)
  99    (hzero : ∀ i : Fin siteCount, c.transport i = 0) :
 100    totalTransport c = 0 := by
 101  unfold totalTransport total
 102  simp [hzero]
 103
 104/-- The exact derivative identity can be rewritten after transport cancellation. -/
 105theorem dJdt_eq_viscous_plus_stretching {siteCount : ℕ} (e : EvolutionIdentity siteCount)
 106    (htransport : totalTransport e.contributions = 0) :
 107    e.dJdt = totalViscous e.contributions + totalStretching e.contributions := by
 108  rw [e.split, htransport, zero_add]
 109
 110/-- If stretching is absorbed by viscosity, then the total derivative is nonpositive. -/
 111theorem dJdt_nonpos_of_transport_cancel_and_absorption
 112    {siteCount : ℕ} (e : EvolutionIdentity siteCount)
 113    (htransport : totalTransport e.contributions = 0)
 114    (habsorb :
 115      totalStretching e.contributions ≤ - totalViscous e.contributions) :
 116    e.dJdt ≤ 0 := by
 117  rw [dJdt_eq_viscous_plus_stretching e htransport]
 118  linarith
 119
 120end
 121
 122end DiscreteVorticity
 123end NavierStokes
 124end IndisputableMonolith
 125