Pith. sign in
module module high

IndisputableMonolith.Astrophysics.MassToLight

show as:
view Lean formalization →

The MassToLight module defines the characteristic mass-to-light ratio as the golden ratio φ in solar units. Astrophysicists testing Recognition Science stellar predictions would cite it for comparison with observed M/L values. The module aggregates three independent derivations from recognition-weighted collapse, φ-tier nucleosynthesis, and observability constraints without internal proofs.

claimThe characteristic mass-to-light ratio satisfies $M/L = \phi \approx 1.618$ in solar units, where $\phi$ is the golden ratio. This value follows from J-cost weighting of photon emission versus mass storage, the discrete $\phi$-tier structure of nuclear and photon fluxes, and geometric bounds imposed by recognition length $\lambda_{\rm rec}$ and fundamental tick $\tau_0$.

background

Recognition Science places physical quantities on discrete $\phi$-tiers. StellarAssembly supplies the recognition cost differential between photon emission and mass storage during collapse. NucleosynthesisTiers supplies the $\phi$-tier structure of nuclear densities and photon fluxes. ObservabilityLimits supplies constraints from recognition length $\lambda_{\rm rec}$ and fundamental tick $\tau_0 = 1$ tick (from Constants). PhiSupport.Lemmas supplies the identities $\phi^2 = \phi + 1$ and the fixed-point relation $\phi = 1 + 1/\phi$.

proof idea

This is a definition module, no proofs. It collects the three upstream strategy modules to assert a single derived value $M/L = \phi$ and records the falsifier condition on the $\phi$-ladder.

why it matters in Recognition Science

The module supplies the mass-to-light ratio to the central Astrophysics aggregator and to ChandrasekharMassStructure for positive finite mass-scale anchors in the RS ladder range. It fills the M/L derivation step in the paper's Chapter "Astrophysical Tests", Section "M/L Derivation", anchoring stellar observations to the $\phi$-ladder within the T0-T8 forcing chain.

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)