cascadeDepth_mono
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.
claimIf $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 in Recognition Science
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.
scope and limits
- Does not apply when Re ≤ 1.
- Does not compute explicit numerical values of cascade depth.
- Does not address the physical dissipation mechanism at the cutoff.
- Does not prove regularity of the Navier-Stokes equations.
formal statement (Lean)
110theorem cascadeDepth_mono {re₁ re₂ : ℝ} (h1 : 1 < re₁) (h2 : re₁ ≤ re₂) :
111 cascadeDepth re₁ ≤ cascadeDepth re₂ := by
proof body
Term-mode proof.
112 have h2' : 1 < re₂ := lt_of_lt_of_le h1 h2
113 unfold cascadeDepth; simp [h1, h2']
114 apply Nat.floor_le_floor
115 apply div_le_div_of_nonneg_right
116 · apply mul_le_mul_of_nonneg_left
117 · exact Real.log_le_log (by linarith) h2
118 · norm_num
119 · exact le_of_lt (Real.log_pos one_lt_phi)
120
121/-! ## Finiteness of the Cascade -/
122
123/-- The φ-ladder has finitely many rungs below any fixed scale.
124 Since φ > 1, φⁿ → ∞. -/