pith. sign in
module module moderate

IndisputableMonolith.Physics.NeutronStarCrustalRegimesFromRS

show as:
view Lean formalization →

This module defines neutron star crustal regimes derived from Recognition Science. It introduces NSRegime as a discrete classification of density layers with associated functions for density and certification predicates. Astrophysicists and RS researchers would cite it when modeling compact-object interiors in native units. The module is purely definitional with no proofs.

claimThe module introduces the type $NSRegime$ together with functions $density : NSRegime → ℝ_{>0}$, $density_ratio$, $density_pos$ and the predicate $NeutronStarCert$.

background

The module sits in the physics domain and imports the RS time quantum τ₀ = 1 tick from IndisputableMonolith.Constants. It builds definitions for neutron-star crusts on top of the phi-ladder and J-cost structures supplied by the upstream forcing chain. The local setting applies Recognition Science constants (c = 1, ħ = φ^{-5}) to classify density regimes without external fitting parameters.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The module supplies the regime classifications that connect the phi-ladder and mass formula to neutron-star observables. It feeds higher-level physics statements on stellar structure even though the current dependency graph lists no direct used_by edges. It touches the D = 3 and eight-tick octave landmarks by restricting the phi-ladder to crustal layers.

scope and limits

depends on (1)

Lean names referenced from this declaration's body.

declarations in this module (7)