pith. sign in
module module high

IndisputableMonolith.Astrophysics.MassToLight

show as:
view Lean formalization →

The MassToLight module states the characteristic mass-to-light ratio equals the golden ratio φ in solar units. Astrophysicists testing Recognition Science against stellar data would cite the result. The module collects three independent derivations from recognition-weighted collapse, φ-tier nucleosynthesis, and observability bounds, each converging on the same value.

claimThe derived mass-to-light ratio in solar units satisfies $M/L = \phi$, where $\phi$ is the golden ratio. This value lies on the $\phi$-ladder and emerges from J-cost weighting, nuclear tier structure, and recognition-length constraints.

background

Recognition Science places quantities on the discrete $\phi$-ladder generated by the self-similar fixed point $\phi = 1 + 1/\phi$. The module imports three strategy modules whose core insights are quoted below.

StellarAssembly derives M/L from the recognition cost differential between photon emission and mass storage during stellar collapse. NucleosynthesisTiers derives M/L from the discrete $\phi$-tier structure of nuclear densities and photon fluxes. ObservabilityLimits derives M/L from the observability constraints imposed by $\lambda_{rec}$ and $\tau_0 = 1$ tick. PhiSupport.Lemmas supplies the algebraic identities $\phi^2 = \phi + 1$ and the uniqueness of the positive root of $x^2 = x + 1$.

proof idea

This is a definition module, no proofs. It aggregates the three upstream strategy modules and records their agreement on the single value $\phi$.

why it matters in Recognition Science

The module supplies the mass-to-light ratio to the central Astrophysics aggregator and to ChandrasekharMassStructure for mass-scale anchors. It fills the M/L derivation in the LaTeX manuscript, Chapter "Astrophysical Tests", Section "M/L Derivation". The result connects directly to the $\phi$-ladder and the T5 J-uniqueness step of the 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)