pith. sign in
def

cascadeDepth

definition
show as:
module
IndisputableMonolith.NavierStokes.PhiLadderCutoff
domain
NavierStokes
line
96 · github
papers citing
none yet

plain-language theorem explainer

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

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.

Switch to Lean above to see the machine-checked source, dependencies, and usage graph.