pith. machine review for the scientific record. sign in
module module moderate

IndisputableMonolith.Nuclear.NeutronStarEOSStructure

show as:
view Lean formalization →

The module defines neutron-star equation-of-state structures that imply the positive effective nuclear-force coefficients required by the Recognition ledger. Astrophysicists modeling compact objects or r-process yields cite it to maintain consistency with the J-cost and phi-ladder framework. It consists of four sibling definitions and one implication theorem that transfers the nuclear-force positivity result into the stellar context.

claimNeutron-star equation-of-state structure implies positive effective nuclear-force coefficients: neutron-star EOS structure maps to nuclear-force coefficients satisfying $c > 0$.

background

Recognition Science derives nuclear interactions from the J-functional equation and the self-similar fixed point phi. The upstream NuclearForceStructure module establishes that effective nuclear-force coefficients remain positive under this law. This module introduces neutron-star EOS structure as the ledger-based encoding of the equation of state for neutron-star matter, together with the implication that maps stellar density profiles back to the force coefficients.

proof idea

This is a definition module, no proofs. The argument structure consists of direct definitions of the EOS objects from the ledger and a straightforward implication that inherits positivity from the nuclear-force module.

why it matters in Recognition Science

The module supplies the nuclear-force-side input required by the downstream RProcessYieldsStructure for computing r-process yields. It closes the link between neutron-star interiors and the positive nuclear coefficients in the Recognition framework, enabling consistent modeling of nucleosynthesis in high-density environments.

scope and limits

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (1)

Lean names referenced from this declaration's body.

declarations in this module (4)