planetary_formation_one_statement
plain-language theorem explainer
The declaration establishes that stable orbital radii in a protoplanetary disk follow the geometric progression r(k) = r0 * phi^k for r0 > 0. This yields positivity for all natural k, exact adjacent ratios of phi, strict increase, and gap-skip ratios confined to (2.5, 2.7). Modelers of disk dynamics from recognition-cost minimization cite it for its parameter-free derivation of the Titius-Bode pattern. The proof packages four supporting lemmas on the orbit function into a single conjunction.
Claim. For $r_0 > 0$ and $k$ a natural number, let $r(k) := r_0 phi^k$. Then $r(k) > 0$, $r(k+1)/r(k) = phi$, $r(k) < r(k+1)$, and $2.5 < r(k+2)/r(k) < 2.7$.
background
The module derives orbital radii from J-cost minimization on radial bond density in a protoplanetary disk. The definition r_orbit(r0, k) sets the stable radius at rung k to r0 multiplied by phi to the power k, where phi is the self-similar fixed point forced in T6. The local setting treats the disk as minimizing recognition cost, so neighboring stable orbits must occur at r/phi and r*phi to avoid positive J-cost mismatch on the standing-wave pattern. This supplies the first-principles account of the Titius-Bode pattern with only one free scale r0. Upstream lemmas establish the four conjuncts: r_orbit_pos shows positivity by multiplying r0 > 0 with phi^k > 0; r_orbit_adjacent_ratio unfolds the successor and cancels to obtain exactly phi; r_orbit_strict_mono uses one_lt_phi and nlinarith for the strict inequality; r_orbit_gap_skip_band bounds the phi-squared ratio inside (2.5, 2.7).
proof idea
The proof is a term-mode construction that directly supplies the four conjuncts by naming the lemmas r_orbit_pos, r_orbit_adjacent_ratio, r_orbit_strict_mono, and r_orbit_gap_skip_band.
why it matters
This packages the structural predictions of the J-cost model for planetary formation and links directly to the self-similar fixed point phi in T6 of the forcing chain. It supplies the recognition-cost derivation of the Titius-Bode law with no per-planet parameters. No downstream theorems are recorded, yet the statement serves as the single interface for empirical adjudication against JPL data on Solar System orbits.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.