r_process_implies_ns_eos
plain-language theorem explainer
The declaration shows that r-process yields derived from the ledger directly entail the neutron-star equation-of-state input. Nuclear astrophysicists modeling heavy-element formation in mergers would cite this link when tracing nucleosynthesis back to ledger-derived forces. The proof is a one-line term that applies the hypothesis directly because the two propositions are definitionally equal.
Claim. If the r-process yields structure holds from the ledger, then the neutron-star equation of state follows from the ledger.
background
In the Nuclear.RProcessYieldsStructure module, neutron_star_eos_from_ledger is defined as nuclear_force_from_ledger, the proposition that the neutron-star equation of state is obtained from the fundamental ledger. r_process_yields_from_ledger is defined as neutron_star_eos_from_ledger, establishing that r-process yields inherit the same ledger origin. The module imports NeutronStarEOSStructure and sits inside the broader nuclear ledger chain that connects nucleosynthesis to the Recognition Science forcing structure.
proof idea
The proof is a one-line term that applies the hypothesis h directly, discharging the goal because r_process_yields_from_ledger is definitionally identical to neutron_star_eos_from_ledger.
why it matters
This theorem closes a definitional implication inside the nuclear ledger chain, ensuring that r-process yields and neutron-star EOS inputs remain consistent under the same ledger origin. It supports later steps that model element abundances in neutron-star mergers. No downstream uses are recorded yet, and the claim touches no open scaffolding.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.