discreteVelocityDim
plain-language theorem explainer
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.
Claim. The 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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.