two_rung_gap_eq_phi_squared
plain-language theorem explainer
The theorem states that orbital radius at rung k+2 equals radius at rung k scaled by phi squared. Astrophysicists working on J-cost minimization in protoplanetary disks cite it to account for observed gaps such as Mars to Jupiter. The proof is a direct algebraic reduction from the definition of orbital radius using exponent rules and ring simplification.
Claim. For any real number $r_0$ and natural number $k$, the stable orbital radius at rung $k+2$ equals the stable orbital radius at rung $k$ multiplied by $phi^2$.
background
The module derives planetary orbital radii from J-cost minimization on radial bond density in a protoplanetary disk. The central definition is the stable orbital radius at rung $k$ for inner-reference scale $r_0$, given explicitly by $r_0$ times $phi$ to the power $k$. This construction follows from the self-similar fixed point that forces $phi$ under bond-cost minimisation (T6 in the forcing chain).
proof idea
The proof is a term-mode reduction. It unfolds the definition of orbital radius, rewrites the two successor powers via the successor exponent rule, and closes with the ring tactic.
why it matters
This identity supplies the two-rung gap step required for the phi-ladder model of planetary formation (Track R3). It directly supports the half-rung tolerance band used for empirical checks against JPL data. The result rests on the Recognition Composition Law and the self-similar forcing of $phi$, while the module places it inside the eight-tick octave scaling.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.