structure
definition
def or abbrev
CoreNSOperator
show as:
view Lean formalization →
formal statement (Lean)
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. -/