NSRegime
plain-language theorem explainer
This inductive definition enumerates the five canonical neutron-star regimes recognized in Recognition Science. Astrophysicists deriving density profiles on the phi-ladder would cite it to enforce adjacent-regime ratios equal to phi. The definition consists of five explicit constructors with automatic derivation of Fintype and equality instances, enabling direct cardinality proofs and case analysis.
Claim. The inductive type enumerating neutron-star regimes is defined with five constructors: outer crust, inner crust, nuclear pasta, outer core, and inner core.
background
The module sets five canonical neutron-star crustal regimes equal to configDim D = 5, with adjacent-regime density ratios fixed at phi on the phi-ladder. This draws from the Recognition Science forcing chain where T5 fixes J-uniqueness, T6 forces phi as self-similar fixed point, and T8 yields D = 3 spatial dimensions, extended here to layered stellar structure. The imported Constants module supplies phi and related RS-native values such as c = 1 and G = phi^5 / pi.
proof idea
This is a direct inductive definition with five constructors followed by derivation of DecidableEq, Repr, BEq, and Fintype instances.
why it matters
The definition supplies the type for the NeutronStarCert structure asserting Fintype.card = 5 together with the phi density ratio and positivity properties. It also supports the nsRegime_count theorem. In the framework it realizes configDim D = 5 for neutron stars, extending the phi-ladder and eight-tick octave to astrophysical scales while remaining consistent with the Recognition Composition Law.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.