r_process_implies_ns_eos
plain-language theorem explainer
r_process_implies_ns_eos shows that the r-process yields ledger condition directly entails the neutron star equation of state ledger condition. Nuclear astrophysicists modeling heavy-element formation in mergers would cite the link when connecting yields to EOS inputs. The proof is a one-line term that returns the hypothesis, as the two propositions coincide by definition.
Claim. If the r-process yields are derived from the ledger, then the neutron star equation of state is derived from the ledger.
background
The declaration appears in the Nuclear module. neutron_star_eos_from_ledger is the proposition that nuclear force derives from the ledger. r_process_yields_from_ledger is defined to be identical to that proposition, creating a direct chain. The module imports NeutronStarEOSStructure, which supplies the base ledger definition for the EOS side.
proof idea
The proof is a one-line term that returns the hypothesis h. Because r_process_yields_from_ledger is definitionally equal to neutron_star_eos_from_ledger, the implication holds immediately without further reduction.
why it matters
The result closes the implication arrow from r-process yields to neutron star EOS inputs inside the nuclear sector of the Recognition framework. It maintains ledger consistency between yield structures and EOS constraints along the nuclear forcing chain. No downstream uses are recorded, indicating an interface role rather than a terminal lemma.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.