pith. machine review for the scientific record. sign in
module module moderate

IndisputableMonolith.Nuclear.RProcessYieldsStructure

show as:
view Lean formalization →

This module structures the implication that r-process yields connect to neutron-star equation of state inputs in the Recognition Science nuclear domain. Researchers working on nucleosynthesis in neutron-star mergers would cite it to enforce consistency between yield ledgers and EOS parameters. The module consists of definitions and a single implication arrow with no internal proofs, depending only on the imported NeutronStarEOSStructure.

claimR-process yields structure implies neutron-star EOS-side input: $r$-process yields structure $implies$ neutron-star EOS structure.

background

The module sits in the Nuclear domain of Recognition Science and imports NeutronStarEOSStructure to supply the target side of the implication. It introduces r-process yields structure as a ledger-derived object (via the sibling r_process_yields_from_ledger) that supplies side inputs to the EOS. The local setting follows the overall Recognition Science forcing chain, where nuclear processes are constrained by the same J-cost and phi-ladder conventions used elsewhere in the monolith.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The module supplies the structural link required by downstream nuclear and merger models in the Recognition Science framework. It directly encodes the doc-comment claim that r-process yields structure implies neutron-star EOS-side input and sits upstream of any quantitative r-process yield calculations or EOS integrations. No used_by edges are recorded, indicating it functions as an early interface node.

scope and limits

depends on (1)

Lean names referenced from this declaration's body.

declarations in this module (4)