neutron_star_eos_from_ledger
plain-language theorem explainer
This definition equates the neutron-star equation-of-state ledger condition to the positivity of the four effective nuclear-force coefficients. Nuclear astrophysicists using the Recognition Science ledger would cite it when propagating microscopic force constraints into stellar structure calculations. The construction is a direct one-line abbreviation of the upstream nuclear-force ledger definition.
Claim. The neutron-star equation-of-state ledger condition holds precisely when the volume coefficient, surface coefficient, Coulomb coefficient, and asymmetry coefficient of the nuclear force are each strictly positive.
background
In the Nuclear module the neutron-star equation-of-state structure is constructed by direct reference to the nuclear-force ledger. The upstream definition states that the nuclear-force ledger holds when the volume, surface, Coulomb, and asymmetry coefficients are all positive; this supplies the effective coefficients required for the ledger-based treatment of nuclear interactions. The module imports NuclearForceStructure to inherit this positivity requirement without additional hypotheses.
proof idea
The definition is a one-line abbreviation that directly copies the body of the nuclear_force_from_ledger definition.
why it matters
This definition supplies the interface that lets neutron-star EOS theorems inherit nuclear-force positivity. It is invoked by neutron_star_eos_structure (which asserts the condition via has_nuclear_force_structure) and by the r-process yields theorems that propagate the same ledger condition. Within the Recognition Science chain it closes the link between the nuclear-force coefficients (derived from the Recognition Composition Law) and neutron-star observables, with no scaffolding remaining at this step.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.