phiRungScale_succ
plain-language theorem explainer
The recursive scaling property states that the φ-rung length at level n+1 equals φ times the length at level n. Analysts formalizing the Navier-Stokes energy cascade cutoff on the Recognition Science lattice cite this to confirm geometric progression of the discrete scales. The proof is a direct one-line algebraic reduction that substitutes the power definition and applies the exponent successor rule.
Claim. For every natural number $n$, the φ-rung scale satisfies $S(n+1) = φ · S(n)$, where $S(n) := φ^n$ is the relative length of the nth rung on the discrete lattice.
background
The module formalizes the algebraic core of the Navier-Stokes regularity argument in which the φ-ladder supplies an ultraviolet cutoff that terminates the energy cascade on the RS discrete lattice. The upstream definition states that the scale at φ-rung n, relative to the voxel scale ℓ₀, is given explicitly by phiRungScale n := phi^n. This supplies the geometric sequence whose positivity, monotonicity, and finite truncation below any fixed scale are established in the same file.
proof idea
The proof is a one-line term-mode wrapper. It unfolds the definition of phiRungScale to replace the left-hand side by phi^(n+1), rewrites the successor power via the rule phi^(n+1) = phi * phi^n, and closes the equality by ring normalization.
why it matters
The relation supplies the inductive step needed for the monotonicity and positivity lemmas that feed the cascade-depth function N_d = ⌊(3/4) ln(Re)/ln(φ)⌋. It realizes the self-similar fixed-point scaling forced at T6 of the UnifiedForcingChain and thereby closes the combinatorial scaffolding for the finite-rung termination claim in the NS_Regularity_Phi_Ladder_Cutoff paper.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.