discrete_finite_dim
plain-language theorem explainer
The theorem establishes that the discrete velocity space has strictly positive dimension for every positive integer N. Researchers formalizing the phi-ladder ultraviolet cutoff for Navier-Stokes regularity cite it to confirm the discrete system stays finite-dimensional. The proof is a one-line term that unfolds the dimension definition and applies positivity.
Claim. For every natural number $N > 0$, the dimension of the discrete velocity space is strictly positive.
background
The module develops the algebraic core showing that the phi-ladder supplies an ultraviolet cutoff terminating the Navier-Stokes energy cascade on the recognition-science discrete lattice. Key definitions include the J-cost, the derived cost of a multiplicative recognizer's comparator on positive ratios, and the phi-rung scales, which are positive and strictly increasing. Upstream results establish that J-cost is nonnegative and vanishes only at unity, together with the cost of recognition events.
proof idea
The proof is a one-line wrapper that unfolds the definition of the discrete velocity dimension and applies the positivity tactic.
why it matters
This result supports the module's main claims on sub-dissipation decay to zero and finitely many rungs below any scale. It fills a basic step in the phi-ladder cutoff argument for Navier-Stokes regularity, consistent with the forced eight-tick octave and three spatial dimensions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.