phiRungScale_strictMono
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.
claimLet $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 in Recognition Science
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.
scope and limits
- Does not establish the definition of the φ-rung scale function.
- Does not prove positivity of the scales.
- Does not connect to the full Navier-Stokes equations.
- Does not address convergence of the decay series.
formal statement (Lean)
84theorem phiRungScale_strictMono : StrictMono phiRungScale := by
proof body
Term-mode proof.
85 intro a b hab
86 exact pow_lt_pow_right₀ one_lt_phi hab
87
88/-- φ-rung scale at n+1 equals φ times the scale at n. -/