 191/-! ## Discrete Lattice Properties -/
 192
 193/-- Dimension of the discrete velocity space on (Z/NZ)³. -/
 194def discreteVelocityDim (N : ℕ) : ℕ := 3 * N ^ 3
 195
 196/-- The discrete system is finite-dimensional for N > 0. -/
 197theorem discrete_finite_dim (N : ℕ) (hN : 0 < N) :
 198    0 < discreteVelocityDim N := by
 199  unfold discreteVelocityDim; positivity
 200
 201/-! ## J-Cost Blow-up Exclusion -/
 202
 203/-- If J-cost is bounded by B, then the ratio r ≤ 2B + 2. -/
 204theorem Jcost_ratio_bound {r B : ℝ} (hr : 0 < r) (hbound : Jcost r ≤ B) :
 205    r ≤ 2 * B + 2 := by
 206  unfold Jcost at hbound
 207  have : 0 < r⁻¹ := inv_pos.mpr hr
 208  linarith
 209
 210/-- Bounded J-cost implies bounded pointwise vorticity. -/
 211theorem bounded_Jcost_bounded_max {max_val ref_val B : ℝ}
 212    (hmax : 0 < max_val) (href : 0 < ref_val)
 213    (hbound : Jcost (max_val / ref_val) ≤ B) :
 214    max_val ≤ (2 * B + 2) * ref_val := by
 215  have hr : 0 < max_val / ref_val := div_pos hmax href
 216  have hle := Jcost_ratio_bound hr hbound
 217  have : max_val / ref_val * ref_val ≤ (2 * B + 2) * ref_val :=
 218    mul_le_mul_of_nonneg_right hle (le_of_lt href)
 219  rwa [div_mul_cancel₀ _ (ne_of_gt href)] at this
 220
 221/-! ## Certificate Structure -/
 222
 223/-- Certificate packaging the main results. -/
 224structure PhiLadderCutoffCert where

papers checked against this theorem

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