cascadeDepth_mono
plain-language theorem explainer
Cascade depth counts the number of φ-rungs below a given Reynolds number and increases monotonically with Re. Workers on the Recognition Science account of Navier-Stokes regularity cite this to bound the depth of the energy cascade before the lattice cutoff. The argument is a direct term proof that reduces the claim to the monotonicity of the real logarithm and the floor function.
Claim. If $1 < Re_1 ≤ Re_2$, then the number of φ-rungs below the scale set by $Re_1$ is at most the number below the scale set by $Re_2$.
background
The module formalizes the algebraic core of the claim that the φ-ladder supplies an ultraviolet cutoff terminating the Navier-Stokes energy cascade on the RS discrete lattice. Cascade depth is the integer part of log(Re)/log(φ), using the scale function that places rung k at φ^k. Key supporting definitions are J-cost (nonnegative, zero only at unity) from the PhiForcingDerived structure and the strict increase of φ-rung scales.
proof idea
Unfold cascadeDepth. The hypothesis yields 1 < Re2. Apply Nat.floor_le_floor to reduce to log(Re1)/log(φ) ≤ log(Re2)/log(φ). This follows from log_le_log on Re1 ≤ Re2, positivity of log(φ) from one_lt_phi, and division by the positive constant log(φ) via div_le_div_of_nonneg_right.
why it matters
The monotonicity is assembled into phiLadderCutoff, the main certificate that collects Jcost nonnegativity, zero-iff, finite rungs, monotonicity and decay. It supplies the combinatorial step showing the φ-ladder (self-similar fixed point at T6) terminates the cascade at finite depth, consistent with the eight-tick octave and D=3. It closes the finiteness part of the NS regularity argument in the referenced paper.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.