pith. sign in
module module high

IndisputableMonolith.Astrophysics.MassToLight

show as:
view Lean formalization →

The MassToLight module derives the characteristic mass-to-light ratio as the golden ratio φ in solar units. Astrophysicists testing Recognition Science against stellar and galactic observations would cite it for the predicted value. The module aggregates three independent strategies from StellarAssembly, NucleosynthesisTiers, and ObservabilityLimits, each converging on the same φ outcome via J-cost, tier structure, and geometric bounds.

claimThe derived mass-to-light ratio satisfies $M/L = φ$ in solar units, where $φ = (1 + √5)/2$, obtained from J-cost weighting of photon emission versus mass storage, φ-tier nuclear and photon fluxes, and observability constraints from recognition length λ_rec and tick τ₀.

background

This module operates in the astrophysics domain of Recognition Science. It imports Constants for the fundamental time quantum τ₀ = 1 tick and PhiSupport.Lemmas for the golden-ratio identities φ² = φ + 1 and the positive root uniqueness of x² = x + 1. The three upstream modules supply the derivations: StellarAssembly weights photon emission against mass storage via recognition cost J during collapse; NucleosynthesisTiers places nuclear densities and photon fluxes on discrete φ-tiers; ObservabilityLimits enforces geometric constraints from λ_rec, τ₀, and coherence energy E_coh.

proof idea

This is a definition module, no proofs. It collects the three parallel derivation strategies from the imported modules and states the resulting M/L = φ value together with the agreement theorem H_ThreeStrategiesAgree.

why it matters in Recognition Science

The module supplies the M/L anchor to the parent Astrophysics aggregator and to ChandrasekharMassStructure for positive finite mass-scale anchors in the RS ladder. It implements the astrophysical test in the LaTeX Manuscript, Chapter Astrophysical Tests, Section M/L Derivation. It supports the zero-parameter status of RS by deriving the ratio without free parameters and touches the falsifier that observed M/L must lie on the φ-ladder within measurement uncertainty.

scope and limits

used by (2)

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.

declarations in this module (14)