transitionRadius
plain-language theorem explainer
The transition radius between galactic rotation regimes is defined as the k-th power of the golden ratio phi. Astrophysicists working in Recognition Science cite this to locate the boundaries of the five regimes on the phi-ladder. The declaration is a direct one-line definition with no proof steps required.
Claim. For each natural number $k$, the transition radius at rung $k$ is $r_k = phi^k$, where $phi$ is the golden ratio satisfying $phi^2 = phi + 1$.
background
The module derives galactic rotation curves from Recognition Science by identifying five regimes (rigid-body inner, rising, flat, declining, truncation) that match configDim D = 5. Each regime transition occurs at a successive rung of the phi-ladder, the discrete sequence generated by powers of the golden ratio. This definition supplies the explicit radii for those transitions.
proof idea
This is a one-line definition that directly sets the transition radius at rung k to phi raised to the power k.
why it matters
The definition supplies the radii required by the GalacticRotationCert structure, which certifies exactly five regimes, the constant ratio phi between consecutive radii, and strict positivity of all radii. It implements the phi-ladder placement of regime boundaries in the RS astrophysics model, consistent with the self-similar fixed point (T6) and the mass formula that uses the same ladder. No open questions attach to this definition.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.