subDissipationDecayFactor
plain-language theorem explainer
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.
Claim. The 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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.