PlanetaryFormationCert
The orbital ladder certificate bundles positivity, base case at k=0, exact adjacent ratio phi, strict increase, closed form r(k)=r0 phi^k, numerical ratio bands, and half-rung tolerance agreement for the multiplicative radius sequence. Astrophysicists working on J-cost minimization in protoplanetary disks cite it to certify that observed semi-major axes lie on the predicted ladder with only one free scale parameter. The structure is assembled by direct substitution of the module's supporting lemmas on the radius function.
claimA structure certifying that the orbital radius function $r(k)=r_0 phi^k$ for $r_0>0$ and $k∈ℕ$ satisfies $r(k)>0$, $r(0)=r_0$, $r(k+1)/r(k)=phi$, $r(k)<r(k+1)$, the adjacent ratio lies in $(1.61,1.62)$, the two-rung gap ratio lies in $(2.5,2.7)$, and each $r(k)$ lies inside the half-rung interval $[r(k)/√phi,r(k)√phi]$.
background
In the Recognition Science treatment of astrophysics a protoplanetary disk minimizes J-cost on radial bond density precisely when orbital radii form a phi-multiplicative ladder. The orbital radius at rung k for reference scale r0 is defined by r(k)=r0 phi^k. The half-rung agreement predicate holds for a measured radius r_meas when there exists k such that r_meas lies between r(k)/√phi and r(k)√phi, with √phi≈1.272 supplying the tolerance width that is exactly half the adjacent ratio in log space.
proof idea
This is a structure definition with no proof body. Each field is witnessed by the corresponding theorem already proved in the same module: positivity and base case from the orbit positivity and zero theorems, adjacent ratio from the ratio theorem, closed form from the closed-form theorem, and half-rung agreement from the ladder agreement theorem.
why it matters in Recognition Science
The structure supplies the master certificate for planetary formation under J-cost minimization and is instantiated directly by the planetary formation certificate definition. It realizes the structural prediction of the phi-ladder for orbital radii forced by the self-similar fixed point phi (T6) together with the recognition composition law. The module explicitly connects the construction to the Titius-Bode pattern and to empirical checks against JPL data, including the asteroid-belt placement and the Jupiter gap-skip.
scope and limits
- Does not fix the absolute scale r0 from first principles.
- Does not prove dynamical stability of the resulting orbits.
- Does not incorporate multi-body perturbations or resonances.
- Does not derive initial disk surface-density profiles.
formal statement (Lean)
177structure PlanetaryFormationCert where
178 r_orbit_pos : ∀ r0 : ℝ, 0 < r0 → ∀ k : ℕ, 0 < r_orbit r0 k
179 r_orbit_zero : ∀ r0 : ℝ, r_orbit r0 0 = r0
180 r_orbit_adjacent_ratio :
181 ∀ r0 : ℝ, 0 < r0 → ∀ k : ℕ,
182 r_orbit r0 (k + 1) / r_orbit r0 k = phi
183 r_orbit_strict_mono :
184 ∀ r0 : ℝ, 0 < r0 → ∀ k : ℕ,
185 r_orbit r0 k < r_orbit r0 (k + 1)
186 r_orbit_closed_form :
187 ∀ r0 : ℝ, ∀ k : ℕ, r_orbit r0 k = r0 * phi ^ k
188 r_orbit_adjacent_band :
189 ∀ r0 : ℝ, 0 < r0 → ∀ k : ℕ,
190 1.61 < r_orbit r0 (k + 1) / r_orbit r0 k ∧
191 r_orbit r0 (k + 1) / r_orbit r0 k < 1.62
192 r_orbit_gap_skip_band :
193 ∀ r0 : ℝ, 0 < r0 → ∀ k : ℕ,
194 (2.5 : ℝ) < r_orbit r0 (k + 2) / r_orbit r0 k ∧
195 r_orbit r0 (k + 2) / r_orbit r0 k < 2.7
196 ladder_agrees_at_half_rung :
197 ∀ r0 : ℝ, 0 < r0 → ∀ k : ℕ,
198 AgreesAtHalfRung r0 (r_orbit r0 k)
199