phiRungScale_succ
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.
claimFor 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 in Recognition Science
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.
scope and limits
- Does not prove positivity or strict increase of the scales.
- Does not relate the scales to Reynolds number or dissipation rate.
- Does not establish convergence of any associated series.
- Does not address uniqueness of the φ-ladder construction.
formal statement (Lean)
89theorem phiRungScale_succ (n : ℕ) :
90 phiRungScale (n + 1) = phi * phiRungScale n := by
proof body
Term-mode proof.
91 unfold phiRungScale; rw [pow_succ]; ring
92
93/-! ## Cascade Depth -/
94
95/-- The cascade depth: N_d = ⌊(3/4) · ln(Re) / ln(φ)⌋. -/