r_orbit_zero
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.
claimFor 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 in Recognition Science
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.
scope and limits
- Does not assume or prove positivity of the reference scale.
- Does not address physical stability or empirical fit to observed orbits.
- Does not extend to non-integer rungs or continuous indices.
- Does not derive the value of phi itself.
Lean usage
theorem base_case (r0 : ℝ) : r_orbit r0 0 = r0 := r_orbit_zero r0formal statement (Lean)
87theorem r_orbit_zero (r0 : ℝ) : r_orbit r0 0 = r0 := by
proof body
Term-mode proof.
88 unfold r_orbit
89 simp
90