sub_dissipation_decay_to_zero
plain-language theorem explainer
The geometric sequence with ratio equal to the sub-dissipation decay factor converges to zero at infinity. Workers on the phi-ladder cutoff for Navier-Stokes regularity would cite this to confirm that residual energy vanishes after finitely many rungs below dissipation. The proof is a one-line wrapper applying the standard tendsto_pow_atTop_nhds_zero_of_lt_one lemma once positivity and the strict bound less than one are supplied.
Claim. Let $r := phi^{-2}$ be the sub-dissipation decay factor. Then the sequence $r^k$ tends to 0 in the neighborhood filter as $k$ tends to infinity.
background
The module formalizes the algebraic core of the claim that the phi-ladder supplies an ultraviolet cutoff terminating the Navier-Stokes energy cascade on the RS discrete lattice. The sub-dissipation decay factor is defined as $phi^{-1}^2$, the energy decay ratio below the dissipation scale. Upstream results establish that this factor is positive and strictly less than one, using the property that $phi > 1$.
proof idea
The proof is a one-line wrapper that applies tendsto_pow_atTop_nhds_zero_of_lt_one, passing the positivity of subDissipationDecayFactor and the strict inequality subDissipationDecayFactor_lt_one as arguments.
why it matters
This result is assembled into the main phiLadderCutoff certificate that collects Jcost nonnegativity, cascade finiteness, and decay bounds. It closes the step showing energy is strictly less than one after k rungs below dissipation, as listed among the module's main results. Within the Recognition framework it supports the phi-ladder ultraviolet cutoff that follows from the self-similar fixed point and eight-tick octave structure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.