IndisputableMonolith.Astrophysics.PlanetaryFormationFromJCost
This module constructs the stable orbital radius function on the phi-ladder for planetary formation models in Recognition Science. Astrophysicists working with discrete J-cost minima would cite the r_orbit construction and its ratio lemmas. The module proceeds by recursive definitions at zero and successor rungs together with monotonicity and band lemmas.
claimThe function $r(k,r_0)$ denotes the stable orbital radius at rung $k$ for reference scale $r_0$, satisfying $r(0,r_0)=r_0$ and adjacent ratios lying in the band around $phi^2$ with strict monotonicity in $k$.
background
The module sits in the astrophysics domain and imports the RS time quantum $tau_0=1$ tick from Constants. It defines the orbital radius function together with supporting results on positivity, base case, successor step, strict increase, and closed relations such as the two-rung gap equaling $phi^2$. The local setting uses the J-cost $J(x)=(x+x^{-1})/2-1$ and the self-similar phi fixed point from the upstream forcing chain to select discrete stable radii.
proof idea
This is a definition module, no proofs. It supplies the base case r_orbit_zero, the successor clause r_orbit_succ, and then derives positivity, strict monotonicity, adjacent-ratio band membership, and the exact two-rung gap identity from the phi-ladder arithmetic.
why it matters in Recognition Science
The module supplies the discrete orbital ladder that realizes J-cost minimization for planetary formation, feeding any downstream model that requires stable radii in RS-native units. It directly instantiates the phi fixed point (T6) and the eight-tick octave structure (T7) at the astrophysical scale.
scope and limits
- Does not derive numerical radii for observed planets.
- Does not incorporate multi-body gravitational perturbations.
- Does not address accretion or formation timescales.
- Does not extend beyond the single-reference-scale ladder.
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