phiRungScale_pos
plain-language theorem explainer
φ-rung scales are positive for every natural number n. Researchers formalizing the Navier-Stokes regularity argument via the φ-ladder cutoff cite this to guarantee that all energy scales on the discrete lattice remain well-defined and positive. The proof is a one-line term application of the lemma that positive bases raised to natural powers stay positive.
Claim. For every natural number $n$, the φ-rung scale satisfies $0 < φ^n$.
background
The module formalizes the algebraic and combinatorial core of the claim that the φ-ladder supplies an ultraviolet cutoff that terminates the Navier-Stokes energy cascade on the RS discrete lattice. The central definition is phiRungScale n := φ^n, the scale at rung n relative to the voxel scale ℓ₀. The module lists this positivity result among its main results alongside J-cost non-negativity, strict monotonicity of the scales, and decay of sub-dissipation factors to zero.
proof idea
The proof is a one-line term that applies the lemma pow_pos to the fact that φ > 0 (phi_pos) and the natural exponent n.
why it matters
This theorem supplies one of the listed main results in the Navier-Stokes regularity paper, ensuring positive scales for the subsequent decay and finiteness arguments. It feeds the parent results subDissipationDecayFactor_lt_one, sub_dissipation_decay_to_zero, and cascadeDepth_mono inside the same module. In the Recognition Science setting it anchors the φ-ladder construction (T6 self-similar fixed point) that yields the discrete UV cutoff for the energy cascade.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.