theorem proved term proof

`tier_difference_value`

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

formal statement (Lean)

 111theorem tier_difference_value : tier_difference = 1 := by

Term-mode proof.

 112  unfold tier_difference nuclear_tier_local luminosity_tier_local
 113  norm_num
 114
 115/-- The nucleosynthesis-derived M/L -/

Lean names referenced from this declaration's body.

luminosity_tier_local in IndisputableMonolith.Astrophysics.NucleosynthesisTiers decl_use
nuclear_tier_local in IndisputableMonolith.Astrophysics.NucleosynthesisTiers decl_use
tier_difference in IndisputableMonolith.Astrophysics.NucleosynthesisTiers decl_use
L in IndisputableMonolith.Recognition decl_use
M in IndisputableMonolith.Recognition decl_use
L in IndisputableMonolith.Recognition.Cycle3 decl_use
M in IndisputableMonolith.Recognition.Cycle3 decl_use