IndisputableMonolith.NavierStokes.StretchingPairs

   1import Mathlib
   2import IndisputableMonolith.NavierStokes.PhiLadderCutoff
   3import IndisputableMonolith.NavierStokes.DiscreteVorticity
   4
   5/-!
   6# RCL Pair Events for Discrete Stretching
   7
   8This module isolates the algebraic core behind the J-cost monotonicity program:
   9
  10- paired stretching/compression events,
  11- the exact Recognition Composition Law balance for such pairs,
  12- finite pair budgets indexed either by lists or by lattice sites.
  13
  14It is intentionally PDE-free so that concrete discrete Navier--Stokes operator
  15surfaces can reuse the same definitions without introducing abstraction cycles.
  16-/
  17
  18namespace IndisputableMonolith
  19namespace NavierStokes
  20namespace StretchingPairs
  21
  22open PhiLadderCutoff
  23open DiscreteVorticity
  24
  25noncomputable section
  26
  27/-- Cost change for a paired stretching event
  28`x -> lam*x` together with `x -> x/lam`. -/
  29def pairwiseStretchingChange (x lam : ℝ) : ℝ :=
  30  Jcost (x * lam) + Jcost (x / lam) - 2 * Jcost x
  31
  32/-- Exact Recognition Composition Law identity for the canonical cost. -/
  33theorem pairwise_RCL_balance {x lam : ℝ} (hx : 0 < x) (hlam : 0 < lam) :
  34    pairwiseStretchingChange x lam =
  35      2 * Jcost x * Jcost lam + 2 * Jcost lam := by
  36  unfold pairwiseStretchingChange Jcost
  37  have hxne : x ≠ 0 := ne_of_gt hx
  38  have hlamne : lam ≠ 0 := ne_of_gt hlam
  39  field_simp [hxne, hlamne]
  40  ring
  41
  42/-- Equivalent factorized form of the paired stretching balance. -/
  43theorem pairwise_RCL_balance_factored {x lam : ℝ} (hx : 0 < x) (hlam : 0 < lam) :
  44    pairwiseStretchingChange x lam =
  45      2 * (Jcost x + 1) * Jcost lam := by
  46  rw [pairwise_RCL_balance hx hlam]
  47  ring
  48
  49/-- Paired stretching cannot decrease J-cost: it is nonnegative by RCL and
  50nonnegativity of `Jcost`. -/
  51theorem pairwiseStretching_nonneg {x lam : ℝ} (hx : 0 < x) (hlam : 0 < lam) :
  52    0 ≤ pairwiseStretchingChange x lam := by
  53  rw [pairwise_RCL_balance_factored hx hlam]
  54  have hxJ : 0 ≤ Jcost x := Jcost_nonneg hx
  55  have hlamJ : 0 ≤ Jcost lam := Jcost_nonneg hlam
  56  nlinarith
  57
  58/-- A concrete paired stretching event. -/
  59structure PairEvent where
  60  amplitude : ℝ
  61  stretchFactor : ℝ
  62  amplitude_pos : 0 < amplitude
  63  stretchFactor_pos : 0 < stretchFactor
  64
  65/-- The J-cost budget contributed by one paired stretching event. -/
  66def pairEventBudget (ev : PairEvent) : ℝ :=
  67  pairwiseStretchingChange ev.amplitude ev.stretchFactor
  68
  69theorem pairEventBudget_nonneg (ev : PairEvent) : 0 ≤ pairEventBudget ev :=
  70  pairwiseStretching_nonneg ev.amplitude_pos ev.stretchFactor_pos
  71
  72/-- Total RCL pair budget carried by a finite family of stretching events. -/
  73def totalPairBudget (events : List PairEvent) : ℝ :=
  74  (events.map pairEventBudget).sum
  75
  76theorem totalPairBudget_nonneg (events : List PairEvent) : 0 ≤ totalPairBudget events := by
  77  induction events with
  78  | nil =>
  79      simp [totalPairBudget]
  80  | cons ev events ih =>
  81      simp [totalPairBudget]
  82      exact add_nonneg (pairEventBudget_nonneg ev) ih
  83
  84/-- Indexed pair budget over a finite lattice window. -/
  85def indexedPairBudget {siteCount : ℕ} (event : Fin siteCount → PairEvent) : ℝ :=
  86  total (fun i => pairEventBudget (event i))
  87
  88theorem indexedPairBudget_nonneg {siteCount : ℕ} (event : Fin siteCount → PairEvent) :
  89    0 ≤ indexedPairBudget event := by
  90  unfold indexedPairBudget total
  91  exact Finset.sum_nonneg (fun i _ => pairEventBudget_nonneg (event i))
  92
  93end
  94
  95end StretchingPairs
  96end NavierStokes
  97end IndisputableMonolith
  98