Pith. sign in
module module moderate

IndisputableMonolith.Astrophysics.SupernovaNucleoFromPhiLadder

show as:
view Lean formalization →

Links supernova nucleosynthesis yields to the Recognition Science phi-ladder via a domain cost and a canonical production threshold. Astrophysicists working on RS mass and abundance ladders would cite the certificate that packages nonnegativity and threshold positivity. The module is mostly definitions plus elementary positivity lemmas over the J-cost and Constants imports.

claimA domain cost $C$ on the phi-ladder, a canonical nucleosynthesis threshold $\theta>0$, and a supernova-yield certificate asserting $C\ge 0$ and $\theta>0$ in RS-native units (built from the J-cost and $\varphi$).

background

Recognition Science places particle and nuclear masses on a discrete $\varphi$-ladder, with the mass yardstick scaled by $\varphi^{r\mathrm{-}8+\mathrm{gap}(Z)}$. The cost side of that story is the unique J-functional $J(x)=(x+x^{-1})/2-1$ forced by the Recognition Composition Law; nonnegativity of J and related domain costs underpins thresholds for creation and yield.

This astrophysics module sits downstream of Constants (RS time quantum and $\varphi$) and Cost (J and derived costs). It introduces a domain cost for the nuclear/supernova setting, records that the cost at the canonical point matches the expected evaluation, proves nonnegativity, and defines a positive canonical threshold. Those pieces are bundled into a SupernovaYieldCert inhabited by a concrete certificate.

The local goal is not a full abundance table, but a lean interface: cost and threshold facts that later supernova or r-process arguments can import without re-deriving ladder arithmetic.

proof idea

Definition-heavy module. Domain cost and canonical threshold are defs; equality-at-point and nonnegativity/positivity are short lemmas reducing to Cost/Constants facts about J and $\varphi$. The certificate is a structure packing those inequalities; inhabitation is a constructor application once the positivity lemmas are in hand. No deep tactic proof; algebraic reduction and reuse of upstream cost nonnegativity.

why it matters in Recognition Science

Gives the astrophysics layer a first-class hook into the phi-ladder mass and cost story used elsewhere in the monolith. Supernova yields and nucleosynthesis thresholds become certificate-carrying objects rather than informal numerics, aligned with RS landmarks: $\varphi$ as self-similar fixed point (T6), J-uniqueness (T5), and the ladder mass formula. No downstream used_by edges are recorded yet; the module is an export surface for later abundance, r-process, or stellar-endpoint developments that need a nonnegative domain cost and a positive production threshold in RS units.

scope and limits

depends on (2)

Lean names referenced from this declaration's body.

declarations in this module (8)