`total_conservativeTransportField_zero`

proved

show as: view math explainer →

module: IndisputableMonolith.NavierStokes.DiscreteNSOperator
domain: NavierStokes
line: 73 · github
papers citing: none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.NavierStokes.DiscreteNSOperator on GitHub at line 73.

browse module

All declarations in this module, on Recognition.

explainer page

Tracked in the explainer inventory; generation is lazy so crawlers do not trigger LLM jobs.

open explainer

depends on

used by

formal source

  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

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.