nsRegime_count
plain-language theorem explainer
The declaration proves that the inductive type enumerating neutron star crustal regimes has exactly five elements. Modelers of neutron star structure in the Recognition Science framework cite this result to anchor the five-regime decomposition on the phi-ladder. The proof proceeds by a single decide tactic that exploits the derived Fintype instance on the inductive definition.
Claim. The finite type of neutron star crustal regimes satisfies $|NSRegime| = 5$.
background
The module defines five canonical neutron-star crustal regimes corresponding to configDim D = 5: outer crust, inner crust, nuclear pasta, outer core, and inner core. These form an inductive type NSRegime whose constructors are outerCrust, innerCrust, nuclearPasta, outerCore, and innerCore, from which a Fintype instance is derived automatically. The local setting is the derivation of neutron star properties from the Recognition Science phi-ladder, where adjacent regimes differ by a density factor of phi.
proof idea
The proof is a one-line wrapper that invokes the decide tactic on the equality Fintype.card NSRegime = 5, which succeeds because the inductive definition supplies an explicit enumeration of five constructors.
why it matters
This result supplies the five_regimes field in the neutronStarCert definition, which certifies the overall neutron star model with phi_ratio and density positivity. It realizes the configDim D = 5 landmark from the forcing chain and supports the density rung structure on the phi-ladder.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.