Physics Astrophysics Star Formation From Rs Star Formation Stage

The star formation ladder

Star formation is the process by which a cold, dense molecular cloud collapses under its own gravity to form a star. Astronomers divide this collapse into five canonical stages: molecular cloud, prestellar core, protostar, T Tauri, and main sequence. The first is the raw material, a cloud of gas and dust; the last is the stable hydrogen-burning star. In between, the core condenses, heats, and ignites.

The threshold for collapse is the Jeans mass, the minimum mass at which gravity overcomes thermal pressure. It scales as M_J ∝ T^(3/2) × ρ^(-1/2), where T is temperature and ρ is density. The classical picture is that a cloud fragment exceeding this mass collapses; below it, pressure holds it up.

In Recognition Science, the framework models star formation as a discrete ladder. Its machine-checked library of formal theorems declares an inductive type StarFormationStage, a discrete record of exactly those five stages, and proves that its cardinality is 5. The framework then models the Jeans mass at each rung as a power of the golden ratio φ: jeansMass(k) = φ^k. A theorem proves the ratio of successive masses is exactly φ: jeansMass(k+1) / jeansMass(k) = φ. This is a formal statement about a chosen model, not a measurement of real clouds.

The framework's contribution is structural: it shows that if you accept its five-stage ladder and its φ-scaling for the Jeans mass, then the ratio between stages is forced to be the golden ratio. The certificate bundles these two facts into a single object. What the declaration does not do is assert that real stars obey this ladder. The physical bridge from the formal model to observed star formation is not claimed by the declaration; it remains a target for future work.

inductive StarFormationStage where
  | molecularCloud | prestellarCore | protostar | tTauri | mainSequence
  deriving DecidableEq, Repr, BEq, Fintype

theorem starFormationStageCount : Fintype.card StarFormationStage = 5 := by decide

noncomputable def jeansMass (k : ℕ) : ℝ := phi ^ k

theorem jeansMassRatio (k : ℕ) :
    jeansMass (k + 1) / jeansMass k = phi := by
  unfold jeansMass
  have hpos := pow_pos phi_pos k
  rw [pow_succ, div_eq_iff hpos.ne']
  ring

What this page does not claim

The declaration does not assert that real stars form in exactly five discrete stages. The phi-scaling of Jeans mass is a model choice, not a measured property of molecular clouds. The framework does not derive the Jeans mass formula from first principles; it takes it as input.

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/Physics/AstrophysicsStarFormationFromRS.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: