subDissipationDecayFactor_lt_one
plain-language theorem explainer
The sub-dissipation decay factor equals the square of the reciprocal of the golden ratio. Navier-Stokes analysts applying the Recognition Science phi-ladder cutoff cite this result to bound energy loss below the dissipation scale. The proof is a term-mode reduction that unfolds the definition, invokes the upstream fact that the golden ratio exceeds one, and closes via non-linear arithmetic.
Claim. Let $phi > 1$ be the golden ratio. The energy decay ratio below the dissipation scale satisfies $phi^{-2} < 1$.
background
The module formalizes the algebraic core of Navier-Stokes regularity from the phi-ladder ultraviolet cutoff on the RS discrete lattice. Relevant definitions include the J-cost function obeying the Recognition Composition Law J(xy) + J(x/y) = 2J(x)J(y) + 2J(x) + 2J(y), together with phi-rung scales that are positive and strictly monotone. The sub-dissipation decay factor is defined explicitly as phi^{-1}^2, the energy decay ratio below the dissipation scale. The lemma depends on the upstream result one_lt_phi asserting 1 < phi.
proof idea
The term proof unfolds subDissipationDecayFactor to phi^{-1}^2. It applies the lemma one_lt_phi to obtain phi^{-1} < 1 via inv_lt_one_of_one_lt_0. The argument closes with nlinarith using sq_nonneg (1 - phi^{-1}) and inv_pos.mpr phi_pos.
why it matters
This result is assembled into the main certificate phiLadderCutoff (zero sorry) and directly enables the convergence theorem sub_dissipation_decay_to_zero together with sub_dissipation_energy_decays. It supports termination of the energy cascade after finitely many rungs, consistent with the Recognition Science forcing chain (T5 J-uniqueness through T8 D = 3) and the phi-ladder cutoff in the cited paper.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.