discreteVelocityDim
The dimension of the discrete velocity space on the periodic lattice (Z/NZ)^3 equals three times N cubed. Researchers modeling Navier-Stokes regularity via the phi-ladder cutoff cite this count to establish that the discrete system has finitely many degrees of freedom. The definition is a direct arithmetic formula with no lemmas or tactics required.
claimThe dimension of the discrete velocity space on the lattice $ (Z/NZ)^3 $ is $ 3N^3 $.
background
This definition sits inside the module that formalizes the algebraic core of Navier-Stokes regularity from the phi-ladder cutoff. The module shows that the phi-ladder supplies an ultraviolet cutoff that terminates the energy cascade on the Recognition Science discrete lattice. Supporting results include Jcost_nonneg (J(x) nonnegative for x > 0) and phiRungScale_pos (phi-rungs positive and strictly increasing). Upstream structures ensure collision-free programs and simplicial edge lengths from psi, which keep the discrete setting algebraically closed.
proof idea
The declaration is a definition that directly returns the product of three and N cubed. No lemmas are applied and no tactics are used; the expression follows at once from counting three velocity components across an N by N by N grid.
why it matters in Recognition Science
The definition supplies the explicit count used by the theorem discrete_finite_dim, which proves strict positivity for N > 0. This anchors the finite-dimensionality step that precedes the main results on sub-dissipation decay to zero and finitely many rungs below any scale. It aligns with the framework's D = 3 spatial dimensions and eight-tick octave by giving the concrete size of the discrete velocity space before continuum limits are taken.
scope and limits
- Does not prove positivity or monotonicity of the dimension.
- Does not relate the dimension to J-cost or phi-rung scaling.
- Does not address the continuous Navier-Stokes equations or regularity criteria.
- Does not incorporate Reynolds number or other physical parameters.
Lean usage
theorem discrete_finite_dim (N : ℕ) (hN : 0 < N) : 0 < discreteVelocityDim N := by unfold discreteVelocityDim; positivityformal statement (Lean)
194def discreteVelocityDim (N : ℕ) : ℕ := 3 * N ^ 3
proof body
Definition body.
195
196/-- The discrete system is finite-dimensional for N > 0. -/