IndisputableMonolith.NavierStokes.JcostMonotonicity

   1import Mathlib
   2import IndisputableMonolith.NavierStokes.DiscreteNSOperator
   3
   4/-!
   5# J-cost Monotonicity for the Concrete Lattice NS Operator
   6
   7This module closes the bookkeeping part of the monotonicity program against a
   8concrete discrete incompressible Navier--Stokes operator surface:
   9
  101. transport cancellation is derived from conservative incompressible flux;
  112. the stretching term is bounded by the operator's own RCL pair budget;
  123. viscosity absorbs that operator-derived budget;
  134. therefore the total J-cost derivative is nonpositive.
  14
  15What remains open is no longer the existence of a good certificate object.  The
  16remaining PDE question is to verify, for the real lattice flow, the operator
  17inequalities packaged in `DiscreteNSOperator.IncompressibleNSOperator`.
  18-/
  19
  20namespace IndisputableMonolith
  21namespace NavierStokes
  22namespace JcostMonotonicity
  23
  24open DiscreteVorticity
  25open StretchingPairs
  26open DiscreteNSOperator
  27
  28noncomputable section
  29
  30/-- The actual lattice stretching contribution is absorbed by the operator's
  31viscous budget once the sitewise RCL pair bounds are summed. -/
  32theorem stretching_absorbed_by_viscosity {siteCount : ℕ}
  33    (ns : IncompressibleNSOperator siteCount) :
  34    totalStretching ns.contributions ≤ - totalViscous ns.contributions := by
  35  exact le_trans (totalStretching_le_operatorPairBudget ns)
  36    (operatorPairBudget_absorbed_by_viscosity ns)
  37
  38/-- The concrete discrete NS operator has nonincreasing total J-cost once its
  39pair budget is absorbed by viscosity. -/
  40theorem dJcost_dt_nonpos_of_operator {siteCount : ℕ}
  41    (ns : IncompressibleNSOperator siteCount) :
  42    ns.dJdt ≤ 0 :=
  43  dJdt_nonpos_of_transport_cancel_and_absorption ns.toEvolutionIdentity
  44    (operator_transport_zero ns) (stretching_absorbed_by_viscosity ns)
  45
  46/-- Packaged monotonicity certificate for the concrete lattice operator. -/
  47structure MonotonicityCert (siteCount : ℕ) where
  48  operator : IncompressibleNSOperator siteCount
  49  nonpositive_derivative : operator.dJdt ≤ 0
  50
  51/-- Any concrete lattice NS operator yields a monotonicity certificate once its
  52operator-derived pair budget is absorbed by viscosity. -/
  53def monotonicityCert {siteCount : ℕ}
  54    (ns : IncompressibleNSOperator siteCount) : MonotonicityCert siteCount where
  55  operator := ns
  56  nonpositive_derivative := dJcost_dt_nonpos_of_operator ns
  57
  58end
  59
  60end JcostMonotonicity
  61end NavierStokes
  62end IndisputableMonolith
  63