Physics Astrophysics Star Formation From Rs Jeans Mass Ratio

The mass ratio

The Jeans mass, named after James Jeans's 1902 work on gravitational instability, is the minimum mass a molecular cloud needs before gravity overcomes internal gas pressure and collapse begins. The classical formula scales with temperature and density: M_J ∝ T^(3/2) × ρ^(-1/2). A cloud heavier than this threshold fragments and forms stars; a lighter one holds its shape. Astronomers use the Jeans mass to explain why star-forming regions break into clumps of roughly stellar size instead of collapsing all at once.

In Recognition Science, the framework models star formation as a ladder of discrete density levels, with each rung corresponding to a Jeans mass threshold. The machine-checked library of formal theorems defines jeansMass as phi^k, where phi is the golden ratio, approximately 1.618, and k is a nonnegative integer indexing the rung. The declaration jeansMassRatio proves that the ratio of any threshold to the previous one is exactly phi: jeansMass (k + 1) / jeansMass k = phi. In plain terms, each successive threshold is larger than the last by the same multiplicative factor, the golden ratio, not by a fixed additive amount or a random variable.

This ratio is a theorem, not a postulate: the library verifies it from the definition of jeansMass using the algebraic property that phi^ (k+1) / phi^k = phi, for any k. The proof is checked by the framework's kernel, with no unproved assumptions. The framework also certifies five canonical stages of star formation, from molecular cloud through prestellar core, protostar, and T Tauri phase to main sequence, and ties this count to a structural dimension of five. The mass ratio and the stage count together form a certificate object, a packaged claim that the framework's library checks as a whole.

What jeansMassRatio does not claim is just as important. It does not assert that real observed star-forming clouds have masses that follow this golden ladder; the declaration is a formal statement about the framework's own defined quantity, not an empirical measurement. It does not derive the classical Jeans formula from first principles, nor does it prove that the golden ratio governs actual star formation rates in the Milky Way. The framework's library shows a clean internal relationship: if you accept its definition of jeansMass, the ratio follows. Whether that definition matches astrophysical reality is a separate, empirical question the declaration leaves open.

The practical consequence is a testable prediction: within the framework, if star formation thresholds are quantized, they should appear at masses spaced by the golden ratio. An observer could search for such a pattern in the mass spectrum of prestellar cores. The framework's contribution is not a new law of gravity but a sharp, checkable structure imposed on a classical threshold, and a machine-checked guarantee that the structure is internally consistent.

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

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

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

What this page does not claim

The declaration does not assert that real observed star-forming clouds follow the golden ladder. It does not derive the classical Jeans formula from first principles. It does not prove that the golden ratio governs actual star formation rates in the Milky Way.

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: