neutron_star_eos_structure
plain-language theorem explainer
Neutron-star equation-of-state structure follows from the nuclear-force ledger. Compact-object modelers cite this link to ground EOS inputs in the force structure. The proof is a one-line wrapper applying the has_nuclear_force_structure theorem.
Claim. The neutron-star equation-of-state structure holds because it is defined to coincide with the nuclear-force structure from the ledger.
background
Nuclear structure in Recognition Science rests on a ledger that encodes force relations. The nuclear_force_from_ledger proposition asserts that the nuclear force structure is realized in the ledger. The has_nuclear_force_structure theorem proves this by direct reduction to nuclear_force_structure, as shown in both the IslandOfStabilityStructure and NeutronStarEOSStructure modules.
proof idea
The proof is a one-line wrapper that applies has_nuclear_force_structure.
why it matters
This theorem is invoked by has_ns_eos_structure in the RProcessYieldsStructure module to supply the EOS structure for r-process calculations. It advances the nuclear sector of the Recognition Science framework by linking neutron-star modeling to the force ledger.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.