r_orbit_pos
plain-language theorem explainer
The theorem shows that the orbital radius function r_orbit(r0, k) remains strictly positive for every positive reference scale r0 and every natural number k. Astrophysicists deriving protoplanetary disk radii from J-cost minimization would cite it to keep all ladder predictions inside the physical domain. The proof is a one-line term that unfolds the multiplicative definition and applies mul_pos together with pow_pos on phi_pos.
Claim. Let $r_0 > 0$ be real and $k$ a natural number. Define the orbital radius at rung $k$ by $r(k) := r_0 phi^k$. Then $r(k) > 0$.
background
The module treats planetary orbital radii as the radii that minimize J-cost on radial bond density inside a protoplanetary disk. The function r_orbit is defined by the explicit product r0 multiplied by phi raised to the power k, where phi is the self-similar fixed point forced by T6. This construction reproduces the Titius-Bode pattern as a direct consequence of Recognition Composition Law minimisation with a single overall scale r0. The upstream definition r_orbit supplies the closed multiplicative form; the separate anchor r0 in Masses.Anchor records sector-specific integer offsets arising from wallpaper geometry and is not used here.
proof idea
The term proof unfolds the definition of r_orbit, converting the goal into the inequality r0 * phi^k > 0. It then invokes mul_pos on the two hypotheses 0 < r0 and 0 < phi^k, where the second inequality is obtained by applying pow_pos to the known fact phi_pos.
why it matters
The result is packaged inside the structure PlanetaryFormationCert and is invoked by planetary_formation_one_statement, which asserts the complete ladder properties (positivity, adjacent ratio exactly phi, strict increase, and gap-skip ratio phi squared). It supplies the basic well-definedness step that lets the Recognition Science chain from T6 self-similarity reach concrete astrophysical predictions; the empirical comparison against JPL data is performed by the companion Python script referenced in the module documentation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.