IndisputableMonolith.Astrophysics.PlanetaryFormationFromJCost
The module defines the stable orbital radius at rung k for inner-reference scale r0, deriving discrete orbital positions from the J-cost and phi-ladder in Recognition Science. Astrophysicists modeling planetary spacing would cite these constructions to obtain rung-based radii without continuous integration. The module proceeds via base definition plus inductive lemmas on positivity, monotonicity, adjacent ratios, and two-rung gaps.
claimThe stable orbital radius at rung $k$ for inner-reference scale $r_0$ is the function satisfying $r(0,r_0)=r_0$, strict increase with $k$, and adjacent ratios confined to a band around the self-similar fixed point $\phi$.
background
The module imports the RS time quantum $\tau_0=1$ tick from Constants. It introduces the orbital radius function on the phi-ladder, with supporting lemmas for position, successor, strict monotonicity, adjacent ratio band, gap-skip band, and the identity that a two-rung gap equals $\phi^2$. The local setting is the direct translation of J-cost minimization into stable orbital locations, using the Recognition Composition Law to enforce self-similarity.
proof idea
This is a definition module with supporting lemmas. It begins with the base definition of the radius function, then applies inductive steps to establish positivity, successor preservation, strict monotonicity, ratio bounds, and the two-rung gap identity.
why it matters in Recognition Science
The module supplies the orbital-radius primitives that connect the forcing chain (T5 J-uniqueness, T6 phi fixed point, T7 eight-tick octave) to concrete astrophysical scales. It would feed parent theorems on planetary formation from J-cost, realizing the step from abstract Recognition Science to observable orbital structure, though no downstream declarations are yet listed.
scope and limits
- Does not compute numerical radii for specific planets.
- Does not incorporate general-relativistic or multi-body perturbations.
- Does not address formation dynamics beyond static J-cost minima.
- Does not extend the ladder beyond integer rungs.
depends on (1)
declarations in this module (15)
-
def
r_orbit -
theorem
r_orbit_pos -
theorem
r_orbit_zero -
theorem
r_orbit_succ -
theorem
r_orbit_adjacent_ratio -
theorem
r_orbit_strict_mono -
theorem
r_orbit_closed -
theorem
r_orbit_adjacent_ratio_band -
theorem
r_orbit_gap_skip_band -
theorem
two_rung_gap_eq_phi_squared -
def
AgreesAtHalfRung -
theorem
ladder_agrees_at_half_rung -
structure
PlanetaryFormationCert -
def
planetaryFormationCert -
theorem
planetary_formation_one_statement