cascadeDepth
The cascade depth maps a Reynolds number Re to a natural number N_d given by the floor of (3/4) times ln(Re) over ln(phi) when Re exceeds 1, and zero otherwise. Navier-Stokes analysts working on regularity via the Recognition Science lattice cite this integer to bound the length of the energy cascade. The definition is supplied directly by a case distinction on the threshold Re > 1.
claim$N_d(Re) := 0$ if $Re ≤ 1$, and $N_d(Re) := ⌊(3/4) · (ln Re / ln φ)⌋$ otherwise.
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 discrete lattice. Jcost records the recognition cost function J(x) ≥ 0 with equality only at x = 1. phiRungScale produces the strictly increasing positive sequence of rung lengths on the ladder. The local setting is the φ-ladder cutoff argument for Navier-Stokes regularity, with the cascade depth supplying the integer depth N_d that appears in the packaged certificate.
proof idea
The definition proceeds by direct case split. When Re ≤ 1 the value is set to zero. When Re > 1 it computes the floor of the scaled logarithm (3/4) · (log Re / log phi).
why it matters in Recognition Science
This definition supplies the integer depth that enters the certificate PhiLadderCutoffCert packaging Jcost nonnegativity, the zero-iff property, finiteness, and monotonicity. It fills the combinatorial step in the paper NS_Regularity_Phi_Ladder_Cutoff.tex that the φ-ladder terminates the cascade. The construction sits inside the Recognition Science forcing chain that forces D = 3 and the eight-tick octave.
scope and limits
- Does not derive the numerical prefactor 3/4 from the forcing chain.
- Does not prove existence or uniqueness of Navier-Stokes solutions.
- Does not address the physical interpretation of the Reynolds number threshold.
- Does not connect the depth to explicit dissipation rates.
formal statement (Lean)
96def cascadeDepth (re : ℝ) : ℕ :=
proof body
Definition body.
97 if 1 < re then
98 Nat.floor ((3/4 : ℝ) * Real.log re / Real.log phi)
99 else 0
100
101/-- The cascade depth is zero for Re ≤ 1. -/