r_orbit_adjacent_ratio
plain-language theorem explainer
Adjacent rungs on the φ-ladder for orbital radii satisfy r(k+1)/r(k) = φ exactly for any positive scale r0. Planetary formation models cite this to obtain the Titius-Bode pattern as a zero-parameter structural prediction from J-cost minimisation. The short term proof applies the successor lemma for the orbit function and cancels the common positive factor via field simplification.
Claim. For any positive real $r_0$ and natural number $k$, if $r(k) := r_0 φ^k$, then $r(k+1)/r(k) = φ$.
background
In the Recognition Science treatment of planetary formation, orbital radii minimise J-cost when they lie on the multiplicative ladder $r(k) = r_0 φ^k$. The function r_orbit is defined directly as this product, with positivity following from the positivity of r0 and φ. The successor relation r_orbit(r0, k+1) = r_orbit(r0, k) * φ is established by unfolding the power and applying ring arithmetic.
proof idea
The proof first establishes positivity of the k-th radius via the dedicated positivity lemma. It then rewrites the (k+1) term using the successor theorem, which expands the power, and finally cancels the common positive factor with field simplification.
why it matters
This lemma supplies the exact adjacent ratio required by the PlanetaryFormationCert structure, which in turn feeds the one-statement summary of planetary formation. It closes the structural prediction that adjacent rungs differ by exactly φ, consistent with the self-similar fixed point forced in T6. The result supports the empirical adjudication against JPL data for the Solar System.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.