pith. sign in
module module high

IndisputableMonolith.Astrophysics.NucleosynthesisTiers

show as:
view Lean formalization →

This module defines φ-tiers as integer indices on the φ-ladder together with NuclearTier and LuminosityTier for nucleosynthesis calculations. Astrophysicists using Recognition Science cite it when linking stellar assembly to tier differences in mass-to-light derivations. The module consists of type definitions, local functions, and value computations with no complex proofs.

claimA φ-tier is an integer index $k$ on the φ-ladder. NuclearTier and LuminosityTier are local functions of rung and gap; tier_difference_value computes the difference between them; ml_nucleosynthesis assembles the resulting mass-to-light contribution.

background

The module sits inside the Astrophysics domain and imports StellarAssembly (recognition-weighted collapse), Constants (τ₀ = 1 tick), Cost, and PhiSupport.Lemmas (φ² = φ + 1 and fixed-point identity). It introduces PhiTier as the integer index on the φ-ladder, phi_ladder and phi_ladder_step as the underlying sequence, and the three tier constructors (NuclearTier, LuminosityTier, tier_difference). These rest on the self-similar fixed point from the forcing chain T6.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The module supplies the nucleosynthesis tier component that feeds the Astrophysics aggregator, the MassToLight unified certificate, and ObservabilityLimits. It completes the φ-tier nucleosynthesis leg of the three parallel M/L strategies and connects directly to the recognition cost differential in StellarAssembly.

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)