Astrophysics Planetary Formation From Jcost Planetary Formation One Statement

The φ-ladder of orbits

The planetary_formation_one_statement is a theorem in the Recognition Science framework's machine-checked library of formal theorems. It states that stable orbital radii in a protoplanetary disk sit on a multiplicative ladder where each step multiplies the radius by the golden ratio φ ≈ 1.618. The sequence is r_orbit(k) = r₀ · φᵏ, where r₀ is a single overall scale and k is an integer rung number.

The theorem proves several structural facts about this ladder. Every rung is positive, the ratio of adjacent rungs is exactly φ, and rungs increase strictly with k. It also proves a numerical band: the adjacent ratio lies between 1.61 and 1.62, which is the canonical Titius-Bode-compatible band. A two-rung gap, such as skipping the asteroid belt between Mars and Jupiter, gives a cumulative ratio of φ², which falls between 2.5 and 2.7.

The framework's rationale is that 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 is the recognition-cost reading of the Titius-Bode law, an empirical pattern that physics has had no first-principles derivation for. The framework derives it from its cost function, with no free parameters per planet, only the single overall scale r₀.

For the Solar System, the theorem is paired with a falsifier. A planet's semi-major axis must lie within a half-rung tolerance band, meaning within a factor of √φ ≈ 1.272 of a predicted rung. With r₀ = 0.4 AU for Mercury, the predicted rungs land at 0.40, 0.65, 1.05, 1.69, 2.74, 4.43 AU, and so on. The actual values for Venus, Earth, and Mars fall within the bands; the asteroid belt sits at the empty k=4 rung; Jupiter at k=5 is a gap-skip. The theorem itself proves the ladder's internal structure; the comparison against measured orbits is an empirical check run by a companion Python script against JPL Horizons data.

The theorem does not claim that planets must form at these radii from physical mechanisms like gravitational collapse or disk viscosity. It is a structural statement about what the framework's cost minimization forces, given the self-similarity that produces φ. The empirical agreement with the Solar System is a check, not a proof that the framework's physics is correct. The declaration proves the ladder's properties; it does not prove that real disks minimize J-cost in the way the framework assumes.

/-- **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⟩

/-- 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

/-- 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

/-- Half-rung tolerance: a measured semi-major axis `r_meas`
agrees with the φ-ladder at scale `r0` iff there exists `k` with
`r_meas ∈ [r_orbit r0 k / √φ, r_orbit r0 k · √φ]`. The
half-rung width `√φ ≈ 1.272` is exactly half the adjacent ratio
in log-space. -/
def AgreesAtHalfRung (r0 r_meas : ℝ) : Prop :=
  ∃ k : ℕ, r_orbit r0 k / Real.sqrt phi ≤ r_meas ∧
           r_meas ≤ r_orbit r0 k * Real.sqrt phi

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 real protoplanetary disks minimize J-cost; that physical bridge remains an assumption. The empirical agreement with Solar System orbits is a check, not a proof that the framework's physics is correct. The declaration does not derive the overall scale r₀; it takes it as a single free parameter.

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: