phiRungWavenumber_pos
plain-language theorem explainer
The theorem states that the wavenumber at rung n on the phi-ladder is strictly positive for every natural number n. Workers on the Navier-Stokes regularity argument via phi-ladder cutoff cite it to guarantee that every scale in the discrete energy cascade is well-defined and positive. The proof is a one-line application of the positivity of integer powers of a positive real.
Claim. For every natural number $n$, the wavenumber at rung $n$ (in units of $k_0$) satisfies $0 < (phi^{-1})^n$.
background
The module formalizes the algebraic core of the claim that the phi-ladder supplies an ultraviolet cutoff that terminates the Navier-Stokes energy cascade on the RS discrete lattice. Key supporting definitions include phiRungWavenumber, which sets the wavenumber at rung n to phi inverse to the power n, and the family of Jcost lemmas that establish non-negativity and zero only at unity. Upstream results supply the definition of rung in multiple contexts (Fermion masses, asteroid ore classes, anchor policies) but the immediate dependency is the phiRungWavenumber definition itself together with the positivity of phi.
proof idea
The proof is a direct term-mode application of pow_pos to the positive base obtained from inv_pos.mpr phi_pos.
why it matters
Positivity of rung wavenumbers is required for the subsequent results listed in the module (subDissipationDecayFactor_lt_one, finitely_many_rungs_below, cascadeDepth_mono) that close the ultraviolet cutoff argument. It sits inside the phi-ladder construction that supplies the discrete scales used throughout Recognition Science, consistent with the eight-tick octave and the self-similar fixed point phi.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.