subDissipationDecayFactor_pos
plain-language theorem explainer
The positivity of the sub-dissipation decay factor, defined as φ^{-2} with φ the self-similar fixed point, is established to anchor decay estimates in the φ-ladder cutoff for Navier-Stokes regularity. Researchers analyzing discrete energy cascades in fluid models would cite this result when bounding sub-dissipation terms. The proof is a one-line term that invokes pow_pos after confirming the inverse of φ is positive.
Claim. $0 < φ^{-2}$, where φ is the self-similar fixed point of the Recognition Composition Law and the decay factor is the energy ratio below the dissipation scale.
background
The module formalizes the algebraic core of Navier-Stokes regularity via the φ-ladder cutoff on the RS discrete lattice. subDissipationDecayFactor is defined as φ^{-1}^2, the energy decay ratio below the dissipation scale. This sits among sibling results on Jcost nonnegativity, Jcost zero only at unity, and phiRungScale positivity and strict monotonicity.
proof idea
The proof is a one-line term wrapper that applies pow_pos to the square of φ^{-1}. It first obtains 0 < φ^{-1} via inv_pos.mpr applied to the upstream positivity of φ, then raises the result to the second power.
why it matters
This supplies the strict positivity hypothesis required by the parent theorems sub_dissipation_decay_to_zero (which shows iterated decay tends to zero) and sub_dissipation_energy_decays (which bounds energy below unity after one rung). It fills the positivity step in the φ-ladder cutoff argument for Navier-Stokes regularity, consistent with the Recognition Science forcing chain at T6 (phi fixed point) and T7 (eight-tick octave). No open scaffolding is touched.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.