Pith. sign in
module module moderate

IndisputableMonolith.Physics.AstrophysicsStarFormationFromRS

show as:
view Lean formalization →

The module defines stages of star formation and the Jeans mass using Recognition Science parameters. Astrophysicists modeling stellar collapse from first principles would reference these objects. The module consists of definitions and basic properties that build directly on the imported RS constants.

claimDefines the enumeration $\mathsf{StarFormationStage}$, the count $\mathsf{starFormationStageCount}$, the mass function $\mathsf{jeansMass}$, the ratio $\mathsf{jeansMassRatio}$, and the certificate $\mathsf{StarFormationCert}$ in RS-native units.

background

The module sits inside the Recognition Science application layer and imports the fundamental time quantum $\tau_0 = 1$ tick from Constants. It introduces star-formation stages together with the Jeans mass expressed on the phi-ladder. The local setting is the translation of the Recognition Composition Law and J-uniqueness into astrophysical criteria at stellar scales.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The module supplies the RS-native objects required by any downstream astrophysics extension of the unified forcing chain. It populates the physics domain with concrete definitions that can later attach to T7 (eight-tick octave) and T8 (D = 3) results.

scope and limits

depends on (1)

Lean names referenced from this declaration's body.

declarations in this module (6)