module module

`IndisputableMonolith.Astrophysics.NucleosynthesisTiers`

show as: view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

used by (3)

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

IndisputableMonolith.Astrophysics module_import
IndisputableMonolith.Astrophysics.MassToLight module_import
IndisputableMonolith.Astrophysics.ObservabilityLimits module_import

depends on (4)

Lean names referenced from this declaration's body.

IndisputableMonolith.Astrophysics.StellarAssembly module_import
IndisputableMonolith.Constants module_import
IndisputableMonolith.Cost module_import
IndisputableMonolith.PhiSupport.Lemmas module_import

declarations in this module (20)

structure of L11
def J_bit L47
abbrev PhiTier L52
def phi_ladder L55
lemma phi_ladder_step L58
structure NuclearTier L72
def nuclear_tier_local L83
structure LuminosityTier L93
def luminosity_tier_local L100
def tier_difference L109
theorem tier_difference_value L111
def ml_nucleosynthesis L116
theorem ml_nucleosynthesis_eq_phi L118
def eight_tick_quantizes_tiers L132
theorem tiers_are_quantized L135
theorem ml_matches_stellar_observations L152
def population_tiers L172
theorem all_ml_on_phi_ladder L175
theorem ml_from_phi_tier_structure L187
theorem strategies_agree L202