cascadeDepth_le_one
plain-language theorem explainer
The declaration shows that the cascade depth vanishes for Reynolds numbers at most one. Workers on the φ-ladder ultraviolet cutoff for Navier-Stokes would invoke this bound to terminate the energy cascade in the laminar regime. Its proof is a one-line term that unfolds the piecewise definition of cascadeDepth and simplifies using the supplied inequality.
Claim. If the Reynolds number satisfies $Re ≤ 1$, then the cascade depth $N_d(Re) = 0$, where $N_d(Re)$ equals zero for $Re ≤ 1$ and equals $⌊(3/4) ln(Re)/ln(φ)⌋$ otherwise.
background
This result belongs to the module formalizing Navier-Stokes regularity via the φ-ladder cutoff on the RS discrete lattice. The cascade depth $N_d$ is defined as zero whenever $Re ≤ 1$ and otherwise as the floor of $(3/4) · ln(Re) / ln(φ)$. The module also introduces Jcost (nonnegative and zero only at unity) and phiRungScale (positive and strictly monotone), which supply the rung counting that $N_d$ discretizes.
proof idea
The proof is a one-line term-mode wrapper. It unfolds the definition of cascadeDepth, which selects the zero branch under the hypothesis re ≤ 1, and applies simp with the fact that not (1 < re) follows from the hypothesis.
why it matters
This lemma supplies the base case for cascade depth in the φ-ladder argument for Navier-Stokes regularity. It ensures the energy cascade terminates immediately for subcritical Reynolds numbers, aligning with the eight-tick octave and D = 3 in the Recognition Science framework. It supports the module's listed results on sub_dissipation_decay_to_zero and cascadeDepth_mono.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.