Pith. sign in
module module high

IndisputableMonolith.Astrophysics.NucleosynthesisTiers

show as:
view Lean formalization →

This module defines φ-tiers as integer indices on the φ-ladder and introduces NuclearTier and LuminosityTier for nucleosynthesis organization. Astrophysicists deriving stellar mass-to-light ratios cite it when eliminating external calibration in M/L calculations. The module supplies supporting definitions that rest on golden-ratio identities and stellar-assembly cost differentials.

claimA $\phi$-tier is an integer index $n$ on the $\phi$-ladder. NuclearTier and LuminosityTier are local tier assignments derived from the ladder step function.

background

The module operates in the astrophysics domain and imports the RS time quantum $\tau_0 = 1$ tick from Constants, recognition-cost primitives from Cost, and golden-ratio lemmas from PhiSupport.Lemmas. The latter establish $\phi^2 = \phi + 1$ and the fixed-point identity $\phi = 1 + 1/\phi$. StellarAssembly supplies the upstream recognition-cost differential between photon emission and mass storage during collapse. The sole module-level doc-comment states that a $\phi$-tier is an integer index on the $\phi$-ladder.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The module supplies the $\phi$-tier nucleosynthesis definitions required by the Astrophysics aggregator. It is imported by MassToLight (which unifies three independent M/L derivations) and ObservabilityLimits (which bounds M/L via recognition length and tick constraints). The downstream doc-comment lists "$φ$-tier nucleosynthesis" among the central derivations that remove external calibration inputs.

scope and limits

used by (3)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (4)

Lean names referenced from this declaration's body.

declarations in this module (20)