phiRungScale
plain-language theorem explainer
phiRungScale defines the scale at φ-rung n as φ^n relative to the base voxel scale. Analysts of the Navier-Stokes regularity argument via φ-ladder cutoff cite it when bounding cascade depth on the discrete lattice. The definition is a direct power expression that immediately supports application of standard power lemmas for growth and ordering.
Claim. Let φ be the golden ratio fixed point. The scale at the nth rung of the φ-ladder is φ^n.
background
The module formalizes the algebraic core of the claim that the φ-ladder supplies an ultraviolet cutoff terminating the Navier-Stokes energy cascade on the RS discrete lattice. Supporting results include Jcost_nonneg (J(x) ≥ 0 for x > 0) and Jcost_eq_zero_iff (J(x) = 0 only at x = 1). The rung concept appears in upstream mass and spectroscopy definitions, where it assigns integer levels to fermions or ore classes, but the present scaling uses exponential growth in φ.
proof idea
The declaration is a direct definition as phi raised to n. Downstream results such as phiRungScale_pos apply pow_pos and phiRungScale_strictMono apply pow_lt_pow_right₀ directly to this expression.
why it matters
It supplies the explicit scaling used by finitely_many_rungs_below to obtain finite N such that scales exceed any fixed L, and by PhiLadderCutoffCert to certify finite cascade depth for any Reynolds number. This completes the combinatorial step in the NS regularity argument from the φ-ladder cutoff paper, connecting to the forced φ from T6 and the eight-tick octave from T7.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.