phiRungScale_strictMono
plain-language theorem explainer
The theorem establishes that the φ-rung scale function is strictly increasing: smaller rung indices produce strictly smaller scales. Workers on the Navier-Stokes regularity argument via the φ-ladder cutoff cite it to guarantee that scales grow without bound and that only finitely many rungs lie below any given energy threshold. The proof is a one-line term application of the power strict monotonicity lemma for bases greater than one.
Claim. Let $1 < phi$ be the golden ratio. The φ-rung scale function satisfies $m < n implies phi^m < phi^n$ for natural numbers $m, n$.
background
In the module on Navier-Stokes regularity from the φ-ladder cutoff, the φ-rung scale assigns to each rung index $k$ the value $phi^k$. This construction sits inside Recognition Science where phi arises as the self-similar fixed point and the discrete lattice supplies an ultraviolet cutoff for energy cascades. The supporting lemma one_lt_phi establishes the base inequality $1 < phi$. The module also introduces J-cost functions that measure recognition defects and proves they are nonnegative with equality only at unity.
proof idea
The proof is a direct term-mode application of the power monotonicity lemma. It introduces the assumption $a < b$ and then invokes pow_lt_pow_right₀ at base phi using the fact one_lt_phi.
why it matters
This result is required for the subsequent claims that only finitely many rungs lie below any scale and that cascade depth is monotone in Reynolds number. It fills item 3 in the module's main results list for the paper NS_Regularity_Phi_Ladder_Cutoff.tex. Within the Recognition framework it secures the ultraviolet cutoff property of the discrete φ-ladder, preventing infinite cascades in the Navier-Stokes energy transfer.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.