r_orbit_zero
plain-language theorem explainer
The declaration establishes that the orbital radius function at rung zero recovers the reference scale exactly. Researchers modeling planetary systems via J-cost minimization on phi-ladders cite this base case when verifying ladder properties for Titius-Bode derivations. The proof is a one-line wrapper that unfolds the definition and simplifies the zero exponent.
Claim. For any real number $r_0$, the orbital radius at rung zero satisfies $r(r_0,0)=r_0$, where $r(r_0,k)=r_0·ϕ^k$ is the stable orbital radius at natural-number rung $k$.
background
The module models protoplanetary disks that minimize J-cost on radial bond density by placing orbital radii on a phi-multiplicative ladder. The upstream definition supplies the explicit formula for the stable orbital radius at rung $k$ as $r_0·ϕ^k$. This construction rests on the self-similarity forced in T6 of the unified forcing chain, where phi arises as the fixed point of the J-cost functional. The module states that any other ratio incurs a strictly positive J-cost mismatch on the radial standing-wave pattern.
proof idea
The proof is a one-line wrapper that unfolds the definition of the orbital radius function and applies simp to reduce the exponent zero to one.
why it matters
This supplies the base case for the PlanetaryFormationCert structure, which bundles positivity, adjacent ratios equal to phi, and monotonicity of the ladder. It anchors the zero-rung case in the Recognition Science framework, directly implementing the T6 self-similar fixed point for planetary formation with no free parameters beyond the overall scale. The structure is used to certify the full set of ladder properties for empirical comparison against JPL data.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.