pith. sign in
module module high

IndisputableMonolith.Astrophysics

show as:
view Lean formalization →

The Astrophysics module aggregates four submodules to derive the stellar mass-to-light ratio from Recognition Science principles without external calibration. Researchers applying RS to stellar systems and nucleosynthesis cite it as the central entry point. The module organizes three parallel strategies from recognition-weighted collapse, phi-tier nuclear structure, and observability bounds.

claimCentral aggregator for derivations of the stellar mass-to-light ratio $M/L$ in Recognition Science via recognition cost weighting, discrete $phi$-tier nucleosynthesis, and observability constraints from recognition length $lambda_{rec}$ and fundamental tick $tau_0$.

background

This module serves as the central import point for RS astrophysics derivations. It collects results on the mass-to-light ratio from three independent strategies without external inputs, as stated in its module documentation: mass-to-light ratio derivation with three parallel strategies, stellar assembly via recognition-weighted collapse, phi-tier nucleosynthesis, and observability limits from lambda_rec and tau_0 constraints.

proof idea

This is a module aggregator with no local proofs; it imports and re-exports the derivations from MassToLight, StellarAssembly, NucleosynthesisTiers, and ObservabilityLimits.

why it matters in Recognition Science

This module feeds the broader Recognition Science framework by supplying the M/L derivation that eliminates external calibration input. It extends the core functional equation to astrophysical scales through the three strategies documented in the submodules. The aggregator enables unified access for downstream applications in stellar and nuclear physics.

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.