cascadeDepth_finite
plain-language theorem explainer
The theorem shows that the cascade depth function, given by the floor of three-quarters times the natural log of the Reynolds number divided by the natural log of phi for values above 1 and zero otherwise, always returns a natural number. Researchers formalizing the phi-ladder ultraviolet cutoff for Navier-Stokes regularity cite this to guarantee that the energy cascade reaches a finite rung count. The proof is a direct term construction that uses the definition itself as the witness together with reflexivity.
Claim. For every real number $re$, there exists a natural number $N$ such that the cascade depth at $re$ equals $N$, where the cascade depth equals $0$ when $re ≤ 1$ and equals $⌊(3/4) ln(re) / ln(φ)⌋$ otherwise.
background
The module develops the algebraic and combinatorial basis for using the phi-ladder as an ultraviolet cutoff that ends the Navier-Stokes energy cascade on the discrete lattice of Recognition Science. Cascade depth is the integer defined by flooring (3/4) times the natural log of the Reynolds number over the natural log of phi when the Reynolds number exceeds 1, otherwise zero. This rests on the definition of cascade depth and connects to earlier results such as the nonnegativity of J-cost and the positivity of phi-rung scales listed in the module documentation.
proof idea
The proof is a one-line term proof. It supplies the value returned by the cascade depth definition as the existential witness and closes with reflexivity on the equality.
why it matters
This result provides the finite cascade certificate to the main PhiLadderCutoffCert definition. It ensures the energy cascade involves only finitely many rungs, supporting the termination argument in the Navier-Stokes regularity paper. The finite depth aligns with the discrete structure enforced by the eight-tick octave in the Recognition Science forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.