pith. sign in
module module high

IndisputableMonolith.NavierStokes.PhiOptimalCascade

show as:
view Lean formalization →

This module defines the self-similarity defect ratio for geometric cascades and related cost functions in the Recognition Science treatment of Navier-Stokes regularity. Researchers studying the phi-ladder ultraviolet cutoff for energy cascades on the RS lattice would cite it. The module consists of core definitions together with lemmas on positivity, uniqueness at phi, and optimality.

claimLet $r>1$ be a cascade ratio. The self-similarity defect ratio is the function $d(r)$ with $d(r)=0$ precisely when $r=phi$, and the simplified cascade cost is the associated nonnegative function $C(r)$ that vanishes only at the same point.

background

In Recognition Science the phi-ladder supplies a discrete ultraviolet cutoff that terminates the Navier-Stokes energy cascade on the RS lattice. The upstream PhiLadderCutoff module states: 'This module formalizes the algebraic and combinatorial core of the argument that the φ-ladder provides an ultraviolet cutoff terminating the Navier-Stokes energy cascade on the RS discrete lattice.' Constants supplies the base time quantum tau_0 = 1 tick and the J-cost function used to measure deviations from self-similarity. This module introduces the defect ratio and simplified cost to quantify how far a given ratio departs from the optimal phi value.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The module supplies the algebraic core that feeds the main regularity claim of the PhiLadderCutoff module. It establishes that phi is the unique ratio minimizing cascade cost, thereby closing the combinatorial step in the argument that the phi-ladder terminates the energy cascade. No downstream uses are recorded yet.

scope and limits

depends on (2)

Lean names referenced from this declaration's body.

declarations in this module (10)