r_orbit_gap_skip_band
plain-language theorem explainer
The declaration shows that the orbital radius ratio skipping one rung on the phi-ladder lies strictly between 2.5 and 2.7. Protoplanetary-disk modelers cite it to derive the asteroid-belt gap from J-cost minimization. The proof reduces the ratio algebraically to phi squared via unfolding and field simplification, then applies the pre-established bounds lemma.
Claim. Let $r(k) = r_0 phi^k$ for positive real $r_0$ and natural number $k$. Then $2.5 < r(k+2)/r(k) < 2.7$.
background
The module defines the stable orbital radius at rung $k$ as $r_0 phi^k$. This follows from J-cost minimization on radial bond density in a protoplanetary disk, which forces self-similar spacing by the fixed point phi from T6. The upstream lemma phi_squared_bounds states that phi squared lies between 2.5 and 2.7, with the exact value phi plus one. The module derives the Titius-Bode pattern as a structural prediction with no free parameters beyond the overall scale r0.
proof idea
The tactic proof obtains positivity of the denominator radius via the r_orbit_pos lemma. It then unfolds the radius definition, applies pow_add and field_simp to reduce the ratio exactly to phi squared, and invokes the phi_squared_bounds lemma to finish.
why it matters
This result feeds the PlanetaryFormationCert structure and the planetary_formation_one_statement theorem. It supplies the gap-skip identity (Mars to Jupiter) required for the full ladder description, closing the asteroid-belt prediction at rung 4. The argument rests on the self-similarity forced in T6 and the Recognition Composition Law.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.