r_orbit_closed
plain-language theorem explainer
The closed-form expression for stable orbital radius at rung k is the inner reference scale times phi to the power k. Astrophysicists deriving Titius-Bode ratios from J-cost minimization on protoplanetary disks cite this when recovering the phi-ladder from self-similar bond costs. The proof is a one-line reflexivity on the definition of r_orbit.
Claim. For any real number $r_0$ and natural number $k$, the stable orbital radius at rung $k$ satisfies $r_0(k) = r_0 phi^k$.
background
r_orbit is the stable orbital radius at rung k for inner-reference scale r0, defined explicitly as r0 times phi to the k. The module treats a protoplanetary disk as minimizing J-cost on radial bond density, forcing orbits onto a phi-multiplicative ladder by the same self-similarity that fixes phi in T6. This rests on the rung definition from arithmetic and spectroscopy modules together with the canonical arithmetic object.
proof idea
The proof is a one-line wrapper that applies reflexivity to the definition of r_orbit.
why it matters
This supplies the closed form required by planetaryFormationCert, which collects the structural properties for the Titius-Bode prediction. It fills the recognition-cost derivation of the Titius-Bode pattern from T6 plus disc J-cost minimization, with only the single overall scale r0 free. The result operates inside the eight-tick octave and D=3 landmarks of the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.