galacticRotationCert
plain-language theorem explainer
galacticRotationCert supplies a concrete certificate asserting five rotation regimes for galactic curves with phi-governed transitions and positive radii. Researchers modeling flat rotation curves or MOND-like behavior would cite it to ground the phi-ladder structure in RS. The definition is assembled directly from three supporting theorems that establish the regime count, the geometric ratio, and radius positivity.
Claim. The galactic rotation curve certificate asserts that there exist exactly five rotation regimes, that consecutive transition radii satisfy $r_{k+1}/r_k = phi$, and that every transition radius is positive.
background
GalacticRotationCert is a structure packaging three properties: the cardinality of rotation regimes equals 5, consecutive transition radii scale by the golden ratio phi, and all transition radii remain positive. The module describes five canonical regimes (rigid-body inner, rising, flat MOND/DM, declining, truncation) with each transition radius one rung up the phi-ladder. The count follows from rotationRegime_count, which decides the cardinality of RotationRegime is 5. The ratio property is proved in transitionRadius_ratio by unfolding transitionRadius as a power of phi and applying ring simplification. Positivity holds in transitionRadius_pos because phi is positive and powers preserve positivity.
proof idea
The definition constructs the certificate by direct record assignment of its three fields. It wires rotationRegime_count into the regime count, transitionRadius_ratio into the phi scaling, and transitionRadius_pos into the positivity requirement. No further tactics or reductions are applied.
why it matters
This definition completes the basic certification for galactic rotation curves in the RS framework, linking the five-regime structure directly to the phi-ladder. It supports the claim that rotation curves arise from the Recognition Composition Law and the self-similar fixed point phi. No downstream uses are recorded yet, leaving open its integration into explicit velocity derivations or observational tests.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.