transitionRadius_ratio
plain-language theorem explainer
The theorem shows that consecutive transition radii in the galactic rotation curve model stand in the exact ratio phi. Astrophysicists working within Recognition Science cite it to confirm geometric spacing of the five regime boundaries along the phi-ladder. The proof is a direct algebraic reduction obtained by unfolding the power definition and applying field cancellation.
Claim. For every natural number $k$, the ratio of the transition radius at rung $k+1$ to the transition radius at rung $k$ equals $phi$, where the transition radius at rung $k$ is defined to be $phi^k$.
background
The module identifies five canonical rotation-curve regimes (rigid-body, rising, flat, declining, truncation) whose boundaries lie on successive rungs of the phi-ladder. The upstream definition states transitionRadius (k : ℕ) : ℝ := phi ^ k. This construction inherits the self-similar scaling fixed point phi from the forcing chain (T6) and the Recognition Composition Law.
proof idea
The term proof unfolds transitionRadius to obtain phi^(k+1) / phi^k. It adds the positivity fact pow_pos phi_pos k, rewrites via div_eq_iff, replaces the numerator with pow_succ, and finishes with the ring tactic.
why it matters
The result populates the phi_ratio field inside galacticRotationCert, which certifies the full five-regime structure. It supplies the concrete scaling step required by the phi-ladder description in the module doc-comment and aligns with the self-similar fixed point of the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.