phiRungScale
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.
claimLet φ 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 in Recognition Science
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.
scope and limits
- Does not prove positivity of the scales.
- Does not establish strict monotonicity.
- Does not assign specific rung values to particles or sectors.
- Does not derive φ from the recognition composition law.
formal statement (Lean)
77def phiRungScale (n : ℕ) : ℝ := phi ^ n
proof body
Definition body.
78
79/-- φ-rung scales are positive. -/