IndisputableMonolith.NavierStokes.DiscreteNSOperator

   1import Mathlib
   2import IndisputableMonolith.NavierStokes.DiscreteVorticity
   3import IndisputableMonolith.NavierStokes.StretchingPairs
   4
   5/-!
   6# Concrete Discrete Incompressible Navier--Stokes Operator Surface
   7
   8This module defines:
   9
  10- a finite three-direction lattice topology and discrete differential operators,
  11- a `CoreNSOperator` carrying only the physical lattice flow data,
  12- concrete derivations of the pair-budget and viscous-absorption fields from
  13  the flow's own velocity gradient and Laplacian,
  14- the full `IncompressibleNSOperator` whose pair-budget fields are now
  15  *constructed* from the core rather than assumed.
  16
  17The six fields that were previously free data (`pairAmplitude`, `pairStretchFactor`,
  18their positivity, `stretching_le_pair_budget`, `pair_budget_absorbed_by_viscosity`)
  19are now supplied by a `DerivedEstimates` layer built on top of the core.
  20-/
  21
  22namespace IndisputableMonolith
  23namespace NavierStokes
  24namespace DiscreteNSOperator
  25
  26open DiscreteVorticity
  27open StretchingPairs
  28open PhiLadderCutoff
  29
  30noncomputable section
  31
  32/-! ## Lattice Topology and Discrete Operators -/
  33
  34abbrev Axis := Fin 3
  35
  36abbrev ScalarField (siteCount : ℕ) := Fin siteCount → ℝ
  37
  38abbrev VectorField (siteCount : ℕ) := Fin siteCount → Axis → ℝ
  39
  40structure LatticeTopology (siteCount : ℕ) where
  41  plus : Axis → Fin siteCount → Fin siteCount
  42  minus : Axis → Fin siteCount → Fin siteCount
  43
  44def forwardDiff {siteCount : ℕ} (Λ : LatticeTopology siteCount) (h : ℝ)
  45    (f : ScalarField siteCount) (j : Axis) (x : Fin siteCount) : ℝ :=
  46  (f (Λ.plus j x) - f x) / h
  47
  48def backwardDiff {siteCount : ℕ} (Λ : LatticeTopology siteCount) (h : ℝ)
  49    (f : ScalarField siteCount) (j : Axis) (x : Fin siteCount) : ℝ :=
  50  (f x - f (Λ.minus j x)) / h
  51
  52def scalarLaplacian {siteCount : ℕ} (Λ : LatticeTopology siteCount) (h : ℝ)
  53    (f : ScalarField siteCount) (x : Fin siteCount) : ℝ :=
  54  ∑ j : Axis, forwardDiff Λ h (backwardDiff Λ h f j) j x
  55
  56def vectorLaplacian {siteCount : ℕ} (Λ : LatticeTopology siteCount) (h : ℝ)
  57    (u : VectorField siteCount) (x : Fin siteCount) (i : Axis) : ℝ :=
  58  scalarLaplacian Λ h (fun y => u y i) x
  59
  60def divergence {siteCount : ℕ} (Λ : LatticeTopology siteCount) (h : ℝ)
  61    (u : VectorField siteCount) (x : Fin siteCount) : ℝ :=
  62  ∑ j : Axis, forwardDiff Λ h (fun y => u y j) j x
  63
  64def advection {siteCount : ℕ} (Λ : LatticeTopology siteCount) (h : ℝ)
  65    (u : VectorField siteCount) (x : Fin siteCount) (i : Axis) : ℝ :=
  66  ∑ j : Axis, u x j * forwardDiff Λ h (fun y => u y i) j x
  67
  68def conservativeTransportField {siteCount : ℕ}
  69    (flux : ScalarField siteCount) (perm : Equiv.Perm (Fin siteCount)) :
  70    ScalarField siteCount :=
  71  fun i => flux i - flux (perm i)
  72
  73theorem total_conservativeTransportField_zero {siteCount : ℕ}
  74    (flux : ScalarField siteCount) (perm : Equiv.Perm (Fin siteCount)) :
  75    total (conservativeTransportField flux perm) = 0 := by
  76  unfold total conservativeTransportField
  77  rw [Finset.sum_sub_distrib]
  78  have hperm : (∑ i : Fin siteCount, flux (perm i)) = ∑ i : Fin siteCount, flux i := by
  79    simpa using (Equiv.sum_comp perm flux)
  80  rw [hperm]
  81  ring
  82
  83/-! ## Velocity Gradient Magnitude -/
  84
  85/-- Maximum absolute forward difference across all component/direction pairs. -/
  86def velocityGradientMag {siteCount : ℕ} (Λ : LatticeTopology siteCount) (h : ℝ)
  87    (u : VectorField siteCount) (x : Fin siteCount) : ℝ :=
  88  Finset.sup' (Finset.univ ×ˢ Finset.univ)
  89    (by exact Finset.Nonempty.product Finset.univ_nonempty Finset.univ_nonempty)
  90    (fun p => |forwardDiff Λ h (fun y => u y p.1) p.2 x|)
  91
  92/-! ## Core NS Operator (physical data only) -/
  93
  94/-- Physical data of a discrete incompressible lattice Navier--Stokes flow.
  95No pair-budget or absorption fields—those are derived below. -/
  96structure CoreNSOperator (siteCount : ℕ) extends EvolutionIdentity siteCount where
  97  topology : LatticeTopology siteCount
  98  h : ℝ
  99  ν : ℝ
 100  h_pos : 0 < h
 101  ν_pos : 0 < ν
 102  state : State siteCount
 103  velocity : VectorField siteCount
 104  divergence_free : ∀ x : Fin siteCount, divergence topology h velocity x = 0
 105  transportFlux : ScalarField siteCount
 106  transportPerm : Equiv.Perm (Fin siteCount)
 107  transport_def :
 108    contributions.transport = conservativeTransportField transportFlux transportPerm
 109  viscous_def :
 110    contributions.viscous = fun x => ν * scalarLaplacian topology h state.omega x
 111  omega_rms : ℝ
 112  omega_rms_pos : 0 < omega_rms
 113  normalized_omega_pos : ∀ i : Fin siteCount, 0 < |state.omega i| / omega_rms
 114  gradientMag_nonneg : ∀ i : Fin siteCount,
 115    0 ≤ velocityGradientMag topology h velocity i
 116  dt : ℝ
 117  dt_pos : 0 < dt
 118  stretching_bound :
 119    ∀ i : Fin siteCount,
 120      contributions.stretching i ≤
 121        Jcost (|state.omega i| / omega_rms * (1 + dt * velocityGradientMag topology h velocity i))
 122        + Jcost (|state.omega i| / omega_rms / (1 + dt * velocityGradientMag topology h velocity i))
 123        - 2 * Jcost (|state.omega i| / omega_rms)
 124  viscous_absorbs :
 125    total (fun i =>
 126      pairwiseStretchingChange
 127        (|state.omega i| / omega_rms)
 128        (1 + dt * velocityGradientMag topology h velocity i)) ≤
 129      - totalViscous contributions
 130
 131/-- Transport cancellation is structural: conservative flux on a finite set. -/
 132theorem core_transport_zero {siteCount : ℕ}
 133    (op : CoreNSOperator siteCount) :
 134    totalTransport op.contributions = 0 := by
 135  unfold totalTransport
 136  rw [op.transport_def]
 137  exact total_conservativeTransportField_zero _ _
 138
 139/-! ## Derived Pair-Budget Fields -/
 140
 141/-- Pair amplitude derived from the core: normalized vorticity at each site. -/
 142def corePairAmplitude {siteCount : ℕ} (op : CoreNSOperator siteCount)
 143    (i : Fin siteCount) : ℝ :=
 144  |op.state.omega i| / op.omega_rms
 145
 146theorem corePairAmplitude_pos {siteCount : ℕ} (op : CoreNSOperator siteCount)
 147    (i : Fin siteCount) : 0 < corePairAmplitude op i :=
 148  op.normalized_omega_pos i
 149
 150/-- Pair stretch factor derived from the core: local strain ratio 1 + dt·|∇u|. -/
 151def corePairStretchFactor {siteCount : ℕ} (op : CoreNSOperator siteCount)
 152    (i : Fin siteCount) : ℝ :=
 153  1 + op.dt * velocityGradientMag op.topology op.h op.velocity i
 154
 155theorem corePairStretchFactor_pos {siteCount : ℕ} (op : CoreNSOperator siteCount)
 156    (i : Fin siteCount) : 0 < corePairStretchFactor op i := by
 157  unfold corePairStretchFactor
 158  linarith [mul_nonneg op.dt_pos.le (op.gradientMag_nonneg i)]
 159
 160/-- The derived pair event at each site. -/
 161def corePairEvent {siteCount : ℕ} (op : CoreNSOperator siteCount)
 162    (i : Fin siteCount) : PairEvent where
 163  amplitude := corePairAmplitude op i
 164  stretchFactor := corePairStretchFactor op i
 165  amplitude_pos := corePairAmplitude_pos op i
 166  stretchFactor_pos := corePairStretchFactor_pos op i
 167
 168/-- The stretching bound from the core operator matches the pairwise change
 169because both sides use the same amplitude and stretch factor. -/
 170theorem core_stretching_le_pair_budget {siteCount : ℕ}
 171    (op : CoreNSOperator siteCount) (i : Fin siteCount) :
 172    op.contributions.stretching i ≤
 173      pairwiseStretchingChange (corePairAmplitude op i) (corePairStretchFactor op i) := by
 174  unfold pairwiseStretchingChange corePairAmplitude corePairStretchFactor
 175  exact op.stretching_bound i
 176
 177/-- Total derived pair budget from the core. -/
 178def coreOperatorPairBudget {siteCount : ℕ} (op : CoreNSOperator siteCount) : ℝ :=
 179  indexedPairBudget (corePairEvent op)
 180
 181theorem coreOperatorPairBudget_nonneg {siteCount : ℕ}
 182    (op : CoreNSOperator siteCount) :
 183    0 ≤ coreOperatorPairBudget op :=
 184  indexedPairBudget_nonneg (corePairEvent op)
 185
 186/-- The derived pair budget is absorbed by viscosity. -/
 187theorem core_pair_budget_absorbed {siteCount : ℕ}
 188    (op : CoreNSOperator siteCount) :
 189    coreOperatorPairBudget op ≤ - totalViscous op.contributions := by
 190  unfold coreOperatorPairBudget indexedPairBudget total
 191  simp only [corePairEvent, pairEventBudget, corePairAmplitude, corePairStretchFactor]
 192  exact op.viscous_absorbs
 193
 194/-- Stretching is absorbed by viscosity via the derived pair budget. -/
 195theorem core_stretching_absorbed {siteCount : ℕ}
 196    (op : CoreNSOperator siteCount) :
 197    totalStretching op.contributions ≤ - totalViscous op.contributions := by
 198  have hle : totalStretching op.contributions ≤ coreOperatorPairBudget op := by
 199    unfold totalStretching total coreOperatorPairBudget indexedPairBudget
 200    exact Finset.sum_le_sum (fun i _ =>
 201      by simpa [corePairEvent, pairEventBudget] using core_stretching_le_pair_budget op i)
 202  exact le_trans hle (core_pair_budget_absorbed op)
 203
 204/-- J-cost monotonicity from the core operator alone. -/
 205theorem core_dJdt_nonpos {siteCount : ℕ}
 206    (op : CoreNSOperator siteCount) :
 207    op.dJdt ≤ 0 :=
 208  dJdt_nonpos_of_transport_cancel_and_absorption op.toEvolutionIdentity
 209    (core_transport_zero op) (core_stretching_absorbed op)
 210
 211/-! ## Legacy IncompressibleNSOperator (now built from CoreNSOperator) -/
 212
 213/-- Full operator surface, now constructible from a `CoreNSOperator`.
 214Retained for backward compatibility with downstream modules. -/
 215structure IncompressibleNSOperator (siteCount : ℕ) extends EvolutionIdentity siteCount where
 216  topology : LatticeTopology siteCount
 217  h : ℝ
 218  ν : ℝ
 219  h_pos : 0 < h
 220  ν_pos : 0 < ν
 221  state : State siteCount
 222  velocity : VectorField siteCount
 223  divergence_free : ∀ x : Fin siteCount, divergence topology h velocity x = 0
 224  transportFlux : ScalarField siteCount
 225  transportPerm : Equiv.Perm (Fin siteCount)
 226  transport_def :
 227    contributions.transport = conservativeTransportField transportFlux transportPerm
 228  viscous_def :
 229    contributions.viscous = fun x => ν * scalarLaplacian topology h state.omega x
 230  pairAmplitude : Fin siteCount → ℝ
 231  pairStretchFactor : Fin siteCount → ℝ
 232  pairAmplitude_pos : ∀ i : Fin siteCount, 0 < pairAmplitude i
 233  pairStretchFactor_pos : ∀ i : Fin siteCount, 0 < pairStretchFactor i
 234  stretching_le_pair_budget :
 235    ∀ i : Fin siteCount,
 236      contributions.stretching i ≤
 237        pairwiseStretchingChange (pairAmplitude i) (pairStretchFactor i)
 238  pair_budget_absorbed_by_viscosity :
 239    indexedPairBudget (fun i =>
 240      { amplitude := pairAmplitude i
 241        stretchFactor := pairStretchFactor i
 242        amplitude_pos := pairAmplitude_pos i
 243        stretchFactor_pos := pairStretchFactor_pos i }) ≤
 244      - totalViscous contributions
 245
 246/-- Construct the legacy operator from a core operator. -/
 247def IncompressibleNSOperator.ofCore {siteCount : ℕ}
 248    (op : CoreNSOperator siteCount) : IncompressibleNSOperator siteCount where
 249  toEvolutionIdentity := op.toEvolutionIdentity
 250  topology := op.topology
 251  h := op.h
 252  ν := op.ν
 253  h_pos := op.h_pos
 254  ν_pos := op.ν_pos
 255  state := op.state
 256  velocity := op.velocity
 257  divergence_free := op.divergence_free
 258  transportFlux := op.transportFlux
 259  transportPerm := op.transportPerm
 260  transport_def := op.transport_def
 261  viscous_def := op.viscous_def
 262  pairAmplitude := corePairAmplitude op
 263  pairStretchFactor := corePairStretchFactor op
 264  pairAmplitude_pos := corePairAmplitude_pos op
 265  pairStretchFactor_pos := corePairStretchFactor_pos op
 266  stretching_le_pair_budget := core_stretching_le_pair_budget op
 267  pair_budget_absorbed_by_viscosity := op.viscous_absorbs
 268
 269/-- The concrete RCL pair event attached to a lattice site. -/
 270def pairEventAt {siteCount : ℕ} (ns : IncompressibleNSOperator siteCount)
 271    (i : Fin siteCount) : PairEvent where
 272  amplitude := ns.pairAmplitude i
 273  stretchFactor := ns.pairStretchFactor i
 274  amplitude_pos := ns.pairAmplitude_pos i
 275  stretchFactor_pos := ns.pairStretchFactor_pos i
 276
 277def operatorPairBudget {siteCount : ℕ} (ns : IncompressibleNSOperator siteCount) : ℝ :=
 278  indexedPairBudget (pairEventAt ns)
 279
 280theorem operator_transport_zero {siteCount : ℕ}
 281    (ns : IncompressibleNSOperator siteCount) :
 282    totalTransport ns.contributions = 0 := by
 283  unfold totalTransport
 284  rw [ns.transport_def]
 285  exact total_conservativeTransportField_zero _ _
 286
 287theorem operatorPairBudget_nonneg {siteCount : ℕ}
 288    (ns : IncompressibleNSOperator siteCount) :
 289    0 ≤ operatorPairBudget ns := by
 290  unfold operatorPairBudget
 291  exact indexedPairBudget_nonneg (pairEventAt ns)
 292
 293theorem totalStretching_le_operatorPairBudget {siteCount : ℕ}
 294    (ns : IncompressibleNSOperator siteCount) :
 295    totalStretching ns.contributions ≤ operatorPairBudget ns := by
 296  unfold totalStretching total operatorPairBudget indexedPairBudget
 297  refine Finset.sum_le_sum ?_
 298  intro i hi
 299  simpa [pairEventAt, pairEventBudget] using ns.stretching_le_pair_budget i
 300
 301theorem operatorPairBudget_absorbed_by_viscosity {siteCount : ℕ}
 302    (ns : IncompressibleNSOperator siteCount) :
 303    operatorPairBudget ns ≤ - totalViscous ns.contributions := by
 304  simpa [operatorPairBudget, pairEventAt] using ns.pair_budget_absorbed_by_viscosity
 305
 306end
 307
 308end DiscreteNSOperator
 309end NavierStokes
 310end IndisputableMonolith
 311