phiRungWavenumber
plain-language theorem explainer
The wavenumber at rung n equals the inverse golden ratio raised to the power n, expressed in units of the base wavenumber. Analysts of the φ-ladder ultraviolet cutoff for Navier-Stokes regularity reference this definition when discretizing cascade scales. It is introduced via a direct power expression without additional lemmas.
Claim. The wavenumber at rung $n$ (in units of $k_0$) is given by $k_n = phi^{-n}$, where $phi$ denotes the golden ratio.
background
The module formalizes the algebraic and combinatorial core of the argument that the φ-ladder provides an ultraviolet cutoff terminating the Navier-Stokes energy cascade on the RS discrete lattice. Supporting definitions include Jcost, which is nonnegative and vanishes only at unity, and phiRungScale, which is positive and strictly monotone. Rung is an abbrev for the type of possibly fractional rungs on the φ-ladder, given by ℚ.
proof idea
The declaration is a direct definition setting the wavenumber equal to the n-th power of the inverse golden ratio. It requires no lemmas and acts as the base case for the subsequent positivity and recurrence theorems.
why it matters
This supplies the wavenumber scaling that supports the module's results on sub-dissipation decay and finite rungs below any scale. It connects to the Recognition Science framework through the phi self-similar fixed point in the forcing chain, enabling the discrete structure for the energy cascade termination. The definition is used by the theorems establishing positivity, the successor relation, and anti-monotonicity of the wavenumbers.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.