finitely_many_rungs_below
plain-language theorem explainer
For any fixed real scale L the φ-ladder contains only finitely many rungs below it. Navier-Stokes regularity arguments that rely on the Recognition Science cutoff cite this finiteness result. The proof extracts N from the standard limit φ^n → ∞ as n → ∞, which follows from φ > 1.
Claim. For every real number $L$, there exists a natural number $N$ such that $L ≤ φ^n$ holds for every natural number $n ≥ N$, where $φ$ is the golden ratio and the rung scale at level $n$ is $φ^n$.
background
The module formalizes the φ-ladder cutoff for Navier-Stokes regularity on the RS discrete lattice. The rung scale at level n is defined by phiRungScale n := φ^n and is positive and strictly increasing. Upstream results establish 1 < φ, which guarantees that its powers diverge to infinity. This sits inside the Recognition Science derivation where φ arises as the self-similar fixed point.
proof idea
The argument invokes the tendsto fact for powers: since 1 < φ, φ^n tends to infinity at infinity. It rewrites this as the atTop_atTop property, picks N large enough that φ^n exceeds the ceiling of L for n ≥ N, and concludes via the inequality L ≤ ⌈L⌉₊.
why it matters
This finiteness statement is assembled into the main certificate phiLadderCutoff, which collects the J-cost properties, the decay factor, and the cascade depth results. It supplies the ultraviolet termination needed for the regularity claim in the paper NS_Regularity_Phi_Ladder_Cutoff. Within the framework it closes the finite-depth cascade consistent with the eight-tick structure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.