core_transport_zero

formal source

 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