r_process_implies_ns_eos
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.
claimIf 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 in Recognition Science
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.
scope and limits
- Does not derive explicit numerical yields for any isotope.
- Does not produce the functional form of the neutron-star equation of state.
- Does not incorporate general-relativistic or magnetic-field corrections.
formal statement (Lean)
18theorem r_process_implies_ns_eos (h : r_process_yields_from_ledger) :
19 neutron_star_eos_from_ledger :=
proof body
Term-mode proof.
20 h
21
22end RProcessYieldsStructure
23end Nuclear
24end IndisputableMonolith