r_orbit
plain-language theorem explainer
The definition supplies the stable orbital radius at rung k for inner-reference scale r0 as r0 multiplied by phi to the power k. Astrophysicists modeling protoplanetary disks would cite it when deriving Titius-Bode patterns from J-cost minimization. It is introduced as a direct abbreviation of the multiplicative ladder forced by T6.
Claim. The orbital radius at rung $k$ for reference scale $r_0$ is $r(k) = r_0 phi^k$.
background
The module models planetary orbital radii as arising from J-cost minimization on radial bond density in a protoplanetary disk. Stable radii form a phi-multiplicative ladder, with the same self-similarity that forces phi as the fixed point in T6 of the UnifiedForcingChain. The parameter r0 is the overall disk scale; the upstream Anchor.r0 supplies sector-specific exponent offsets derived from wallpaper and cube geometry.
proof idea
This is a direct definition implementing the phi-ladder formula via real exponentiation. No lemmas are applied.
why it matters
This definition is the foundation for the PlanetaryFormationCert structure and the planetary_formation_one_statement theorem, which collect positivity, exact phi adjacent ratio, and strict monotonicity. It realizes the recognition-cost reading of the Titius-Bode pattern forced by T6 plus disk J-cost minimization, with no free parameters per planet beyond the single scale r0. It supports half-rung agreement checks against JPL data.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.