cascadeDepth_le_one
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.
claimIf 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 in Recognition Science
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.
scope and limits
- Does not address the value of cascade depth for Re > 1.
- Does not derive the floor expression from first principles.
- Does not connect directly to J-cost or dissipation decay factors.
formal statement (Lean)
102theorem cascadeDepth_le_one {re : ℝ} (h : re ≤ 1) : cascadeDepth re = 0 := by
proof body
Term-mode proof.
103 unfold cascadeDepth; simp [not_lt.mpr h]
104
105/-- The cascade depth is always a concrete natural number. -/