pith. sign in
module module high

IndisputableMonolith.Cosmochemistry.StellarAbundanceFromPhiLadder

show as:
view Lean formalization →

This module derives the even-odd abundance ratio near the iron peak as equal to φ using the Recognition Science phi ladder. Cosmochemists and stellar modelers would cite it for phi-based abundance predictions. The module builds its results through definitions and lemmas imported from the Constants and Cost modules.

claimThe even-odd abundance ratio near the iron peak satisfies $r = A_{even}/A_{odd} = φ$, where $φ$ is the self-similar fixed point of the J-function.

background

Recognition Science derives stellar abundances from the phi-ladder mass formula, with masses scaled by powers of φ from a yardstick. The module imports the RS time quantum τ₀ = 1 tick from Constants and cost functions from Cost to quantify ratios. It focuses on even-odd nucleon ratios near iron, which the framework sets to φ via J-uniqueness.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

This module supplies the cosmochemistry component of the Recognition framework, linking abundances to the phi fixed point (T6) and the phi-ladder mass formula. It has no listed downstream theorems yet but supports larger stellar nucleosynthesis calculations.

scope and limits

depends on (2)

Lean names referenced from this declaration's body.

declarations in this module (8)