pith. sign in
module module high

IndisputableMonolith.Astrophysics

show as:
view Lean formalization →

Astrophysics module aggregates three independent derivations of the stellar mass-to-light ratio from Recognition Science principles. Researchers applying RS to stellar systems cite it as the unified entry point that removes external calibration for M/L. The module organizes this content by importing submodules on stellar assembly, phi-tier nucleosynthesis, and observability limits, each supplying one derivation path.

claimThe module collects derivations of the stellar mass-to-light ratio $M/L$ via recognition cost weighting during collapse, discrete $\phi$-tier nuclear densities and photon fluxes, and observability constraints from recognition length $\lambda_{rec}$ and fundamental tick $\tau_0$.

background

Recognition Science applies the J-cost functional and phi-ladder to astrophysics, deriving quantities from the Recognition Composition Law without external parameters. The Astrophysics module acts as the central aggregator for these results in the stellar domain.

The imported MassToLight submodule unifies three strategies. StellarAssembly derives $M/L$ from the recognition cost differential between photon emission and mass storage. NucleosynthesisTiers uses the discrete $\phi$-tier structure of nuclear densities. ObservabilityLimits imposes bounds from $\lambda_{rec}$ and $\tau_0$ for a system to remain observable.

proof idea

This is a module aggregator with no internal proofs. It structures the argument by importing the four submodules that each supply one independent derivation path for the mass-to-light ratio.

why it matters in Recognition Science

This module supplies the astrophysics component that feeds the broader Recognition Science claim of deriving all physics from the single functional equation. It connects to the T5 J-uniqueness and T6 phi fixed point through mass formulas on the phi-ladder. The parent usage appears as the central import point for M/L results in stellar contexts.

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.