phiRungWavenumber_succ
plain-language theorem explainer
The declaration establishes the recursive relation for rung wavenumbers in the φ-ladder: the wavenumber at rung n+1 equals φ^{-1} times the wavenumber at rung n. Researchers analyzing the Recognition Science derivation of Navier-Stokes regularity would cite this when tracking the geometric decrease along the ladder steps. The proof is a one-line term-mode reduction that unfolds the definition and applies the power successor rule followed by ring simplification.
Claim. For every natural number $n$, the wavenumber at rung $n+1$ satisfies $k_{n+1} = φ^{-1} k_n$, where $k_n = φ^{-1 n}$ denotes the wavenumber at rung $n$ in units of the base wavenumber $k_0$.
background
In the Navier-Stokes module the φ-ladder supplies a discrete ultraviolet cutoff that terminates the energy cascade on the RS lattice. The function phiRungWavenumber maps each natural-number rung index $n$ to the real value $φ^{-1}^n$, giving the wavenumber at that rung in units of $k_0$. The module lists seven main results that together show energy decay below dissipation and finite cascade depth; this recurrence is the algebraic step that makes the geometric contraction explicit.
proof idea
The term proof unfolds the definition phiRungWavenumber(n) := φ^{-1}^n, rewrites the successor exponent via pow_succ to obtain φ^{-1}^{n+1} = φ^{-1} · φ^{-1}^n, and closes with the ring tactic.
why it matters
This supplies the basic recurrence for rung wavenumbers required by later results in the same module such as subDissipationDecayFactor_lt_one, sub_dissipation_decay_to_zero, and cascadeDepth_mono. It directly supports the claim that the φ-ladder terminates the Navier-Stokes cascade, aligning with the T7 eight-tick octave and D = 3 spatial dimensions of the Recognition Science forcing chain. The paper NS_Regularity_Phi_Ladder_Cutoff.tex lists it among the core algebraic identities.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.