Astrophysics Galactic Rotation Curve From Rs Rotation Regime Count

The five regimes

A galaxy's rotation curve plots how fast stars and gas orbit the center against their distance from it. Astronomers have long described the curve in pieces: a rigid-body rise near the center, a rising segment, a long flat stretch where orbital speed barely changes, a declining part, and a final truncation where the disk ends. The Recognition Science framework encodes this familiar description as a formal object called RotationRegime, an inductive type whose five constructors are exactly those five phases: rigidBodyInner, rising, flat, declining, and truncation.

The theorem rotationRegime_count proves, by direct computation, that the number of distinct regimes is five. This is a statement about the framework's own definition, not about any particular galaxy. The proof is a machine-checked computation in the framework's library of formal theorems, with zero axioms and zero unfinished proofs. It establishes that the five-phase description is internally consistent and complete relative to the definition chosen.

The same source file defines transitionRadius, the radius at which the curve moves from one regime to the next. The theorem transitionRadius_ratio proves that each successive transition radius is exactly phi (the golden ratio, about 1.618) times the previous one. A companion theorem, transitionRadius_pos, proves every such radius is positive. Together these three results form a certificate, GalacticRotationCert, that packages the count, the ratio, and the positivity into one structure.

In Recognition Science, the golden ratio is not a free parameter; the framework derives it as the unique self-similar scaling from its cost function. The rotation-curve file applies that derived constant to the astrophysical picture: regime boundaries spaced by phi. This is a definitional and formal exercise within the framework. It models a stylized rotation curve, not a measured one. The file does not claim that any observed galaxy's rotation curve actually transitions at radii in exact phi ratios, nor does it derive the flat-regime phenomenon (often attributed to dark matter or modified gravity) from first principles.

What the theorem gives a reader is a precise, checkable statement: the framework's five-phase description of a rotation curve is exactly five-phase, and the boundaries follow a phi ladder. The astrophysical content is the identification of the five regimes, which matches the standard empirical description; the formal content is the count and the ratio, which are proved. The gap between the formal model and any real galaxy's data is not closed by this file, and that gap is openly a target for future work.

theorem rotationRegime_count : Fintype.card RotationRegime = 5 := by decide

theorem transitionRadius_ratio (k : ℕ) :
    transitionRadius (k + 1) / transitionRadius k = phi := by
  unfold transitionRadius
  have hpos : (0 : ℝ) < phi ^ k := pow_pos phi_pos k
  rw [div_eq_iff hpos.ne', pow_succ]
  ring

theorem transitionRadius_pos (k : ℕ) : 0 < transitionRadius k :=
  pow_pos phi_pos k

noncomputable def galacticRotationCert : GalacticRotationCert where
  five_regimes := rotationRegime_count
  phi_ratio := transitionRadius_ratio
  radius_always_pos := transitionRadius_pos

What this page does not claim

This theorem does not claim any observed galaxy's rotation curve transitions at radii in exact phi ratios. It does not derive the flat rotation curve from dark matter or modified gravity. It does not establish that the five regimes are the only possible description of a rotation curve outside the framework.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Astrophysics/GalacticRotationCurveFromRS.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: