PlanetaryFormationCert
plain-language theorem explainer
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.
Claim. A 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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.