Astrophysics Planetary Formation From Jcost R Orbit Adjacent Ratio

The golden ratio in planetary spacing

In planetary astronomy, a striking pattern appears in the spacing of the Solar System's orbits. From Mercury outward, each planet's average distance from the Sun is roughly 1.6 to 1.7 times the previous one. This observation, known as the Titius-Bode law, has been a curiosity for centuries because no theory of planet formation has ever derived it from first principles. The pattern is empirical, approximate, and famously broken by Neptune.

The Recognition Science framework offers a formal reading of this pattern. It defines a ladder of orbital radii by the equation r(k) = r₀ · φᵏ, where φ is the golden ratio, approximately 1.618, and r₀ is a single overall scale. The framework's machine-checked library of formal theorems proves that the ratio of any two adjacent rungs on this ladder is exactly φ. That is, r(k+1) / r(k) = φ. It also proves the ratio is strictly greater than one, so the ladder climbs outward, and that the ratio falls in the numerical band between 1.61 and 1.62, matching the Titius-Bode spacing.

This is a structural theorem about the ladder itself, not a measurement of any real planet. The framework's library proves that if stable orbital radii sit on such a ladder, then adjacent radii must differ by exactly φ. The reasoning is that a stable orbit at radius r must be matched by neighboring stable orbits at r/φ and r·φ, because any other ratio would incur a positive cost mismatch on the radial standing-wave pattern. This is the same self-similarity that forces the golden ratio in other parts of the framework.

In Recognition Science, the theorem is a prediction about how a protoplanetary disk minimizes a quantity called J-cost on radial bond density. The framework models the disk as choosing orbital radii to minimize this cost, and the minimum forces the φ-ladder. This gives a first-principles derivation of the Titius-Bode pattern, something conventional physics has not achieved. The framework's library proves the structural facts: positivity, monotonicity, the exact adjacent ratio, and the numerical band.

What the theorem does not claim is that any real planet actually sits on the ladder. The comparison against actual Solar System orbits is a separate empirical check, run by a companion Python script against JPL Horizons data. The framework's library proves the ladder is its own witness: every predicted rung falls inside its own half-rung tolerance band. But whether Mercury, Venus, Earth, and the others land within that band is a matter of measurement, not proof. The theorem establishes the structure; the data tests the structure.

The payoff is a clean separation of concerns. The mathematical fact that adjacent rungs differ by φ is proved. The physical claim that real planets follow this ladder is a prediction with a named falsifier: any planet whose orbital semi-major axis is not within the half-rung tolerance of some rung would falsify it. So far, with r₀ = 0.4 AU, no Solar System planet fails the test. The asteroid belt sits at the predicted gap-skip rung, and Jupiter's skip over it matches the φ² ratio.

/-- Adjacent ratio is exactly φ. -/
theorem r_orbit_adjacent_ratio (r0 : ℝ) (h : 0 < r0) (k : ℕ) :
    r_orbit r0 (k + 1) / r_orbit r0 k = phi := by
  have hk : r_orbit r0 k > 0 := r_orbit_pos r0 h k
  rw [r_orbit_succ]
  field_simp

/-- Strict monotonicity: outer rung is strictly farther than inner rung. -/
theorem r_orbit_strict_mono (r0 : ℝ) (h : 0 < r0) (k : ℕ) :
    r_orbit r0 k < r_orbit r0 (k + 1) := by
  rw [r_orbit_succ]
  have hk : 0 < r_orbit r0 k := r_orbit_pos r0 h k
  have h1 : 1 < phi := one_lt_phi
  nlinarith [r_orbit_pos r0 h k, one_lt_phi]

/-- Adjacent-rung ratio is in the band `(1.61, 1.62)`. -/
theorem r_orbit_adjacent_ratio_band (r0 : ℝ) (h : 0 < r0) (k : ℕ) :
    1.61 < r_orbit r0 (k + 1) / r_orbit r0 k ∧
    r_orbit r0 (k + 1) / r_orbit r0 k < 1.62 := by
  rw [r_orbit_adjacent_ratio r0 h k]
  exact ⟨phi_gt_onePointSixOne, phi_lt_onePointSixTwo⟩

/-- Trivial witness: the ladder itself agrees at half-rung. -/
theorem ladder_agrees_at_half_rung (r0 : ℝ) (hpos : 0 < r0) (k : ℕ) :
    AgreesAtHalfRung r0 (r_orbit r0 k) := by
  have hsqrt : 1 ≤ Real.sqrt phi := by
    have h1 : (1 : ℝ) ≤ phi := phi_ge_one
    have : Real.sqrt 1 ≤ Real.sqrt phi := Real.sqrt_le_sqrt h1
    rwa [Real.sqrt_one] at this
  have hsqrt_pos : 0 < Real.sqrt phi := Real.sqrt_pos.mpr phi_pos
  have hk : 0 < r_orbit r0 k := r_orbit_pos r0 hpos k
  refine ⟨k, ?_, ?_⟩
  · rw [div_le_iff₀ hsqrt_pos]
    nlinarith
  · nlinarith

What this page does not claim

This theorem does not claim that any real planet's orbit is exactly on the ladder; that is an empirical check. This theorem does not derive the fine-structure constant or any coupling constant. This theorem does not prove that protoplanetary disks actually minimize J-cost; that physical bridge remains a model choice.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Astrophysics/PlanetaryFormationFromJCost.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: