Astrophysics Planetary Formation From Jcost R Orbit Strict Mono

The ladder's ordering

The recognition framework, which models physical structure from a forced cost of maintaining a discrete record of events, has a machine-checked library of formal theorems. One of its declarations, r_orbit_strict_mono, proves a fact about a specific mathematical model of planetary orbits. If a protoplanetary disk minimizes the framework's cost function on its radial structure, then the stable orbital radii are defined by the formula r_orbit(k) = r₀ · φᵏ, where r₀ is a single overall scale, k is a non-negative integer labeling each orbit, and φ is the golden ratio, approximately 1.618.

Given this definition, the theorem r_orbit_strict_mono states that for any positive scale r₀ and any rung k, the orbital radius at rung k is strictly less than the radius at rung k+1. In plain language, the ladder of allowed orbits is strictly ordered: each successive rung is farther out than the last. This is a pure structural fact about the defined sequence. The proof relies on two simpler results: that each radius is positive, and that the golden ratio is greater than 1. The theorem is not a physical observation; it is a logical consequence of the definition of the ladder itself.

The declaration also establishes the adjacent ratio exactly: r_orbit(k+1) / r_orbit(k) = φ. This means the spacing between consecutive rungs is not arbitrary but is fixed by the golden ratio. A related theorem, r_orbit_gap_skip_band, shows that skipping one rung gives a ratio φ², which falls in the numerical band between 2.5 and 2.7. These are the structural facts the framework proves about its own model.

What the declaration does not claim is that any real planet follows this ladder. The framework's docstring labels the ladder a structural prediction, and its empirical check against Solar System data is a separate Python pipeline, not part of the formal proof. The theorem r_orbit_strict_mono is conditional: if orbital radii are given by the φ-ladder, then they increase strictly. It says nothing about whether Mercury, Venus, or any other observed body actually sits on such a rung. That comparison is an empirical question, not a proved result.

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

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

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

What this page does not claim

This theorem does not claim that any real planet's orbit is described by the φ-ladder. This theorem does not claim that planetary formation in the Solar System is fully explained by the recognition framework. This theorem does not claim that the cost function J(x) is the only possible cost function for planetary systems.

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: