Astrophysics Planetary Formation From Jcost R Orbit Gap Skip Band

The gap-skip band

The Titius-Bode law is a centuries-old observation that planetary orbits often fall into a rough geometric progression. The Recognition Science framework offers a first-principles derivation of this pattern. Its starting point is the ledger, a discrete record of recognition events, and the cost of recording them. The framework proves that any cost function meeting five plain conditions must equal J(x) = (x + 1/x)/2 - 1. From this, it derives that the golden ratio φ, about 1.618, is the unique self-similar scaling. A stable orbit at radius r must be matched by neighboring stable orbits at r/φ and r·φ, because any other ratio incurs a strictly positive cost mismatch on the radial standing-wave pattern.

This yields a ladder of orbital radii: r_orbit(k) = r₀ · φᵏ, where r₀ is a single overall scale and k is a nonnegative integer. The framework's machine-checked library of formal theorems proves the basic structural facts: each rung is positive, each adjacent ratio is exactly φ, and the sequence strictly increases. The declaration r_orbit_gap_skip_band is one of these theorems. It states that skipping one rung, going from k to k+2, gives a cumulative ratio φ², which lies in the numerical band (2.5, 2.7). This is the formal content: a two-rung gap produces a ratio in that specific interval.

The band has a direct reading in the Solar System. Taking the inner reference r₀ = 0.4 AU at Mercury, the ladder places the next rungs at Venus (k=1, predicted 0.65 AU), Earth (k=2, predicted 1.05 AU), and Mars (k=3, predicted 1.69 AU). The k=4 rung lands at 2.74 AU, which is the inner edge of the asteroid belt, where no planet formed. The next rung, k=5, is Jupiter at a predicted 4.43 AU. The gap between Mars and Jupiter is therefore a two-rung skip, and the theorem certifies that this skip ratio sits in the canonical band. The framework calls this the gap-skip identity.

What the theorem does not claim is as important as what it proves. The theorem is purely structural: it certifies a ratio band for a defined ladder. It does not prove that any real planet must sit on this ladder. The comparison against actual JPL Horizons data for the Solar System is an empirical check, run by a companion Python script, not a theorem. The framework's own falsifier is precise: any Solar-System planet whose semi-major axis is not within the ratio φ^(1/2) of a rung would refute the prediction. With r₀ = 0.4 AU, the framework states that no planet fails this test, but that statement is a measurement check, not a formal derivation.

In plain terms, the declaration establishes a clean mathematical fact about a golden-ratio ladder: skip one rung, and the ratio is between 2.5 and 2.7. It is a theorem about the ladder's own structure. Whether the Solar System obeys that ladder is a separate, empirical question, one the framework addresses with a named falsifier and a data pipeline, but does not close with a proof.

/-- Gap-skip ratio (skipping one stable rung) is `φ² ∈ (2.5, 2.7)`. -/
theorem r_orbit_gap_skip_band (r0 : ℝ) (h : 0 < r0) (k : ℕ) :
    (2.5 : ℝ) < r_orbit r0 (k + 2) / r_orbit r0 k ∧
    r_orbit r0 (k + 2) / r_orbit r0 k < 2.7 := by
  have hk : 0 < r_orbit r0 k := r_orbit_pos r0 h k
  have hr0 : r0 ≠ 0 := ne_of_gt h
  have hphi_k : phi ^ k ≠ 0 := pow_ne_zero _ phi_ne_zero
  have hratio :
      r_orbit r0 (k + 2) / r_orbit r0 k = phi ^ 2 := by
    unfold r_orbit
    rw [show (k + 2) = k + 2 from rfl, pow_add]
    field_simp
  rw [hratio]
  exact phi_squared_bounds

/-- **PLANETARY FORMATION ONE-STATEMENT.** Stable protoplanetary-disc
orbital radii sit on the φ-ladder `r_orbit(k) = r₀ · φᵏ`. Adjacent
rungs differ by exactly φ; gap-skip rungs (the asteroid-belt /
Jupiter pattern) differ by φ². The ladder is its own half-rung
witness: every prediction is inside its own falsifier band. -/
theorem planetary_formation_one_statement :
    (∀ r0 : ℝ, 0 < r0 → ∀ k : ℕ, 0 < r_orbit r0 k) ∧
    (∀ r0 : ℝ, 0 < r0 → ∀ k : ℕ,
      r_orbit r0 (k + 1) / r_orbit r0 k = phi) ∧
    (∀ r0 : ℝ, 0 < r0 → ∀ k : ℕ,
      r_orbit r0 k < r_orbit r0 (k + 1)) ∧
    (∀ r0 : ℝ, 0 < r0 → ∀ k : ℕ,
      (2.5 : ℝ) < r_orbit r0 (k + 2) / r_orbit r0 k ∧
      r_orbit r0 (k + 2) / r_orbit r0 k < 2.7) :=
  ⟨r_orbit_pos, r_orbit_adjacent_ratio, r_orbit_strict_mono,
   r_orbit_gap_skip_band⟩

/-- Stable orbital radius at rung `k` for inner-reference scale `r₀`. -/
def r_orbit (r0 : ℝ) (k : ℕ) : ℝ := r0 * phi ^ k

structure PlanetaryFormationCert where
  r_orbit_pos : ∀ r0 : ℝ, 0 < r0 → ∀ k : ℕ, 0 < r_orbit r0 k
  r_orbit_zero : ∀ r0 : ℝ, r_orbit r0 0 = r0
  r_orbit_adjacent_ratio :
    ∀ r0 : ℝ, 0 < r0 → ∀ k : ℕ,
      r_orbit r0 (k + 1) / r_orbit r0 k = phi
  r_orbit_strict_mono :
    ∀ r0 : ℝ, 0 < r0 → ∀ k : ℕ,
      r_orbit r0 k < r_orbit r0 (k + 1)
  r_orbit_closed_form :
    ∀ r0 : ℝ, ∀ k : ℕ, r_orbit r0 k = r0 * phi ^ k
  r_orbit_adjacent_band :
    ∀ r0 : ℝ, 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
  r_orbit_gap_skip_band :
    ∀ r0 : ℝ, 0 < r0 → ∀ k : ℕ,
      (2.5 : ℝ) < r_orbit r0 (k + 2) / r_orbit r0 k ∧
      r_orbit r0 (k + 2) / r_orbit r0 k < 2.7
  ladder_agrees_at_half_rung :
    ∀ r0 : ℝ, 0 < r0 → ∀ k : ℕ,
      AgreesAtHalfRung r0 (r_orbit r0 k)

What this page does not claim

The theorem does not prove that any real planet must sit on the φ-ladder. The theorem does not claim that the asteroid belt is empty because of the gap-skip identity. The theorem does not derive the overall scale r₀ from first principles.

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: