subDissipationDecayFactor
The sub-dissipation decay factor is defined as φ^{-2} and supplies the per-rung energy reduction below the dissipation threshold on the φ-ladder. Analysts deriving Navier-Stokes regularity via the Recognition Science cutoff cite this constant when bounding cascade convergence. The definition is a direct algebraic assignment using the inverse golden ratio raised to the second power.
claimThe energy decay ratio below the dissipation scale is defined by $δ = φ^{-2}$, where $φ$ denotes the golden ratio fixed point.
background
The module formalizes the algebraic core of the φ-ladder ultraviolet cutoff terminating the Navier-Stokes energy cascade on the RS discrete lattice. Supporting definitions include Jcost, satisfying Jcost(x) ≥ 0 for x > 0 with equality precisely when x = 1, and phiRungScale, which are positive and strictly monotone. The local setting is given by the module statement that the φ-ladder provides the cutoff, with main results covering Jcost nonnegativity, phiRungScale monotonicity, and cascade finiteness.
proof idea
Direct definition as the square of the inverse of phi, with no lemmas or tactics applied beyond the constant expression.
why it matters in Recognition Science
This definition supplies the decay ratio referenced by PhiLadderCutoffCert and by the theorems subDissipationDecayFactor_lt_one, sub_dissipation_decay_to_zero, and sub_dissipation_energy_decays. It fills the ultraviolet cutoff step in the Recognition Science argument for Navier-Stokes regularity, consistent with the φ-ladder and eight-tick octave structure. The parent certificate packages it together with Jcost nonnegativity and cascade monotonicity.
scope and limits
- Does not establish full Navier-Stokes regularity or existence of smooth solutions.
- Does not derive the numerical value of phi or its forcing from T0-T8.
- Does not address external forcing terms or boundary conditions.
- Does not quantify the Reynolds number dependence beyond the cascade depth.
formal statement (Lean)
140def subDissipationDecayFactor : ℝ := phi⁻¹ ^ 2
proof body
Definition body.
141
142/-- The decay factor is positive. -/