pith. machine review for the scientific record. sign in
module module high

IndisputableMonolith.Astrophysics

show as:
view Lean formalization →

The Astrophysics module aggregates Recognition Science derivations of the stellar mass-to-light ratio M/L through three parallel strategies drawn from stellar collapse, nuclear tiers, and observability bounds. Astrophysicists seeking to remove external calibration inputs would cite it when building models from the phi-ladder and recognition cost. The module organizes its content solely as an importer of four submodules, each supplying one independent derivation path.

claimThe module aggregates derivations of the stellar mass-to-light ratio $M/L$ from recognition cost differentials in collapse, discrete $phi$-tier nuclear densities and photon fluxes, and observability constraints imposed by recognition length $lambda_{rec}$ and fundamental tick $tau_0$.

background

This module serves as the central import point for Recognition Science astrophysics. It collects four submodules that together eliminate external calibration for the mass-to-light ratio. The supplied module documentation states: Central import point for RS astrophysics derivations: Mass-to-light ratio (M/L) derivation with three parallel strategies, Stellar assembly via recognition-weighted collapse, phi-tier nucleosynthesis, Observability limits from lambda_rec, tau0 constraints.

proof idea

This is a module aggregator containing no theorems or proofs. It structures the argument by importing the four submodules MassToLight, StellarAssembly, NucleosynthesisTiers, and ObservabilityLimits, each of which supplies one independent derivation strategy for M/L.

why it matters in Recognition Science

This module feeds the main Astrophysics aggregator and supplies the three parallel M/L derivations required by the Recognition Science framework. It connects stellar assembly, phi-tier nucleosynthesis, and observability limits to the broader forcing chain and phi-ladder, enabling derivation of astrophysical observables directly from the single functional equation without external constants.

scope and limits

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (5)

Lean names referenced from this declaration's body.