r_process_yields_from_ledger
plain-language theorem explainer
This definition sets the r-process yields from ledger proposition equal to the neutron-star equation of state from ledger proposition. Nuclear astrophysicists modeling r-process nucleosynthesis in mergers would cite it to link yields directly to EOS constraints. It is implemented as a direct one-line alias with no additional content.
Claim. Define the proposition that r-process yields follow from the ledger to be identical to the proposition that the neutron-star equation of state follows from the ledger.
background
This declaration lives in the RProcessYieldsStructure module, which imports NeutronStarEOSStructure. The upstream result neutron_star_eos_from_ledger is itself defined as an alias for nuclear_force_from_ledger. The module contains sibling declarations has_ns_eos_structure, r_process_yields_structure, and r_process_implies_ns_eos that operate on this shared proposition. In the Recognition Science setting it supplies the interface between r-process yields and the ledger-derived nuclear force assumptions.
proof idea
The definition is a one-line alias that directly equates the r-process yields from ledger proposition to the neutron-star equation of state from ledger proposition.
why it matters
It supplies the common proposition referenced by the downstream theorems r_process_yields_structure (which asserts the property via has_ns_eos_structure) and r_process_implies_ns_eos (which shows the yields property implies the EOS property). The construction bridges r-process nucleosynthesis calculations to neutron-star EOS inputs within the nuclear applications of the ledger framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.