GalacticRotationCert
plain-language theorem explainer
GalacticRotationCert bundles the five-regime classification of galactic rotation curves with phi-ladder spacing of their transition points. Astrophysicists deriving flat velocity profiles from Recognition Science without dark matter would cite this certificate to fix the regime count and radial ratios. The definition simply assembles the Fintype cardinality of the regime enumeration, the constant ratio phi between successive transition radii defined as powers of phi, and strict positivity of each radius.
Claim. A certificate for galactic rotation curves requires a set of five rotation regimes, transition radii satisfying $r_{k+1}/r_k = phi$ for every natural number $k$, and every transition radius strictly positive.
background
RotationRegime enumerates five canonical regimes: rigid-body inner, rising, flat, declining, and truncation. transitionRadius maps each natural number k to phi raised to k, locating each regime boundary one rung higher on the phi-ladder. The module derives rotation curves from Recognition Science by enforcing exactly these five regimes with phi-spaced transitions, consistent with the eight-tick octave and spatial dimension D=3 in the forcing chain.
proof idea
The structure definition collects three properties with no further obligations: the cardinality of the RotationRegime inductive type equals 5, the ratio of consecutive transition radii equals phi, and all transition radii remain positive.
why it matters
This certificate supplies the structural backbone for the galacticRotationCert instance that supports rotation-curve derivations. It implements the five-regime model (configDim D=5) from the Recognition Science astrophysics extension, linking directly to the phi-ladder, T5 J-uniqueness, and T6 phi fixed point. No open questions appear in the supplied material.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.