r_orbit_succ
plain-language theorem explainer
The successor relation asserts that the orbital radius at rung k+1 equals the radius at rung k multiplied by the golden ratio phi. Modelers of protoplanetary disks citing the J-cost derivation of the Titius-Bode law would invoke this step to establish the multiplicative ladder. The proof reduces directly to the power definition of the radius function via unfolding and ring simplification.
Claim. $r_0(k+1) = r_0(k) · ϕ$ where $r_0(k) := r_0 · ϕ^k$ for real scale $r_0 > 0$ and natural number $k$.
background
The function r_orbit(r0, k) is defined as r0 multiplied by phi to the power k, representing stable orbital radii on the phi-ladder in a protoplanetary disk minimizing J-cost on radial bond density. This module derives planetary formation from the Recognition Composition Law and the self-similar fixed point phi forced in T6 of the unified forcing chain. Upstream results supply the base definition of r_orbit together with the constant phi and the anchor scale r0 from mass-sector geometry.
proof idea
The term proof unfolds the definition of r_orbit, rewrites the successor exponent via pow_succ, and closes by ring normalization.
why it matters
This lemma supports the adjacent-ratio theorem r_orbit_adjacent_ratio, which confirms the ratio is exactly phi, and the strict-monotonicity result r_orbit_strict_mono. It fills the structural prediction step in the Titius-Bode derivation from J-cost minimization, linking directly to the self-similar fixed point of T6 and the eight-tick octave.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.